Pointwise

📁 Source: Mathlib/Analysis/Calculus/ContDiffHolder/Pointwise.lean

Statistics

Metric	Count
Definitions ContDiffPointwiseHolderAt	1
Theorems contDiffPointwiseHolderAt, clm_apply, comp, comp_of_differentiableAt, comp₂_of_differentiableAt, congr_of_eventuallyEq, const, contDiffAt, continuousAt, continuousLinearMap_comp, differentiableAt, fderiv, fst, id, isBigO, iteratedFDeriv, of_contDiffOn_holderOnWith, of_exponent_le, of_order_le, of_order_lt, of_toLex_le, prodMk, snd, zero_exponent_iff, zero_order_iff, contDiffPointwiseHolderAt, contDiffPointwiseHolderAt_left_comp, contDiffPointwiseHolderAt, contDiffPointwiseHolderAt_left_comp, contDiffPointwiseHolderAt_iff	30
Total	31

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffPointwiseHolderAt 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop ENat Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	ContDiffPointwiseHolderAt	—	of_le LT.lt.le SeminormedAddCommGroup.toIsTopologicalAddGroup DifferentiableAt.isBigO_sub smulCommClass_self differentiableAt_iteratedFDeriv Asymptotics.IsBigO.of_norm_left Asymptotics.IsBigO.comp_tendsto Asymptotics.IsBigO.id_rpow_of_le_one tendsto_norm_sub_self_nhdsGE

ContDiffPointwiseHolderAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
clm_apply 📖	mathematical	ContDiffPointwiseHolderAt ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing	DFunLike.coe ContinuousLinearMap.funLike	—	RingHomIsometric.ids smulCommClass_self comp₂_of_differentiableAt ContDiffAt.contDiffPointwiseHolderAt ContDiffAt.clm_apply contDiffAt_fst contDiffAt_snd WithTop.coe_lt_top DifferentiableAt.clm_apply DifferentiableAt.fst differentiableAt_id DifferentiableAt.snd
comp 📖	—	ContDiffPointwiseHolderAt	—	—	comp_of_differentiableAt differentiableAt
comp_of_differentiableAt 📖	—	ContDiffPointwiseHolderAt DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	—	ContDiffAt.comp contDiffAt SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.mp_mem Filter.Tendsto.eventually continuousAt ContDiffAt.eventually Filter.univ_mem' iteratedFDeriv_comp le_rfl FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO Filter.Tendsto.isBoundedUnder_le BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousAt.norm ContinuousAt.comp ContDiffAt.continuousAt_iteratedFDeriv WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero Asymptotics.IsBigO.trans Asymptotics.IsBigO.comp_tendsto isBigO of_order_le Asymptotics.IsBigO.rpow Filter.Eventually.of_forall norm_nonneg Asymptotics.IsBigO.norm_norm DifferentiableAt.isBigO_sub Asymptotics.IsBigO.of_norm_left RingHomInvPair.ids UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self DistribMulActionSemiHomClass.toAddMonoidHomClass IsTopologicalAddGroup.toContinuousAdd SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass LinearIsometryEquiv.norm_map zero_order_iff nonpos_iff_eq_zero Nat.instCanonicallyOrderedAdd Mathlib.Tactic.Contrapose.contrapose₂ differentiableAt Filter.isBoundedUnder_const instReflLe
comp₂_of_differentiableAt 📖	—	ContDiffPointwiseHolderAt Prod.normedAddCommGroup Prod.normedSpace Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instTopologicalSpaceProd	—	—	comp_of_differentiableAt prodMk DifferentiableAt.prodMk
congr_of_eventuallyEq 📖	—	ContDiffPointwiseHolderAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	—	ContDiffAt.congr_of_eventuallyEq contDiffAt Filter.EventuallyEq.symm Filter.EventuallyEq.trans_isBigO SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.EventuallyEq.sub Filter.EventuallyEq.iteratedFDeriv Filter.Eventually.self_of_nhds Filter.EventuallyEq.refl isBigO
const 📖	mathematical	—	ContDiffPointwiseHolderAt	—	ContDiffAt.contDiffPointwiseHolderAt contDiffAt_const WithTop.coe_lt_top
contDiffAt 📖	mathematical	ContDiffPointwiseHolderAt	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	—
continuousAt 📖	mathematical	ContDiffPointwiseHolderAt	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	ContDiffAt.continuousAt contDiffAt
continuousLinearMap_comp 📖	mathematical	ContDiffPointwiseHolderAt	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike	—	comp_of_differentiableAt ContinuousLinearMap.contDiffPointwiseHolderAt ContinuousLinearMap.differentiableAt
differentiableAt 📖	mathematical	ContDiffPointwiseHolderAt	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	ContDiffAt.differentiableAt contDiffAt Nat.cast_zero WithTop.charZero
fderiv 📖	mathematical	ContDiffPointwiseHolderAt	ContinuousLinearMap Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing fderiv	—	RingHomIsometric.ids smulCommClass_self ContDiffAt.fderiv_right contDiffAt Nat.cast_one WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero Asymptotics.IsBigO.of_norm_left SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass iteratedFDeriv_succ_eq_comp_right LinearIsometryEquiv.dist_map Asymptotics.IsBigO.norm_left isBigO of_order_le
fst 📖	mathematical	—	ContDiffPointwiseHolderAt Prod.normedAddCommGroup Prod.normedSpace Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup	—	ContDiffAt.contDiffPointwiseHolderAt contDiffAt_fst WithTop.coe_lt_top
id 📖	mathematical	—	ContDiffPointwiseHolderAt	—	ContinuousLinearMap.contDiffPointwiseHolderAt
isBigO 📖	mathematical	ContDiffPointwiseHolderAt	Asymptotics.IsBigO ContinuousMultilinearMap Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype Real.norm nhds ContinuousMultilinearMap.instSub Real.instRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup iteratedFDeriv Real.instPow Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Set Set.instMembership unitInterval	—	—
iteratedFDeriv 📖	mathematical	ContDiffPointwiseHolderAt	ContinuousMultilinearMap Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.normedAddCommGroup' Fin.fintype ContinuousMultilinearMap.normedSpace' Real.normedField smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing iteratedFDeriv	—	smulCommClass_self RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul add_zero of_order_le IsTopologicalAddGroup.toContinuousAdd RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul fderiv add_right_comm add_assoc
of_contDiffOn_holderOnWith 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup HolderOnWith ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace ContinuousMultilinearMap.normedAddCommGroup' Fin.fintype Real.instLE Real.instZero Set.instMembership unitInterval Preorder.toLE Real.instPreorder Real.instOne iteratedFDeriv	ContDiffPointwiseHolderAt	—	ContDiffOn.contDiffAt Asymptotics.IsBigO.of_bound SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.mem_of_superset Real.abs_rpow_of_nonneg abs_dist HolderOnWith.dist_le mem_of_mem_nhds
of_exponent_le 📖	—	ContDiffPointwiseHolderAt Set.Elem Real unitInterval Real.instLE Set Set.instMembership	—	—	contDiffAt Asymptotics.IsBigO.trans SeminormedAddCommGroup.toIsTopologicalAddGroup isBigO Asymptotics.IsBigO.comp_tendsto Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le_of_imp le_antisymm le_trans Eq.le tendsto_norm_sub_self_nhdsGE
of_order_le 📖	—	ContDiffPointwiseHolderAt	—	—	of_toLex_le Prod.Lex.toLex_mono le_rfl
of_order_lt 📖	—	ContDiffPointwiseHolderAt	—	—	ContDiffAt.contDiffPointwiseHolderAt contDiffAt WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero
of_toLex_le 📖	—	ContDiffPointwiseHolderAt Lex Set.Elem Real unitInterval Prod.Lex.instLE Real.instLE Set Set.instMembership DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toLex	—	—	Prod.Lex.le_iff of_order_lt of_exponent_le
prodMk 📖	mathematical	ContDiffPointwiseHolderAt	Prod.normedAddCommGroup Prod.normedSpace Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup	—	ContDiffAt.prodMk contDiffAt SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.mp_mem ContDiffAt.eventually Filter.univ_mem' DFunLike.ext iteratedFDeriv_prodMk le_rfl Asymptotics.IsBigO.of_norm_left ContinuousMultilinearMap.opNorm_prod Asymptotics.IsBigO.norm_left Asymptotics.IsBigO.prod_left isBigO
snd 📖	mathematical	—	ContDiffPointwiseHolderAt Prod.normedAddCommGroup Prod.normedSpace Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup	—	ContDiffAt.contDiffPointwiseHolderAt contDiffAt_snd WithTop.coe_lt_top
zero_exponent_iff 📖	mathematical	—	ContDiffPointwiseHolderAt Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing ContDiffAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	Real.instIsOrderedRing contDiffAt SeminormedAddCommGroup.toIsTopologicalAddGroup Real.rpow_zero NormedDivisionRing.to_normOneClass Filter.Tendsto.isBoundedUnder_le BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.Tendsto.norm Filter.Tendsto.sub_const IsTopologicalAddGroup.to_continuousSub ContinuousMultilinearMap.instIsTopologicalAddGroup ContDiffAt.continuousAt_iteratedFDeriv le_rfl
zero_order_iff 📖	mathematical	—	ContDiffPointwiseHolderAt ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop ENat WithTop.zero instZeroENat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instPow Norm.norm Set Set.instMembership unitInterval	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.cast_zero RingHomInvPair.ids UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self DistribMulActionSemiHomClass.toAddMonoidHomClass IsTopologicalAddGroup.toContinuousAdd SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass Asymptotics.isBigO_norm_left LinearIsometryEquiv.norm_map

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffPointwiseHolderAt 📖	mathematical	—	ContDiffPointwiseHolderAt DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike equivLike	—	RingHomInvPair.ids ContinuousLinearMap.contDiffPointwiseHolderAt
contDiffPointwiseHolderAt_left_comp 📖	mathematical	—	ContDiffPointwiseHolderAt DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike equivLike	—	RingHomInvPair.ids symm_apply_apply ContDiffPointwiseHolderAt.continuousLinearMap_comp

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffPointwiseHolderAt 📖	mathematical	—	ContDiffPointwiseHolderAt DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField funLike	—	ContDiffAt.contDiffPointwiseHolderAt ContDiff.contDiffAt contDiff WithTop.coe_lt_top

LinearIsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffPointwiseHolderAt_left_comp 📖	mathematical	—	ContDiffPointwiseHolderAt DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField EquivLike.toFunLike instEquivLike	—	RingHomInvPair.ids ContinuousLinearEquiv.contDiffPointwiseHolderAt_left_comp

(root)

Definitions

Name	Category	Theorems
ContDiffPointwiseHolderAt 📖	CompData	13 math math: ContDiffPointwiseHolderAt.id, ContDiffAt.contDiffPointwiseHolderAt, ContinuousLinearMap.contDiffPointwiseHolderAt, ContDiffPointwiseHolderAt.snd, ContinuousLinearEquiv.contDiffPointwiseHolderAt, contDiffPointwiseHolderAt_iff, LinearIsometryEquiv.contDiffPointwiseHolderAt_left_comp, ContDiffPointwiseHolderAt.of_contDiffOn_holderOnWith, ContDiffPointwiseHolderAt.zero_exponent_iff, ContDiffPointwiseHolderAt.const, ContDiffPointwiseHolderAt.zero_order_iff, ContDiffPointwiseHolderAt.fst, ContinuousLinearEquiv.contDiffPointwiseHolderAt_left_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffPointwiseHolderAt_iff 📖	mathematical	—	ContDiffPointwiseHolderAt ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Asymptotics.IsBigO ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype Real.norm nhds ContinuousMultilinearMap.instSub Real.instRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup iteratedFDeriv Real.instPow Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Set Set.instMembership unitInterval	—	SeminormedAddCommGroup.toIsTopologicalAddGroup

---

← Back to Index