Documentation Verification Report

Reproducing

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

Statistics

Metric	Count
Definitions `RKHS`, `H₀`, `OfKernel`, `instRKHS`, `coeCLM`, `instFunLike`, `instInnerProductSpaceH₀`, `instPreInnerProductSpaceCoreH₀`, `instSeminormedAddCommGroupH₀`, `kerFun`, `kernel`	11
Theorems `kernel_ofKernel`, `coeCLM_apply`, `coeCLM_injective`, `coe_add`, `coe_neg`, `coe_smul`, `coe_sub`, `coe_zero`, `continuous_eval`, `ext`, `ext_iff`, `inner_kerFun`, `isHermitian_kernel`, `kerFun_apply`, `kerFun_dense`, `kerFun_inner`, `kernel_apply`, `kernel_inner`, `posSemidef_kernel`, `posSemidef_tfae`	20
Total	31

RKHS

Definitions

Name	Category	Theorems
`H₀` 📖	CompOp	1 math math: `OfKernel.kernel_ofKernel`
`OfKernel` 📖	CompOp	1 math math: `OfKernel.kernel_ofKernel`
`coeCLM` 📖	CompOp	2 math math: `coeCLM_injective`, `coeCLM_apply`
`instFunLike` 📖	CompOp	11 math math: `coe_add`, `coe_smul`, `continuous_eval`, `kerFun_apply`, `ext_iff`, `inner_kerFun`, `coeCLM_apply`, `kerFun_inner`, `coe_sub`, `coe_neg`, `coe_zero`
`instInnerProductSpaceH₀` 📖	CompOp	1 math math: `OfKernel.kernel_ofKernel`
`instPreInnerProductSpaceCoreH₀` 📖	CompOp	—
`instSeminormedAddCommGroupH₀` 📖	CompOp	1 math math: `OfKernel.kernel_ofKernel`
`kerFun` 📖	CompOp	6 math math: `kernel_apply`, `kerFun_apply`, `kerFun_dense`, `inner_kerFun`, `kerFun_inner`, `kernel_inner`
`kernel` 📖	CompOp	6 math math: `kernel_apply`, `isHermitian_kernel`, `kerFun_apply`, `OfKernel.kernel_ofKernel`, `kernel_inner`, `posSemidef_kernel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `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` `Pi.topologicalSpace` `Pi.addCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Pi.Function.module` `ContinuousLinearMap.funLike` `coeCLM` `instFunLike`	—	—
`coeCLM_injective` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `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` `Pi.topologicalSpace` `Pi.addCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Pi.Function.module` `ContinuousLinearMap.funLike` `coeCLM`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `instFunLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Pi.instAdd`	—	`ContinuousLinearMap.map_add`
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Pi.instNeg`	—	`ContinuousLinearMap.map_neg`
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Function.hasSMul`	—	`ContinuousLinearMap.map_smul`
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `instFunLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Pi.instSub`	—	`ContinuousLinearMap.map_sub`
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Pi.instZero`	—	`ContinuousLinearMap.map_zero`
`continuous_eval` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `instFunLike`	—	`Continuous.comp'` `continuous_apply` `ContinuousLinearMap.continuous`
`ext` 📖	—	`DFunLike.coe` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `instFunLike`	—	`ext`
`inner_kerFun` 📖	mathematical	—	`Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.funLike` `kerFun` `instFunLike`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.adjoint_adjoint`
`isHermitian_kernel` 📖	mathematical	—	`Matrix.IsHermitian` `ContinuousLinearMap` `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` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.instStarId` `kernel`	—	`Matrix.ext` `ContinuousLinearMap.ext` `ext_inner_right` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.adjoint_inner_left` `inner_conj_symm` `kernel_inner`
`kerFun_apply` 📖	mathematical	—	`DFunLike.coe` `instFunLike` `ContinuousLinearMap` `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` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.funLike` `kerFun` `kernel`	—	`ContinuousLinearMap.comp.congr_simp` `ContinuousLinearMap.adjoint_adjoint`
`kerFun_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` `Submodule.span` `setOf` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `kerFun` `Top.top` `Submodule` `Submodule.instTop`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Submodule.orthogonal_eq_bot_iff` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `Submodule.topologicalClosure.completeSpace` `Submodule.eq_bot_iff` `DFunLike.ext` `ext_inner_left` `coe_zero` `inner_zero_right` `Submodule.inner_right_of_mem_orthogonal` `subset_closure`
`kerFun_inner` 📖	mathematical	—	`Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.funLike` `kerFun` `instFunLike`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.adjoint_adjoint`
`kernel_apply` 📖	mathematical	—	`kernel` `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` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHomCompTriple.ids` `DFunLike.coe` `LinearIsometryEquiv` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `ContinuousLinearMap` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `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` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `ContinuousLinearMap.adjoint` `kerFun`	—	`RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.comp.congr_simp` `ContinuousLinearMap.adjoint_adjoint`
`kernel_inner` 📖	mathematical	—	`Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.funLike` `kernel` `kerFun`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`posSemidef_kernel` 📖	mathematical	—	`Matrix.PosSemidef` `ContinuousLinearMap` `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` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.ring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.instLoewnerPartialOrder` `ContinuousLinearMap.instStarRingId` `kernel`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `isHermitian_kernel` `ContinuousLinearMap.isPositive_iff'` `IsSelfAdjoint.eq_1` `sub_zero` `star_finsuppSum` `Finsupp.sum_comm` `IsTopologicalAddGroup.toContinuousAdd` `StarMul.star_mul` `Matrix.IsHermitian.apply` `star_star` `RingHomIsometric.ids` `Finsupp.sum_apply''` `Finsupp.sum_inner` `RingHomInvPair.instStarRingEnd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.adjoint_inner_left` `kernel_inner` `inner_self_eq_norm_sq_to_K` `IsOrderedRing.toPosMulMono` `StarOrderedRing.toIsOrderedRing` `RCLike.toStarOrderedRing`
`posSemidef_tfae` 📖	mathematical	—	`List.TFAE` `Matrix.PosSemidef` `ContinuousLinearMap` `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` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.ring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.instLoewnerPartialOrder` `ContinuousLinearMap.instStarRingId` `Matrix.IsHermitian` `ContinuousLinearMap.instStarId`	—	`List.TFAE.out` `List.tfae_of_cycle` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `RingHomIsometric.ids` `RingHomInvPair.instStarRingEnd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Finsupp.sum_apply''` `Finsupp.sum_inner` `ContinuousLinearMap.adjoint_inner_left` `subsingleton_or_nontrivial` `inner_self_eq_norm_sq_to_K` `norm_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Finsupp.sum_fun_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `instReflLe` `MulZeroClass.mul_zero` `exists_ne` `Finsupp.sum_comm` `IsScalarTower.left` `IsBoundedSMul.continuousSMul` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Finsupp.sum_sum_index` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `inner_zero_left` `map_add` `SemilinearMapClass.toAddHomClass` `inner_add_left` `Finsupp.sum_single_index` `IsUnit.div_mul_cancel` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `inner_zero_right` `inner_add_right` `Finsupp.sum_add` `mul_comm` `inner_smul_right` `inner_smul_left` `MulZeroClass.zero_mul` `RCLike.charZero_rclike` `RingHomClass.toLinearMapClassNNRat` `add_mul` `Distrib.rightDistribClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `one_mul`

RKHS.OfKernel

Definitions

Name	Category	Theorems
`instRKHS` 📖	CompOp	1 math math: `kernel_ofKernel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`kernel_ofKernel` 📖	mathematical	—	`RKHS.kernel` `RKHS.OfKernel` `UniformSpace.Completion.instNormedAddCommGroup` `RKHS.H₀` `RKHS.instSeminormedAddCommGroupH₀` `UniformSpace.Completion.innerProductSpace` `RKHS.instInnerProductSpaceH₀` `instRKHS` `UniformSpace.Completion.completeSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Matrix.ext` `UniformSpace.Completion.completeSpace` `ContinuousLinearMap.ext` `ext_inner_right` `ContinuousLinearMap.comp.congr_simp` `ContinuousLinearMap.adjoint_adjoint` `ContinuousLinearMap.adjoint_inner_left` `UniformSpace.Completion.inner_coe` `Finsupp.sum_single_index` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `mul_one` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `one_mul`

(root)

Definitions

Name	Category	Theorems
`RKHS` 📖	CompData	—

---

← Back to Index