Commit 2025-11-24 23:37 d6b6f42a

View on Github →

feat(Analysis): Poincaré lemma for 1-forms (#24019)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/TangentCone/Basic.lean

added theorem tangentConeAt_of_mem_nhds

Created Mathlib/MeasureTheory/Integral/CurveIntegral/Poincare.lean

added theorem ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_diffContOnCl

added theorem ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt

added theorem ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable

added theorem Convex.curveIntegral_segment_add_eq_of_hasFDerivWithinAt_symmetric

added theorem Convex.exists_forall_hasDerivWithinAt

added theorem Convex.exists_forall_hasFDerivAt_of_fderiv_symmetric

added theorem Convex.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric

added theorem Convex.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric

added theorem Convex.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric