Documentation Verification Report

l2Space

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

Statistics

Metric	Count
Definitions `HilbertBasis`, `instFunLike`, `instInhabitedSubtypePreLpMemAddSubgroupLpOfNatENNReal`, `mk`, `mkOfOrthogonalEqBot`, `repr`, `toOrthonormalBasis`, `IsHilbertSum`, `linearIsometryEquiv`, `linearIsometry`, `toHilbertBasis`, `instInnerProductSpace`, `«termℓ²(_,_)»`»)	13
Theorems `coe_mk`, `coe_mkOfOrthogonalEqBot`, `coe_toOrthonormalBasis`, `dense_span`, `finite_spans_dense`, `hasSum_inner_mul_inner`, `hasSum_orthogonalProjection`, `hasSum_repr`, `hasSum_repr_symm`, `orthonormal`, `repr_apply_apply`, `repr_self`, `repr_symm_single`, `summable_inner_mul_inner`, `tsum_inner_mul_inner`, `OrthogonalFamily`, `hasSum_linearIsometryEquiv_symm`, `linearIsometryEquiv_apply_dfinsupp_sum_single`, `linearIsometryEquiv_symm_apply`, `linearIsometryEquiv_symm_apply_dfinsupp_sum_single`, `linearIsometryEquiv_symm_apply_single`, `mk`, `mkInternal`, `surjective_isometry`, `hasSum_linearIsometry`, `linearIsometry_apply`, `linearIsometry_apply_dfinsupp_sum_single`, `linearIsometry_apply_single`, `range_linearIsometry`, `summable_of_lp`, `exists_hilbertBasis_extension`, `isHilbertSum`, `linearIsometryEquiv_symm_apply_single_one`, `coe_toHilbertBasis`, `isHilbertSumOrthogonal`, `exists_hilbertBasis`, `hasSum_inner`, `inner_eq_tsum`, `inner_single_left`, `inner_single_right`, `summable_inner`	41
Total	54

HilbertBasis

Definitions

