WithLp

📁 Source: Mathlib/Analysis/Calculus/FDeriv/WithLp.lean

Statistics

Metric	Count
Definitions	0
Theorems hasFDerivAt_apply, hasFDerivAt_ofLp, hasFDerivAt_toLp, hasStrictFDerivAt_apply, hasStrictFDerivAt_ofLp, hasStrictFDerivAt_toLp, differentiableAt_piLp, differentiableOn_piLp, differentiableWithinAt_piLp, differentiable_piLp, hasFDerivWithinAt_piLp, hasStrictFDerivAt_piLp	12
Total	12

PiLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFDerivAt_apply 📖	mathematical	—	HasFDerivAt PiLp WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Pi.module AddCommGroup.toAddCommMonoid NormedSpace.toModule topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace WithLp.ofLp proj	—	HasStrictFDerivAt.hasFDerivAt hasStrictFDerivAt_apply
hasFDerivAt_ofLp 📖	mathematical	—	HasFDerivAt WithLp WithLp.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup Pi.module AddCommGroup.toAddCommMonoid NormedSpace.toModule topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.topologicalSpace WithLp.ofLp ContinuousLinearEquiv.toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp Pi.addCommMonoid continuousLinearEquiv	—	HasStrictFDerivAt.hasFDerivAt RingHomInvPair.ids hasStrictFDerivAt_ofLp
hasFDerivAt_toLp 📖	mathematical	—	HasFDerivAt Pi.addCommGroup NormedAddCommGroup.toAddCommGroup Pi.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace WithLp WithLp.instAddCommGroup WithLp.instModule topologicalSpace WithLp.toLp ContinuousLinearEquiv.toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid PiLp ContinuousLinearEquiv.symm continuousLinearEquiv	—	HasStrictFDerivAt.hasFDerivAt RingHomInvPair.ids hasStrictFDerivAt_toLp
hasStrictFDerivAt_apply 📖	mathematical	—	HasStrictFDerivAt PiLp WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Pi.module AddCommGroup.toAddCommMonoid NormedSpace.toModule topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace WithLp.ofLp proj	—	HasStrictFDerivAt.comp RingHomInvPair.ids hasStrictFDerivAt_apply hasStrictFDerivAt_ofLp
hasStrictFDerivAt_ofLp 📖	mathematical	—	HasStrictFDerivAt WithLp WithLp.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup Pi.module AddCommGroup.toAddCommMonoid NormedSpace.toModule topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.topologicalSpace WithLp.ofLp ContinuousLinearEquiv.toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp Pi.addCommMonoid continuousLinearEquiv	—	HasStrictFDerivAt.of_isLittleO RingHomInvPair.ids Asymptotics.IsLittleO.congr_left Asymptotics.isLittleO_zero sub_self
hasStrictFDerivAt_toLp 📖	mathematical	—	HasStrictFDerivAt Pi.addCommGroup NormedAddCommGroup.toAddCommGroup Pi.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace WithLp WithLp.instAddCommGroup WithLp.instModule topologicalSpace WithLp.toLp ContinuousLinearEquiv.toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid PiLp ContinuousLinearEquiv.symm continuousLinearEquiv	—	HasStrictFDerivAt.of_isLittleO RingHomInvPair.ids Asymptotics.IsLittleO.congr_left Asymptotics.isLittleO_zero sub_self

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt_piLp 📖	mathematical	—	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PiLp WithLp.instAddCommGroup Pi.addCommGroup WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Pi.module ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.topologicalSpace WithLp.ofLp	—	RingHomInvPair.ids ContinuousLinearEquiv.comp_differentiableAt_iff differentiableAt_pi
differentiableOn_piLp 📖	mathematical	—	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PiLp WithLp.instAddCommGroup Pi.addCommGroup WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Pi.module ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.topologicalSpace WithLp.ofLp	—	RingHomInvPair.ids ContinuousLinearEquiv.comp_differentiableOn_iff differentiableOn_pi
differentiableWithinAt_piLp 📖	mathematical	—	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PiLp WithLp.instAddCommGroup Pi.addCommGroup WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Pi.module ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.topologicalSpace WithLp.ofLp	—	RingHomInvPair.ids ContinuousLinearEquiv.comp_differentiableWithinAt_iff differentiableWithinAt_pi
differentiable_piLp 📖	mathematical	—	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PiLp WithLp.instAddCommGroup Pi.addCommGroup WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Pi.module ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.topologicalSpace WithLp.ofLp	—	RingHomInvPair.ids ContinuousLinearEquiv.comp_differentiable_iff differentiable_pi
hasFDerivWithinAt_piLp 📖	mathematical	—	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PiLp WithLp.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Pi.module ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.topologicalSpace WithLp.ofLp ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid RingHomCompTriple.ids PiLp.proj	—	RingHomCompTriple.ids RingHomInvPair.ids ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff hasFDerivWithinAt_pi'
hasStrictFDerivAt_piLp 📖	mathematical	—	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PiLp WithLp.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Pi.module ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.topologicalSpace WithLp.ofLp ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid RingHomCompTriple.ids PiLp.proj	—	RingHomCompTriple.ids RingHomInvPair.ids ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff hasStrictFDerivAt_pi'

---

← Back to Index