Commit 2024-01-16 21:01 8050708e

View on Github →

refactor(Geometry/Manifold/MFDeriv): split file (#9565) With about 2200 lines, this is the largest file in Geometry/Manifolds.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/Diffeomorph.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve.lean

Created Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean

added theorem ModelWithCorners.hasMFDerivWithinAt_symm

added theorem ModelWithCorners.mdifferentiableOn_symm

added theorem PartialHomeomorph.MDifferentiable.comp_symm_deriv

added theorem PartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot

added theorem PartialHomeomorph.MDifferentiable.mdifferentiableAt_symm

added theorem PartialHomeomorph.MDifferentiable.mfderiv_bijective

added theorem PartialHomeomorph.MDifferentiable.mfderiv_injective

added theorem PartialHomeomorph.MDifferentiable.mfderiv_surjective

added theorem PartialHomeomorph.MDifferentiable.range_mfderiv_eq_top

added theorem PartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ

added theorem PartialHomeomorph.MDifferentiable.symm_comp_deriv

added theorem PartialHomeomorph.MDifferentiable.trans

added theorem hasMFDerivAt_extChartAt

added theorem hasMFDerivWithinAt_extChartAt

added theorem mdifferentiableAt_atlas

added theorem mdifferentiableAt_atlas_symm

added theorem mdifferentiableAt_extChartAt

added theorem mdifferentiableOn_atlas

added theorem mdifferentiableOn_atlas_symm

added theorem mdifferentiableOn_extChartAt

added theorem mdifferentiable_chart

added theorem mdifferentiable_of_mem_atlas

added theorem tangentMap_chart

added theorem tangentMap_chart_symm

Modified Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

deleted theorem ContinuousLinearEquiv.mfderivWithin_eq

deleted theorem ContinuousLinearEquiv.mfderiv_eq

deleted theorem ContinuousLinearMap.mfderivWithin_eq

deleted theorem ContinuousLinearMap.mfderiv_eq

deleted def DifferentiableWithinAtProp

deleted theorem HasMFDerivAt.add

deleted theorem HasMFDerivAt.const_smul

deleted theorem HasMFDerivAt.mul'

deleted theorem HasMFDerivAt.mul

deleted theorem HasMFDerivAt.neg

deleted theorem HasMFDerivAt.sub

deleted def HasMFDerivAt

deleted theorem HasMFDerivWithinAt.mul'

deleted theorem HasMFDerivWithinAt.mul

deleted def HasMFDerivWithinAt

deleted theorem MDifferentiable.add

deleted theorem MDifferentiable.const_smul

deleted theorem MDifferentiable.mul

deleted theorem MDifferentiable.neg

deleted theorem MDifferentiable.sub

deleted def MDifferentiable

deleted theorem MDifferentiableAt.add

deleted theorem MDifferentiableAt.const_smul

deleted theorem MDifferentiableAt.mfderiv_prod

deleted theorem MDifferentiableAt.mul

deleted theorem MDifferentiableAt.neg

deleted theorem MDifferentiableAt.sub

deleted def MDifferentiableAt

deleted theorem MDifferentiableOn.mul

deleted def MDifferentiableOn

deleted theorem MDifferentiableWithinAt.mul

deleted def MDifferentiableWithinAt

deleted theorem ModelWithCorners.hasMFDerivWithinAt_symm

deleted theorem ModelWithCorners.mdifferentiableOn_symm

deleted theorem PartialHomeomorph.MDifferentiable.comp_symm_deriv

deleted theorem PartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot

deleted theorem PartialHomeomorph.MDifferentiable.mdifferentiableAt_symm

deleted theorem PartialHomeomorph.MDifferentiable.mfderiv_bijective

deleted theorem PartialHomeomorph.MDifferentiable.mfderiv_injective

deleted theorem PartialHomeomorph.MDifferentiable.mfderiv_surjective

deleted theorem PartialHomeomorph.MDifferentiable.range_mfderiv_eq_top

deleted theorem PartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ

deleted theorem PartialHomeomorph.MDifferentiable.symm_comp_deriv

deleted theorem PartialHomeomorph.MDifferentiable.trans

deleted def PartialHomeomorph.MDifferentiable

deleted theorem Trivialization.mdifferentiable

deleted theorem UniqueMDiffOn.image_denseRange'

deleted theorem UniqueMDiffOn.image_denseRange

deleted theorem UniqueMDiffOn.smooth_bundle_preimage

deleted theorem UniqueMDiffOn.tangentBundle_proj_preimage

deleted theorem UniqueMDiffOn.uniqueDiffOn_inter_preimage

deleted theorem UniqueMDiffOn.uniqueDiffOn_target_inter

deleted theorem UniqueMDiffOn.uniqueMDiffOn_preimage

deleted def UniqueMDiffOn

deleted theorem UniqueMDiffWithinAt.image_denseRange

deleted theorem UniqueMDiffWithinAt.smooth_bundle_preimage'

deleted theorem UniqueMDiffWithinAt.smooth_bundle_preimage

deleted def UniqueMDiffWithinAt

deleted theorem const_smul_mfderiv

deleted theorem differentiable_within_at_localInvariantProp

deleted theorem hasMFDerivAt_const

deleted theorem hasMFDerivAt_extChartAt

deleted theorem hasMFDerivAt_fst

deleted theorem hasMFDerivAt_id

deleted theorem hasMFDerivAt_iff_hasFDerivAt

deleted theorem hasMFDerivAt_neg

deleted theorem hasMFDerivAt_snd

deleted theorem hasMFDerivWithinAt_const

deleted theorem hasMFDerivWithinAt_extChartAt

deleted theorem hasMFDerivWithinAt_fst

deleted theorem hasMFDerivWithinAt_id

deleted theorem hasMFDerivWithinAt_iff_hasFDerivWithinAt

deleted theorem hasMFDerivWithinAt_snd

deleted theorem mdifferentiableAt_atlas

deleted theorem mdifferentiableAt_atlas_symm

deleted theorem mdifferentiableAt_const

deleted theorem mdifferentiableAt_extChartAt

deleted theorem mdifferentiableAt_fst

deleted theorem mdifferentiableAt_id

deleted theorem mdifferentiableAt_iff_differentiableAt

deleted theorem mdifferentiableAt_iff_liftPropAt

deleted theorem mdifferentiableAt_neg

deleted theorem mdifferentiableAt_snd

deleted theorem mdifferentiableOn_atlas

deleted theorem mdifferentiableOn_atlas_symm

deleted theorem mdifferentiableOn_const

deleted theorem mdifferentiableOn_extChartAt

deleted theorem mdifferentiableOn_fst

deleted theorem mdifferentiableOn_id

deleted theorem mdifferentiableOn_iff_differentiableOn

deleted theorem mdifferentiableOn_snd

deleted theorem mdifferentiableWithinAt_const

deleted theorem mdifferentiableWithinAt_fst

deleted theorem mdifferentiableWithinAt_id

deleted theorem mdifferentiableWithinAt_iff_differentiableWithinAt

deleted theorem mdifferentiableWithinAt_iff_liftPropWithinAt

deleted theorem mdifferentiableWithinAt_snd

deleted theorem mdifferentiable_chart

deleted theorem mdifferentiable_const

deleted theorem mdifferentiable_fst

deleted theorem mdifferentiable_id

deleted theorem mdifferentiable_iff_differentiable

deleted theorem mdifferentiable_of_mem_atlas

deleted theorem mdifferentiable_snd

deleted def mfderiv

deleted def mfderivWithin

deleted theorem mfderivWithin_const

deleted theorem mfderivWithin_eq_fderivWithin

deleted theorem mfderivWithin_fst

deleted theorem mfderivWithin_id

deleted theorem mfderivWithin_snd

deleted theorem mfderiv_add

deleted theorem mfderiv_const

deleted theorem mfderiv_eq_fderiv

deleted theorem mfderiv_fst

deleted theorem mfderiv_id

deleted theorem mfderiv_neg

deleted theorem mfderiv_prod_eq_add

deleted theorem mfderiv_prod_left

deleted theorem mfderiv_prod_right

deleted theorem mfderiv_snd

deleted theorem mfderiv_sub

deleted def tangentMap

deleted def tangentMapWithin

deleted theorem tangentMapWithin_id

deleted theorem tangentMapWithin_prod_fst

deleted theorem tangentMapWithin_prod_snd

deleted theorem tangentMap_chart

deleted theorem tangentMap_chart_symm

deleted theorem tangentMap_id

deleted theorem tangentMap_prod_fst

deleted theorem tangentMap_prod_snd

deleted theorem uniqueMDiffOn_iff_uniqueDiffOn

deleted theorem uniqueMDiffWithinAt_iff_uniqueDiffWithinAt

deleted theorem writtenInExtChartAt_model_space

Created Mathlib/Geometry/Manifold/MFDeriv/Defs.lean

added def DifferentiableWithinAtProp

added def HasMFDerivAt

added def HasMFDerivWithinAt

added def MDifferentiable

added def MDifferentiableAt

added def MDifferentiableOn

added def MDifferentiableWithinAt

added def PartialHomeomorph.MDifferentiable

added def UniqueMDiffOn

added def UniqueMDiffWithinAt

added theorem differentiable_within_at_localInvariantProp

added theorem mdifferentiableAt_iff_liftPropAt

added theorem mdifferentiableWithinAt_iff_liftPropWithinAt

added def mfderiv

added def mfderivWithin

added def tangentMap

added def tangentMapWithin

Created Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean

added theorem hasMFDerivAt_iff_hasFDerivAt

added theorem hasMFDerivWithinAt_iff_hasFDerivWithinAt

added theorem mdifferentiableAt_iff_differentiableAt

added theorem mdifferentiableOn_iff_differentiableOn

added theorem mdifferentiableWithinAt_iff_differentiableWithinAt

added theorem mdifferentiable_iff_differentiable

added theorem mfderivWithin_eq_fderivWithin

added theorem mfderiv_eq_fderiv

added theorem uniqueMDiffOn_iff_uniqueDiffOn

added theorem uniqueMDiffWithinAt_iff_uniqueDiffWithinAt

added theorem writtenInExtChartAt_model_space

Created Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

added theorem ContinuousLinearEquiv.mfderivWithin_eq

added theorem ContinuousLinearEquiv.mfderiv_eq

added theorem ContinuousLinearMap.mfderivWithin_eq

added theorem ContinuousLinearMap.mfderiv_eq

added theorem HasMFDerivAt.add

added theorem HasMFDerivAt.const_smul

added theorem HasMFDerivAt.mul'

added theorem HasMFDerivAt.mul

added theorem HasMFDerivAt.neg

added theorem HasMFDerivAt.sub

added theorem HasMFDerivWithinAt.mul'

added theorem HasMFDerivWithinAt.mul

added theorem MDifferentiable.add

added theorem MDifferentiable.const_smul

added theorem MDifferentiable.mul

added theorem MDifferentiable.neg

added theorem MDifferentiable.sub

added theorem MDifferentiableAt.add

added theorem MDifferentiableAt.const_smul

added theorem MDifferentiableAt.mfderiv_prod

added theorem MDifferentiableAt.mul

added theorem MDifferentiableAt.neg

added theorem MDifferentiableAt.sub

added theorem MDifferentiableOn.mul

added theorem MDifferentiableWithinAt.mul

added theorem const_smul_mfderiv

added theorem hasMFDerivAt_const

added theorem hasMFDerivAt_fst

added theorem hasMFDerivAt_id

added theorem hasMFDerivAt_neg

added theorem hasMFDerivAt_snd

added theorem hasMFDerivWithinAt_const

added theorem hasMFDerivWithinAt_fst

added theorem hasMFDerivWithinAt_id

added theorem hasMFDerivWithinAt_snd

added theorem mdifferentiableAt_const

added theorem mdifferentiableAt_fst

added theorem mdifferentiableAt_id

added theorem mdifferentiableAt_neg

added theorem mdifferentiableAt_snd

added theorem mdifferentiableOn_const

added theorem mdifferentiableOn_fst

added theorem mdifferentiableOn_id

added theorem mdifferentiableOn_snd

added theorem mdifferentiableWithinAt_const

added theorem mdifferentiableWithinAt_fst

added theorem mdifferentiableWithinAt_id

added theorem mdifferentiableWithinAt_snd

added theorem mdifferentiable_const

added theorem mdifferentiable_fst

added theorem mdifferentiable_id

added theorem mdifferentiable_snd

added theorem mfderivWithin_const

added theorem mfderivWithin_fst

added theorem mfderivWithin_id

added theorem mfderivWithin_snd

added theorem mfderiv_add

added theorem mfderiv_const

added theorem mfderiv_fst

added theorem mfderiv_id

added theorem mfderiv_neg

added theorem mfderiv_prod_eq_add

added theorem mfderiv_prod_left

added theorem mfderiv_prod_right

added theorem mfderiv_snd

added theorem mfderiv_sub

added theorem tangentMapWithin_id

added theorem tangentMapWithin_prod_fst

added theorem tangentMapWithin_prod_snd

added theorem tangentMap_id

added theorem tangentMap_prod_fst

added theorem tangentMap_prod_snd

Created Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean

added theorem Trivialization.mdifferentiable

added theorem UniqueMDiffOn.image_denseRange'

added theorem UniqueMDiffOn.image_denseRange

added theorem UniqueMDiffOn.smooth_bundle_preimage

added theorem UniqueMDiffOn.tangentBundle_proj_preimage

added theorem UniqueMDiffOn.uniqueDiffOn_inter_preimage

added theorem UniqueMDiffOn.uniqueDiffOn_target_inter

added theorem UniqueMDiffOn.uniqueMDiffOn_preimage

added theorem UniqueMDiffWithinAt.image_denseRange

added theorem UniqueMDiffWithinAt.smooth_bundle_preimage'

added theorem UniqueMDiffWithinAt.smooth_bundle_preimage

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/Manifold.lean