ProdL2

📁 Source: Mathlib/Analysis/InnerProductSpace/ProdL2.lean

Statistics

Metric	Count
Definitions prod, orthogonalDecomposition, instProdInnerProductSpace	3
Theorems prod_apply, coe_orthogonalDecomposition, coe_orthogonalDecomposition_symm, fstL_comp_coe_orthogonalDecomposition, fst_orthogonalDecomposition_apply, orthogonalDecomposition_apply, orthogonalDecomposition_symm_apply, sndL_comp_coe_orthogonalDecomposition, snd_orthogonalDecomposition_apply, toLinearEquiv_orthogonalDecomposition, toLinearEquiv_orthogonalDecomposition_symm, prod_inner_apply	12
Total	15

OrthonormalBasis

Definitions

Name	Category	Theorems
prod 📖	CompOp	1 math math: prod_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_apply 📖	mathematical	—	DFunLike.coe OrthonormalBasis WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat WithLp.instProdNormedAddCommGroup fact_one_le_two_ennreal WithLp.instProdInnerProductSpace instFintypeSum instFunLike prod WithLp.toLp LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Prod.instAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Prod.instModule LinearMap.instFunLike LinearMap.inl LinearMap.inr	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal RingHomInvPair.ids Module.Basis.coe_toOrthonormalBasis Module.Basis.prod_apply

Submodule

Definitions