Name	Category	Theorems
`instFunLike` 📖	CompOp	20 math math: `coe_mk`, `UnitAddTorus.coe_mFourierBasis`, `Orthonormal.exists_hilbertBasis_extension`, `exists_hilbertBasis`, `hasSum_orthogonalProjection`, `hasSum_repr`, `coe_mkOfOrthogonalEqBot`, `dense_span`, `coe_fourierBasis`, `orthonormal`, `repr_symm_single`, `repr_apply_apply`, `repr_self`, `summable_inner_mul_inner`, `OrthonormalBasis.coe_toHilbertBasis`, `coe_toOrthonormalBasis`, `tsum_inner_mul_inner`, `hasSum_inner_mul_inner`, `hasSum_repr_symm`, `finite_spans_dense`
`instInhabitedSubtypePreLpMemAddSubgroupLpOfNatENNReal` 📖	CompOp	—
`mk` 📖	CompOp	—
`mkOfOrthogonalEqBot` 📖	CompOp	1 math math: `coe_mkOfOrthogonalEqBot`
`repr` 📖	CompOp	7 math math: `hasSum_repr`, `repr_symm_single`, `repr_apply_apply`, `repr_self`, `UnitAddTorus.mFourierBasis_repr`, `fourierBasis_repr`, `hasSum_repr_symm`
`toOrthonormalBasis` 📖	CompOp	1 math math: `coe_toOrthonormalBasis`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.topologicalClosure` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Submodule.span` `Set.range`	`DFunLike.coe` `HilbertBasis` `instFunLike`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `Orthonormal.isHilbertSum` `Orthonormal.linearIsometryEquiv_symm_apply_single_one`
`coe_mkOfOrthogonalEqBot` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Submodule.orthogonal` `Submodule.span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Set.range` `Bot.bot` `Submodule` `Submodule.instBot`	`DFunLike.coe` `HilbertBasis` `instFunLike` `mkOfOrthogonalEqBot`	—	—
`coe_toOrthonormalBasis` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `toOrthonormalBasis` `HilbertBasis` `instFunLike`	—	`orthonormal`
`dense_span` 📖	mathematical	—	`Submodule.topologicalClosure` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Submodule.span` `Set.range` `DFunLike.coe` `HilbertBasis` `instFunLike` `Top.top` `Submodule` `Submodule.instTop`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `eq_top_iff` `mem_closure_of_tendsto` `Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `hasSum_repr` `Filter.Eventually.of_forall` `Finset.sum_congr` `sum_mem` `AddSubmonoid.instAddSubmonoidClass` `Submodule.smul_mem` `Submodule.subset_span`
`finite_spans_dense` 📖	mathematical	—	`Submodule.topologicalClosure` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iSup` `Submodule` `Finset` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.span` `SetLike.coe` `Finset.instSetLike` `Finset.image` `DFunLike.coe` `HilbertBasis` `instFunLike` `Top.top` `Submodule.instTop`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `eq_top_iff` `LE.le.trans` `Eq.ge` `dense_span` `Submodule.topologicalClosure.congr_simp` `Submodule.topologicalClosure_mono` `Submodule.span_mono` `Set.range_subset_iff` `Set.mem_iUnion_of_mem` `Finset.mem_coe` `Finset.mem_image_of_mem` `Finset.mem_singleton_self`
`hasSum_inner_mul_inner` 📖	mathematical	—	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `HilbertBasis` `instFunLike` `SummationFilter.unconditional`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `innerSL_apply_apply` `repr_apply_apply` `inner_smul_right` `mul_comm` `HasSum.mapL` `hasSum_repr`
`hasSum_orthogonalProjection` 📖	mathematical	—	`HasSum` `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` `Submodule.setLike` `Submodule.addCommMonoid` `instTopologicalSpaceSubtype` `Submodule.smul` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `HilbertBasis` `Submodule.normedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `instFunLike` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.module` `ContinuousLinearMap.funLike` `Submodule.orthogonalProjection` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `repr_apply_apply` `Submodule.inner_orthogonalProjection_eq_of_mem_left` `hasSum_repr`
`hasSum_repr` 📖	mathematical	—	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Module.toDistribMulAction` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `PreLp` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `repr` `HilbertBasis` `instFunLike` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `LinearIsometryEquiv.symm_apply_apply` `hasSum_repr_symm`
`hasSum_repr_symm` 📖	mathematical	—	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Module.toDistribMulAction` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `PreLp` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `HilbertBasis` `instFunLike` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `repr` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `LinearIsometryEquiv.injective` `lp.single_smul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `repr_self` `mul_one` `LinearIsometryEquiv.coe_toContinuousLinearEquiv` `LinearIsometryEquiv.apply_symm_apply` `lp.hasSum_single` `ENNReal.ofNat_ne_top` `ContinuousLinearMap.hasSum`
`orthonormal` 📖	mathematical	—	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `HilbertBasis` `instFunLike`	—	`orthonormal_iff_ite` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `RingHomInvPair.ids` `LinearIsometryEquiv.inner_map_map` `NormedSpace.toIsBoundedSMul` `repr_self` `lp.inner_single_left` `lp.single_apply` `Pi.single_apply` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one`
`repr_apply_apply` 📖	mathematical	—	`PreLp` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `repr` `Inner.inner` `InnerProductSpace.toInner` `HilbertBasis` `instFunLike`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `LinearIsometryEquiv.inner_map_map` `repr_self` `lp.inner_single_left` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one`
`repr_self` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PreLp` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `NormedAddCommGroup.toSeminormedAddCommGroup` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `repr` `HilbertBasis` `instFunLike` `lp.single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `repr_symm_single` `LinearIsometryEquiv.apply_symm_apply`
`repr_symm_single` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PreLp` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `NormedAddCommGroup.toSeminormedAddCommGroup` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `repr` `lp.single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `HilbertBasis` `instFunLike`	—	`RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`summable_inner_mul_inner` 📖	mathematical	—	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `HilbertBasis` `instFunLike` `SummationFilter.unconditional`	—	`HasSum.summable` `hasSum_inner_mul_inner`
`tsum_inner_mul_inner` 📖	mathematical	—	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `HilbertBasis` `instFunLike` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_inner_mul_inner`

IsHilbertSum

Definitions

Name	Category	Theorems
`linearIsometryEquiv` 📖	CompOp	6 math math: `linearIsometryEquiv_symm_apply`, `hasSum_linearIsometryEquiv_symm`, `Orthonormal.linearIsometryEquiv_symm_apply_single_one`, `linearIsometryEquiv_symm_apply_dfinsupp_sum_single`, `linearIsometryEquiv_symm_apply_single`, `linearIsometryEquiv_apply_dfinsupp_sum_single`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`OrthogonalFamily` 📖	mathematical	`IsHilbertSum`	`OrthogonalFamily` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—
`hasSum_linearIsometryEquiv_symm` 📖	mathematical	`IsHilbertSum`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `LinearIsometry` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearIsometry.instFunLike` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `LinearIsometryEquiv` `RingHomInvPair.ids` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `linearIsometryEquiv` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `OrthogonalFamily` `surjective_isometry` `LinearIsometryEquiv.coe_ofSurjective`
`linearIsometryEquiv_apply_dfinsupp_sum_single` 📖	mathematical	`IsHilbertSum`	`PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `DFinsupp.sum` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `linearIsometryEquiv` `LinearIsometry` `LinearIsometry.instFunLike` `DFinsupp` `DFinsupp.instDFunLike`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `RingHomInvPair.ids` `NormedSpace.toIsBoundedSMul` `map_dfinsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `linearIsometryEquiv_symm_apply_dfinsupp_sum_single` `LinearIsometryEquiv.apply_symm_apply` `AddSubgroup.val_finset_sum` `Finset.sum_apply` `Finset.sum_congr` `Finset.sum_pi_single`
`linearIsometryEquiv_symm_apply` 📖	mathematical	`IsHilbertSum`	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `NormedAddCommGroup.toSeminormedAddCommGroup` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `linearIsometryEquiv` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearIsometry` `LinearIsometry.instFunLike` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `OrthogonalFamily` `surjective_isometry` `LinearIsometryEquiv.coe_ofSurjective`
`linearIsometryEquiv_symm_apply_dfinsupp_sum_single` 📖	mathematical	`IsHilbertSum`	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `NormedAddCommGroup.toSeminormedAddCommGroup` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `linearIsometryEquiv` `DFinsupp.sum` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `lp.single` `LinearIsometry` `LinearIsometry.instFunLike`	—	`RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `map_dfinsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `DFinsupp.sum.congr_simp` `linearIsometryEquiv_symm_apply_single`
`linearIsometryEquiv_symm_apply_single` 📖	mathematical	`IsHilbertSum`	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `NormedAddCommGroup.toSeminormedAddCommGroup` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `linearIsometryEquiv` `lp.single` `LinearIsometry` `LinearIsometry.instFunLike`	—	`RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `OrthogonalFamily` `surjective_isometry` `LinearIsometryEquiv.coe_ofSurjective` `OrthogonalFamily.linearIsometry_apply_single`
`mk` 📖	mathematical	`CompleteSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `OrthogonalFamily` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.topologicalClosure` `UniformSpace.toTopologicalSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearIsometry.toLinearMap`	`IsHilbertSum`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomSurjective.ids` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `LinearIsometry.coe_toLinearMap` `LinearMap.range_eq_top` `eq_top_iff` `LE.le.trans_eq` `OrthogonalFamily.range_linearIsometry`
`mkInternal` 📖	mathematical	`CompleteSpace` `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` `Submodule.setLike` `instUniformSpaceSubtype` `OrthogonalFamily` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.topologicalClosure` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	`IsHilbertSum` `Submodule.normedAddCommGroup`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomSurjective.ids` `Submodule.topologicalClosure.congr_simp` `Submodule.range_subtype`
`surjective_isometry` 📖	mathematical	`IsHilbertSum`	`PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `LinearIsometry` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedAddCommGroup.toSeminormedAddCommGroup` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NormedSpace.toIsBoundedSMul` `LinearIsometry.instFunLike` `OrthogonalFamily.linearIsometry` `OrthogonalFamily`	—	—

OrthogonalFamily

Definitions

Name	Category	Theorems
`linearIsometry` 📖	CompOp	6 math math: `IsHilbertSum.surjective_isometry`, `linearIsometry_apply_single`, `linearIsometry_apply_dfinsupp_sum_single`, `hasSum_linearIsometry`, `range_linearIsometry`, `linearIsometry_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum_linearIsometry` 📖	mathematical	`OrthogonalFamily` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `LinearIsometry` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearIsometry.instFunLike` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toIsBoundedSMul` `linearIsometry` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `Summable.hasSum` `summable_of_lp`
`linearIsometry_apply` 📖	mathematical	`OrthogonalFamily` `NormedAddCommGroup.toSeminormedAddCommGroup`	`DFunLike.coe` `LinearIsometry` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NormedSpace.toIsBoundedSMul` `LinearIsometry.instFunLike` `linearIsometry` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul`
`linearIsometry_apply_dfinsupp_sum_single` 📖	mathematical	`OrthogonalFamily` `NormedAddCommGroup.toSeminormedAddCommGroup`	`DFunLike.coe` `LinearIsometry` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NormedSpace.toIsBoundedSMul` `LinearIsometry.instFunLike` `linearIsometry` `DFinsupp.sum` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `lp.single`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `map_dfinsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `LinearIsometry.instSemilinearIsometryClass` `DFinsupp.sum.congr_simp` `linearIsometry_apply_single`
`linearIsometry_apply_single` 📖	mathematical	`OrthogonalFamily` `NormedAddCommGroup.toSeminormedAddCommGroup`	`DFunLike.coe` `LinearIsometry` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NormedSpace.toIsBoundedSMul` `LinearIsometry.instFunLike` `linearIsometry` `lp.single`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `linearIsometry_apply` `tsum_ite_eq` `SummationFilter.instLeAtTopUnconditional` `lp.single_apply` `Pi.single_eq_same` `Pi.single_eq_of_ne` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `LinearIsometry.instSemilinearIsometryClass`
`range_linearIsometry` 📖	mathematical	`OrthogonalFamily` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompleteSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`LinearMap.range` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NormedSpace.toIsBoundedSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearIsometry.toLinearMap` `linearIsometry` `Submodule.topologicalClosure` `UniformSpace.toTopologicalSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`le_antisymm` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedSpace.toIsBoundedSMul` `RingHomSurjective.ids` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `mem_closure_of_tendsto` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `hasSum_linearIsometry` `Filter.Eventually.of_forall` `SetLike.mem_coe` `sum_mem` `AddSubmonoid.instAddSubmonoidClass` `Submodule.mem_iSup_of_mem` `LinearMap.mem_range_self` `Submodule.topologicalClosure_minimal` `iSup_le` `linearIsometry_apply_single` `IsComplete.isClosed` `T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `IsUniformInducing.isComplete_range` `lp.completeSpace` `Isometry.isUniformInducing` `LinearIsometry.isometry`
`summable_of_lp` 📖	mathematical	`OrthogonalFamily` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `LinearIsometry` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearIsometry.instFunLike` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `summable_iff_norm_sq_summable` `ENNReal.toReal_natCast` `Real.rpow_natCast` `Memℓp.summable` `ENNReal.toReal_ofNat` `Real.instIsOrderedRing` `Real.instNontrivial` `lp.memℓp`

Orthonormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_hilbertBasis_extension` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	`Set.instHasSubset` `DFunLike.coe` `HilbertBasis` `Set.Elem` `HilbertBasis.instFunLike`	—	`exists_maximal_orthonormal` `Subtype.range_coe_subtype` `maximal_orthonormal_iff_orthogonalComplement_eq_bot` `HilbertBasis.coe_mkOfOrthogonalEqBot`
`isHilbertSum` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.topologicalClosure` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Submodule.span` `Set.range`	`IsHilbertSum` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `RCLike.innerProductSpace` `LinearIsometry.toSpanSingleton` `DenselyNormedField.toNontriviallyNormedField` `Pairwise` `Inner.inner` `InnerProductSpace.toInner`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RCLike.toCompleteSpace` `orthogonalFamily` `RingHomSurjective.ids` `Set.iUnion_singleton_eq_range`
`linearIsometryEquiv_symm_apply_single_one` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.topologicalClosure` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Submodule.span` `Set.range`	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PreLp` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `lp.normedAddCommGroup` `fact_one_le_two_ennreal` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `IsHilbertSum.linearIsometryEquiv` `LinearIsometry.toSpanSingleton` `DenselyNormedField.toNontriviallyNormedField` `Pairwise` `Inner.inner` `InnerProductSpace.toInner` `isHilbertSum` `lp.single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `isHilbertSum` `IsHilbertSum.linearIsometryEquiv_symm_apply_single` `LinearIsometry.toSpanSingleton_apply` `one_smul`

OrthonormalBasis

Definitions

Name	Category	Theorems
`toHilbertBasis` 📖	CompOp	1 math math: `coe_toHilbertBasis`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toHilbertBasis` 📖	mathematical	—	`DFunLike.coe` `HilbertBasis` `HilbertBasis.instFunLike` `toHilbertBasis` `OrthonormalBasis` `instFunLike`	—	`orthonormal`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isHilbertSumOrthogonal` 📖	mathematical	—	`IsHilbertSum` `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` `normedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `innerProductSpace` `subtypeₗᵢ`	—	`instOrthogonalCompleteSpace` `IsHilbertSum.mkInternal` `orthogonalFamily_self` `le_trans` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iSup_bool_eq` `Codisjoint.top_le` `IsCompl.codisjoint` `isCompl_orthogonal_of_hasOrthogonalProjection` `HasOrthogonalProjection.ofCompleteSpace` `le_topologicalClosure`

(root)

Definitions

Name	Category	Theorems
`HilbertBasis` 📖	CompData	20 math math: `HilbertBasis.coe_mk`, `UnitAddTorus.coe_mFourierBasis`, `Orthonormal.exists_hilbertBasis_extension`, `exists_hilbertBasis`, `HilbertBasis.hasSum_orthogonalProjection`, `HilbertBasis.hasSum_repr`, `HilbertBasis.coe_mkOfOrthogonalEqBot`, `HilbertBasis.dense_span`, `coe_fourierBasis`, `HilbertBasis.orthonormal`, `HilbertBasis.repr_symm_single`, `HilbertBasis.repr_apply_apply`, `HilbertBasis.repr_self`, `HilbertBasis.summable_inner_mul_inner`, `OrthonormalBasis.coe_toHilbertBasis`, `HilbertBasis.coe_toOrthonormalBasis`, `HilbertBasis.tsum_inner_mul_inner`, `HilbertBasis.hasSum_inner_mul_inner`, `HilbertBasis.hasSum_repr_symm`, `HilbertBasis.finite_spans_dense`
`IsHilbertSum` 📖	CompData	4 math math: `IsHilbertSum.mkInternal`, `Orthonormal.isHilbertSum`, `IsHilbertSum.mk`, `Submodule.isHilbertSumOrthogonal`
`«termℓ²(_,_)»` 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_hilbertBasis` 📖	mathematical	—	`DFunLike.coe` `HilbertBasis` `Set.Elem` `HilbertBasis.instFunLike` `Set` `Set.instMembership`	—	`Orthonormal.exists_hilbertBasis_extension` `orthonormal_empty`