Name	Category	Theorems
orthogonalDecomposition 📖	CompOp	10 math math: orthogonalDecomposition_symm_apply, toLinearEquiv_orthogonalDecomposition_symm, toLinearEquiv_orthogonalDecomposition, coe_orthogonalDecomposition_symm, coe_orthogonalDecomposition, fst_orthogonalDecomposition_apply, sndL_comp_coe_orthogonalDecomposition, fstL_comp_coe_orthogonalDecomposition, snd_orthogonalDecomposition_apply, orthogonalDecomposition_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_orthogonalDecomposition 📖	mathematical	—	ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Submodule ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Prod.instAddCommGroup Prod.instModule addCommMonoid module LinearIsometryEquiv.toContinuousLinearEquiv orthogonalDecomposition ContinuousLinearMap.comp instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid RingHomCompTriple.ids addCommGroup WithLp.instProdTopologicalSpace WithLp.instAddCommGroup ContinuousLinearEquiv.symm WithLp.prodContinuousLinearEquiv ContinuousLinearMap.prod orthogonalProjection instHasOrthogonalProjectionOrthogonal	—	ContinuousLinearMap.ext Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal RingHomInvPair.ids RingHomCompTriple.ids instHasOrthogonalProjectionOrthogonal orthogonalDecomposition_apply
coe_orthogonalDecomposition_symm 📖	mathematical	—	ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup WithLp.instModule Prod.instAddCommGroup Prod.instModule addCommMonoid module LinearIsometryEquiv.toContinuousLinearEquiv LinearIsometryEquiv.symm orthogonalDecomposition ContinuousLinearMap.comp instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid RingHomCompTriple.ids ContinuousLinearMap.coprod IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup subtypeL WithLp.instProdTopologicalSpace WithLp.instAddCommGroup addCommGroup WithLp.prodContinuousLinearEquiv	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal RingHomInvPair.ids
fstL_comp_coe_orthogonalDecomposition 📖	mathematical	—	ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal WithLp.instProdTopologicalSpace instTopologicalSpaceSubtype AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Prod.instAddCommGroup addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup WithLp.instModule Prod.instModule module RingHomCompTriple.ids WithLp.fstL ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal seminormedAddCommGroup addCommMonoid LinearIsometryEquiv.toContinuousLinearEquiv orthogonalDecomposition orthogonalProjection	—	ContinuousLinearMap.ext Nat.instAtLeastTwoHAddOfNat RingHomCompTriple.ids RingHomInvPair.ids fact_one_le_two_ennreal instHasOrthogonalProjectionOrthogonal orthogonalDecomposition_apply
fst_orthogonalDecomposition_apply 📖	mathematical	—	WithLp.fst ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithLp WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup Prod.instModule addCommMonoid module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike orthogonalDecomposition ContinuousLinearMap instTopologicalSpaceSubtype ContinuousLinearMap.funLike orthogonalProjection	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids fact_one_le_two_ennreal instHasOrthogonalProjectionOrthogonal orthogonalDecomposition_apply
orthogonalDecomposition_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup Prod.instModule addCommMonoid module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike orthogonalDecomposition WithLp.toLp ContinuousLinearMap instTopologicalSpaceSubtype ContinuousLinearMap.funLike orthogonalProjection instHasOrthogonalProjectionOrthogonal	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids fact_one_le_two_ennreal instHasOrthogonalProjectionOrthogonal isCompl_orthogonal_of_hasOrthogonalProjection IsCompl.symm orthogonal_orthogonal prodEquivOfIsCompl_symm_apply orthogonalProjection_apply_eq_linearProjOfIsCompl linearProjOfIsCompl.congr_simp
orthogonalDecomposition_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup Prod.instModule addCommMonoid module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm orthogonalDecomposition AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Ring.toSemiring WithLp.fst WithLp.snd	—	RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal
sndL_comp_coe_orthogonalDecomposition 📖	mathematical	—	ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal WithLp.instProdTopologicalSpace instTopologicalSpaceSubtype AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Prod.instAddCommGroup addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup WithLp.instModule Prod.instModule module RingHomCompTriple.ids WithLp.sndL ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal seminormedAddCommGroup addCommMonoid LinearIsometryEquiv.toContinuousLinearEquiv orthogonalDecomposition orthogonalProjection instHasOrthogonalProjectionOrthogonal	—	ContinuousLinearMap.ext Nat.instAtLeastTwoHAddOfNat RingHomCompTriple.ids RingHomInvPair.ids fact_one_le_two_ennreal instHasOrthogonalProjectionOrthogonal orthogonalDecomposition_apply starProjection_orthogonal_val
snd_orthogonalDecomposition_apply 📖	mathematical	—	WithLp.snd ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithLp WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup Prod.instModule addCommMonoid module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike orthogonalDecomposition ContinuousLinearMap instTopologicalSpaceSubtype ContinuousLinearMap.funLike orthogonalProjection instHasOrthogonalProjectionOrthogonal	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids fact_one_le_two_ennreal instHasOrthogonalProjectionOrthogonal orthogonalDecomposition_apply
toLinearEquiv_orthogonalDecomposition 📖	mathematical	—	LinearIsometryEquiv.toLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup Prod.instModule addCommMonoid module orthogonalDecomposition LinearEquiv.trans Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddCommMonoid WithLp.instAddCommGroup addCommGroup RingHomCompTriple.ids LinearEquiv.symm prodEquivOfIsCompl isCompl_orthogonal_of_hasOrthogonalProjection WithLp.linearEquiv	—	RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal
toLinearEquiv_orthogonalDecomposition_symm 📖	mathematical	—	LinearIsometryEquiv.toLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup Prod.instModule addCommMonoid module LinearIsometryEquiv.symm orthogonalDecomposition LinearEquiv.trans AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup addCommGroup RingHomCompTriple.ids WithLp.linearEquiv prodEquivOfIsCompl isCompl_orthogonal_of_hasOrthogonalProjection	—	RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal

WithLp

Definitions

Name	Category	Theorems
instProdInnerProductSpace 📖	CompOp	8 math math: prod_inner_apply, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, OrthonormalBasis.prod_apply, MeasureTheory.charFun_eq_prod_iff, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, ProbabilityTheory.indepFun_iff_charFun_prod, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, MeasureTheory.charFun_prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_inner_apply 📖	mathematical	—	Inner.inner WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat InnerProductSpace.toInner instProdSeminormedAddCommGroup fact_one_le_two_ennreal NormedAddCommGroup.toSeminormedAddCommGroup instProdInnerProductSpace Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ofLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal

---

← Back to Index