lp

Definitions

Name	Category	Theorems
`instInnerProductSpace` 📖	CompOp	4 math math: `inner_eq_tsum`, `inner_single_right`, `inner_single_left`, `hasSum_inner`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum_inner` 📖	mathematical	—	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `normedAddCommGroup` `fact_one_le_two_ennreal` `instInnerProductSpace` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `Summable.hasSum` `summable_inner`
`inner_eq_tsum` 📖	mathematical	—	`Inner.inner` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `normedAddCommGroup` `fact_one_le_two_ennreal` `instInnerProductSpace` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal`
`inner_single_left` 📖	mathematical	—	`Inner.inner` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `normedAddCommGroup` `fact_one_le_two_ennreal` `instInnerProductSpace` `single`	—	`Nat.instAtLeastTwoHAddOfNat` `HasSum.unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `fact_one_le_two_ennreal` `hasSum_inner` `Pi.single_eq_same` `Pi.single_eq_of_ne` `inner_zero_left` `hasSum_ite_eq` `SummationFilter.instLeAtTopUnconditional`
`inner_single_right` 📖	mathematical	—	`Inner.inner` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `normedAddCommGroup` `fact_one_le_two_ennreal` `instInnerProductSpace` `single`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `inner_conj_symm` `inner_single_left`
`summable_inner` 📖	mathematical	—	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `Summable.of_norm_bounded` `RCLike.toCompleteSpace` `summable_mul` `Real.holderConjugate_iff` `ENNReal.toReal_ofNat` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `add_halves` `CharZero.NeZero.two` `norm_inner_le_norm`

---

← Back to Index