Cartan's formula to The relative Poincaré lemma

TheoremCartan's formula#

Cartan's formula within a set, L_V ω = ι_V dω + d (ι_V ω), where the interior product ι_V inserts V into the first slot.

TauCeti.lieDerivFormWithin_eq_curryLeft_extDerivWithin_add.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {s : Set E} {x : E}
  {ω : E → E [⋀^Fin (k + 1)]→L[𝕜] F} (hω : DifferentiableWithinAt 𝕜 ω s x)
  (hV : DifferentiableWithinAt 𝕜 V s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
  TauCeti.lieDerivFormWithin V ω s x =
    (extDerivWithin ω s x).curryLeft (V x) + extDerivWithin (fun y => (ω y).curryLeft (V y)) s x

Lean

Formalized in Tau Ceti as TauCeti.lieDerivFormWithin_eq_curryLeft_extDerivWithin_add.

Other forms

Cartan's formula. Formalized in Tau Ceti as TauCeti.lieDerivForm_eq_curryLeft_extDeriv_add.

TauCeti.lieDerivForm_eq_curryLeft_extDeriv_add.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {x : E}
  {ω : E → E [⋀^Fin (k + 1)]→L[𝕜] F} (hω : DifferentiableAt 𝕜 ω x) (hV : DifferentiableAt 𝕜 V x) :
  TauCeti.lieDerivForm V ω x =
    (extDeriv ω x).curryLeft (V x) + extDeriv (fun y => (ω y).curryLeft (V y)) x

Sources

• Tau Ceti documentation: TauCeti.lieDerivFormWithin_eq_curryLeft_extDerivWithin_add
• Source of TauCeti.lieDerivFormWithin_eq_curryLeft_extDerivWithin_add in TauCeti/Analysis/Calculus/DifferentialForm/LieDeriv.lean

LeanTauCeti.lieDerivFormWithin_eq_curryLeft_extDerivWithin_add · TauCeti.lieDerivForm_eq_curryLeft_extDeriv_add

Used by 2

Used byMoser's identity · Cartan's magic formula

TheoremDuhamel's formula at a small parameter#

For a parameter s₀ of norm less than 1, the derivative of the perturbed flow of f at (x, s₀) in a parameter direction e is -Dφ_T(x) ∫₀ᵀ Dφ_{-σ}(φ_σ x) (∑ᵢ eᵢ ∇hᵢ(φ_σ x)) dσ, where φ is now the negative-gradient flow of the perturbation f_{s₀}.

TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral_of_norm_lt.{u_1, u_2} {E : Type u_1}
  {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι]
  {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f)
  (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i))
  (hc : ∀ (i : ι), HasCompactSupport (h i)) {s₀ : EuclideanSpace ℝ ι} (hs₀ : ‖s₀‖ < 1) {K' : NNReal}
  (hf' : LipschitzWith K' (gradient (TauCeti.perturb f h s₀))) (x : E) (e : EuclideanSpace ℝ ι)
  (T : ℝ) :
  ((fderiv ℝ ((TauCeti.perturbedFlow f h hf hh hc).toFun T) (x, s₀)) (0, e)).1 =
    -(fderiv ℝ ((TauCeti.negativeGradientFlow (TauCeti.perturb f h s₀) hf').toFun T) x)
        (∫ (σ : ℝ) in 0..T,
          (fderiv ℝ ((TauCeti.negativeGradientFlow (TauCeti.perturb f h s₀) hf').toFun (-σ))
              ((TauCeti.negativeGradientFlow (TauCeti.perturb f h s₀) hf').toFun σ x))
            (∑ i,
              e.ofLp i •
                gradient (h i)
                  ((TauCeti.negativeGradientFlow (TauCeti.perturb f h s₀) hf').toFun σ x)))

Lean

Formalized in Tau Ceti as TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral_of_norm_lt.

Other forms

Duhamel's formula for the parameter variation. Formalized in Tau Ceti as TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral.

TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral.{u_1, u_2} {E : Type u_1} {ι : Type u_2}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ}
  {h : ι → E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f))
  (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) (x : E)
  (e : EuclideanSpace ℝ ι) (T : ℝ) :
  ((fderiv ℝ ((TauCeti.perturbedFlow f h hf hh hc).toFun T) (x, 0)) (0, e)).1 =
    -(fderiv ℝ ((TauCeti.negativeGradientFlow f hf).toFun T) x)
        (∫ (σ : ℝ) in 0..T,
          (fderiv ℝ ((TauCeti.negativeGradientFlow f hf).toFun (-σ))
              ((TauCeti.negativeGradientFlow f hf).toFun σ x))
            (∑ i, e.ofLp i • gradient (h i) ((TauCeti.negativeGradientFlow f hf).toFun σ x)))

Sources

• Tau Ceti documentation: TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral_of_norm_lt
• Source of TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral_of_norm_lt in TauCeti/Analysis/Calculus/Morse/MorseSmale/Perturbation.lean

LeanTauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral_of_norm_lt · TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral

TheoremGreen's theorem on a rectangle#

For a one-form f_s ds + f_t dt that is C¹ over an open neighbourhood of a rectangle [a₁, b₁] × [a₂, b₂], the integral of its exterior derivative ∂_s f_t - ∂_t f_s over the rectangle is its integral over the positively oriented boundary.

TauCeti.integral_fderiv_sub_fderiv_Icc {U : Set (ℝ × ℝ)} {fs ft : ℝ × ℝ → ℝ} {a b : ℝ × ℝ}
  (hU : IsOpen U) (hfs : ContDiffOn ℝ 1 fs U) (hft : ContDiffOn ℝ 1 ft U) (hab : a ≤ b)
  (habU : Set.Icc a b ⊆ U) :
  ∫ (z : ℝ × ℝ) in Set.Icc a b, (fderiv ℝ ft z) (1, 0) - (fderiv ℝ fs z) (0, 1) =
    (((∫ (s : ℝ) in a.1..b.1, fs (s, a.2)) + ∫ (t : ℝ) in a.2..b.2, ft (b.1, t)) -
        ∫ (s : ℝ) in a.1..b.1, fs (s, b.2)) -
      ∫ (t : ℝ) in a.2..b.2, ft (a.1, t)

Lean

Formalized in Tau Ceti as TauCeti.integral_fderiv_sub_fderiv_Icc.

Sources

• Tau Ceti documentation: TauCeti.integral_fderiv_sub_fderiv_Icc
• Source of TauCeti.integral_fderiv_sub_fderiv_Icc in TauCeti/Analysis/Calculus/DifferentialForm/Stokes.lean

LeanTauCeti.integral_fderiv_sub_fderiv_Icc

Used by 1

Used byThe energy identity on a rectangle

TheoremThe inverse function theorem produces a C^n inverse#

If f is C^n on the source of the homeomorphism built by the inverse function theorem, then the inverse is C^n on the target.

HasStrictFDerivAt.contDiffOn_toOpenPartialHomeomorph_symm.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {L : E ≃L[𝕜] F} {a : E}
  {n : WithTop ℕ∞} (hf : HasStrictFDerivAt f (↑L) a)
  (hcont : ContDiffOn 𝕜 n f (HasStrictFDerivAt.toOpenPartialHomeomorph f hf).source) :
  ContDiffOn 𝕜 n (↑(HasStrictFDerivAt.toOpenPartialHomeomorph f hf).symm)
    (HasStrictFDerivAt.toOpenPartialHomeomorph f hf).target

Lean

Formalized in Tau Ceti as HasStrictFDerivAt.contDiffOn_toOpenPartialHomeomorph_symm.

Sources

• Tau Ceti documentation: HasStrictFDerivAt.contDiffOn_toOpenPartialHomeomorph_symm
• Source of HasStrictFDerivAt.contDiffOn_toOpenPartialHomeomorph_symm in TauCeti/Analysis/Calculus/InverseFunctionTheorem.lean

LeanHasStrictFDerivAt.contDiffOn_toOpenPartialHomeomorph_symm

TheoremThe inverse function theorem, with a C^n inverse on the whole target#

A map which is C^n on an open set s, with 1 ≤ n, and whose derivative at a ∈ s is a continuous linear equivalence, coincides on a neighbourhood of a with an OpenPartialHomeomorph whose source is contained in s and whose inverse is C^n on its target.

TauCeti.ContDiffOn.exists_openPartialHomeomorph.{u_1, u_2, u_3} {𝕂 : Type u_1} [RCLike 𝕂]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] [CompleteSpace E] {F : Type u_3}
  [NormedAddCommGroup F] [NormedSpace 𝕂 F] {n : WithTop ℕ∞} {g : E → F} {s : Set E} {a : E}
  (hg : ContDiffOn 𝕂 n g s) (hs : IsOpen s) (ha : a ∈ s) (hn : 1 ≤ n) {e : E ≃L[𝕂] F}
  (he : ↑e = fderiv 𝕂 g a) :
  ∃ Θ, ↑Θ = g ∧ a ∈ Θ.source ∧ Θ.source ⊆ s ∧ ContDiffOn 𝕂 n (↑Θ.symm) Θ.target

Lean

Formalized in Tau Ceti as TauCeti.ContDiffOn.exists_openPartialHomeomorph.

Sources

• Tau Ceti documentation: TauCeti.ContDiffOn.exists_openPartialHomeomorph
• Source of TauCeti.ContDiffOn.exists_openPartialHomeomorph in TauCeti/Analysis/Calculus/InverseFunctionTheorem.lean

LeanTauCeti.ContDiffOn.exists_openPartialHomeomorph

Used by 9

Used byThe parametric Morse lemma, as a local chart · The straightening theorem (flow-box theorem) · Andreotti–Frankel theorem for proper holomorphic immersions · The ambient disc theorem in a manifold · Noncompact Euclidean tubular neighbourhood theorem · The inverse function theorem for manifolds · The local Frobenius theorem (TauCeti.IsInvolutiveDistribution.exists_flatChart) · Smooth Euclidean tubular neighbourhood theorem · Tubular neighbourhood theorem

TheoremIterated Rolle's theorem#

Let F (n + 1) be the derivative of F n for every n < k. Then every finite set Z of zeros of F 0 has at most k more points than some finite set of zeros of F k.

TauCeti.exists_card_le_card_add_of_hasDerivAt {F : ℕ → ℝ → ℝ} {k : ℕ}
  (hF : ∀ n < k, ∀ (x : ℝ), HasDerivAt (F n) (F (n + 1) x) x) {Z : Finset ℝ}
  (hZ : ∀ x ∈ Z, F 0 x = 0) : ∃ Z', (∀ x ∈ Z', F k x = 0) ∧ Z.card ≤ Z'.card + k

Lean

Formalized in Tau Ceti as TauCeti.exists_card_le_card_add_of_hasDerivAt.

Sources

• Tau Ceti documentation: TauCeti.exists_card_le_card_add_of_hasDerivAt
• Source of TauCeti.exists_card_le_card_add_of_hasDerivAt in TauCeti/Analysis/Calculus/LocalExtr/Rolle.lean

LeanTauCeti.exists_card_le_card_add_of_hasDerivAt

Uses 1 · Used by 1

Proof usesRolle's theorem for finitely many zeros

Used byThe Gelfond–Schneider theorem for real numbers (Evertse, Theorem 4.21)

TheoremJacobi's adjugate formula, valid at singular as well as invertible matrices#

Matrix.fderiv_det_apply_adjugate.{u_1, u_2} {n : Type u_1} [Fintype n] [DecidableEq n]
  {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] (A H : Matrix n n 𝕜) :
  (fderiv 𝕜 Matrix.det A) H = (A.adjugate * H).trace

Lean

Formalized in Tau Ceti as Matrix.fderiv_det_apply_adjugate.

Sources

• Tau Ceti documentation: Matrix.fderiv_det_apply_adjugate
• Source of Matrix.fderiv_det_apply_adjugate in TauCeti/Analysis/Calculus/FDeriv/Det.lean

LeanMatrix.fderiv_det_apply_adjugate

Uses 1 · Used by 1

Proof usesJacobi's formula, by rows

Used byJacobi's inverse formula

TheoremJacobi's inverse formula#

At a matrix with invertible determinant, the differential is H ↦ det A * trace (A⁻¹ * H).

Matrix.hasFDerivAt_det.{u_1, u_2} {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2}
  [NontriviallyNormedField 𝕜] {A : Matrix n n 𝕜} (hA : IsUnit A.det) :
  HasFDerivAt Matrix.det
    (A.det •
      { toLinearMap := Matrix.traceLinearMap n 𝕜 𝕜, cont := ⋯ } ∘SL
        (ContinuousLinearMap.mul 𝕜 (Matrix n n 𝕜)) A⁻¹)
    A

Lean

Formalized in Tau Ceti as Matrix.hasFDerivAt_det.

Other forms

Jacobi's inverse formula, evaluated on a direction at an invertible matrix. Formalized in Tau Ceti as Matrix.fderiv_det_apply.

Matrix.fderiv_det_apply.{u_1, u_2} {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2}
  [NontriviallyNormedField 𝕜] {A : Matrix n n 𝕜} (hA : IsUnit A.det) (H : Matrix n n 𝕜) :
  (fderiv 𝕜 Matrix.det A) H = A.det * (A⁻¹ * H).trace

Sources

• Tau Ceti documentation: Matrix.hasFDerivAt_det
• Source of Matrix.hasFDerivAt_det in TauCeti/Analysis/Calculus/FDeriv/Det.lean

LeanMatrix.hasFDerivAt_det · Matrix.fderiv_det_apply

Uses 1 · Used by 1

Proof usesJacobi's adjugate formula, valid at singular as well as invertible matrices

Used byJacobi's formula on a manifold

TheoremThe Lefschetz–Whitehead rank estimate#

Let g and h be differentiable at x, with h x outside the range of the derivative h' of h. If the swept map (y, t) ↦ g y + t • h y has rank at most p at (x, t) for infinitely many t, for instance for every t near 0, then h has rank less than p at x.

HasFDerivAt.finrank_range_lt_of_infinite.{u_1, u_2, u_3} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] {g h : E → F} {g' h' : E →L[𝕜] F} {x : E} [FiniteDimensional 𝕜 F]
  (hh : HasFDerivAt h h' x) (hg : HasFDerivAt g g' x) (hx : h x ∉ (↑h').range) {p : ℕ}
  (hp :
    {t |
        Module.finrank 𝕜 ↥(↑(fderiv 𝕜 (fun q => g q.1 + q.2 • h q.1) (x, t))).range ≤ p}.Infinite) :
  Module.finrank 𝕜 ↥(↑h').range < p

Lean

Formalized in Tau Ceti as HasFDerivAt.finrank_range_lt_of_infinite.

Other forms

The Lefschetz–Whitehead rank estimate for unit directions. Formalized in Tau Ceti as HasFDerivAt.finrank_range_lt_of_infinite_of_norm_eq.

HasFDerivAt.finrank_range_lt_of_infinite_of_norm_eq.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
  [FiniteDimensional ℝ F] {g h : E → F} {g' h' : E →L[ℝ] F} {x : E} (hh : HasFDerivAt h h' x)
  (hg : HasFDerivAt g g' x) (hn : ∀ᶠ (y : E) in nhds x, ‖h y‖ = ‖h x‖) (h0 : h x ≠ 0) {p : ℕ}
  (hp :
    {t |
        Module.finrank ℝ ↥(↑(fderiv ℝ (fun q => g q.1 + q.2 • h q.1) (x, t))).range ≤ p}.Infinite) :
  Module.finrank ℝ ↥(↑h').range < p

Sources

• Tau Ceti documentation: HasFDerivAt.finrank_range_lt_of_infinite
• Source of HasFDerivAt.finrank_range_lt_of_infinite in TauCeti/Analysis/Calculus/FDeriv/RankDrop.lean

LeanHasFDerivAt.finrank_range_lt_of_infinite · HasFDerivAt.finrank_range_lt_of_infinite_of_norm_eq

TheoremThe local Morse lemma#

If g is C^{n+2} on a neighbourhood U of a nondegenerate critical point a, with 1 ≤ n ≤ ∞, there is a chart ψ with source in U, sending a to 0, C^n in both directions, on whose source g is its Hessian quadratic form read in the chart.

TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart_of_contDiffOn.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {g : E → ℝ} {a : E} {U : Set E}
  {n : ℕ∞} (hU : U ∈ nhds a) (hg : ContDiffOn ℝ (↑n + 2) g U)
  (h : TauCeti.IsNondegenerateCriticalPoint g a) (hn : n ≠ 0) :
  ∃ ψ,
    ψ.source ⊆ U ∧
      a ∈ ψ.source ∧
        ↑ψ a = 0 ∧
          ContDiffOn ℝ (↑n) (↑ψ) ψ.source ∧
            ContDiffOn ℝ (↑n) (↑ψ.symm) ψ.target ∧
              ∀ y ∈ ψ.source, g y = g a + 2⁻¹ * ((fderiv ℝ (fderiv ℝ g) a) (↑ψ y)) (↑ψ y)

Lean

Formalized in Tau Ceti as TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart_of_contDiffOn.

Sources

• Tau Ceti documentation: TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart_of_contDiffOn
• Source of TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart_of_contDiffOn in TauCeti/Analysis/Calculus/Morse/LocalNormalForm.lean

LeanTauCeti.IsNondegenerateCriticalPoint.exists_morse_chart_of_contDiffOn

Uses 1 · Used by 1

Proof usesThe Morse lemma

Used byThe Morse lemma on a manifold

TheoremThe Morse form of the convergence theorem#

A negative gradient trajectory confined to a compact set on which fderiv ℝ f is continuous and every critical point of f is nondegenerate converges to a critical point of f in that set.

Nondegeneracy enters only through the finiteness of the critical locus, which is TauCeti.HasNondegenerateCriticalPointsOn.finite_setOfPred_fderiv_eq_zero; the differentiability and the continuity of the gradient are read off the continuity of fderiv ℝ f on K, the gradient being the differential transported by the Riesz isometry.

IsIntegralCurveOn.exists_tendsto_atTop_of_hasNondegenerateCriticalPointsOn.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E}
  {K : Set E} (hγ : IsIntegralCurveOn γ (fun x x_1 => -gradient f x_1) (Set.Ici 0))
  (hK : IsCompact K) (hmaps : Set.MapsTo γ (Set.Ici 0) K) (hdiff : ∀ y ∈ K, DifferentiableAt ℝ f y)
  (hfderiv : ContinuousOn (fderiv ℝ f) K) (hM : TauCeti.HasNondegenerateCriticalPointsOn f K) :
  ∃ p ∈ K, gradient f p = 0 ∧ Filter.Tendsto γ Filter.atTop (nhds p)

Lean

Formalized in Tau Ceti as IsIntegralCurveOn.exists_tendsto_atTop_of_hasNondegenerateCriticalPointsOn.

Sources

• Tau Ceti documentation: IsIntegralCurveOn.exists_tendsto_atTop_of_hasNondegenerateCriticalPointsOn
• Source of IsIntegralCurveOn.exists_tendsto_atTop_of_hasNondegenerateCriticalPointsOn in TauCeti/Analysis/Calculus/Morse/Convergence.lean

LeanIsIntegralCurveOn.exists_tendsto_atTop_of_hasNondegenerateCriticalPointsOn

Used by 1

Used byTauCeti.morseBoundary_comp_morseBoundary_eq_zero_iff

TheoremThe Morse form of Łojasiewicz's gradient inequality#

Near a nondegenerate critical point the absolute energy difference is bounded by a multiple of the squared norm of the gradient; equivalently the Łojasiewicz inequality holds there with exponent 1 / 2. Smoothness alone does not guarantee such an inequality, and a gradient trajectory can spiral forever without converging.

TauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_gradient_sq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E}
  (h : TauCeti.IsNondegenerateCriticalPoint f x) :
  ∃ lam > 0, ∀ᶠ (y : E) in nhds x, lam * |f y - f x| ≤ ‖gradient f y‖ ^ 2

Lean

Formalized in Tau Ceti as TauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_gradient_sq.

Other forms

The Morse form of Łojasiewicz's gradient inequality on a normed space. Formalized in Tau Ceti as TauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_fderiv_sq.

TauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_fderiv_sq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E}
  (h : TauCeti.IsNondegenerateCriticalPoint f x) :
  ∃ lam > 0, ∀ᶠ (y : E) in nhds x, lam * |f y - f x| ≤ ‖fderiv ℝ f y‖ ^ 2

Sources

• Tau Ceti documentation: TauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_gradient_sq
• Source of TauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_gradient_sq in TauCeti/Analysis/Calculus/Morse/Linearization.lean

LeanTauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_gradient_sq · TauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_fderiv_sq

Used by 1

Used byThe Morse form of Łojasiewicz's gradient inequality on a Riemannian manifold

TheoremThe Morse lemma#

Near a nondegenerate critical point x of a C^{n+2} function f, with 1 ≤ n ≤ ∞, there is a C^n map φ, fixing 0 and with derivative the identity there, in terms of which f is exactly its Hessian quadratic form: f (x + v) = f x + 2⁻¹ * fderiv ℝ (fderiv ℝ f) x (φ v) (φ v) for v near 0.

TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart repackages this as a chart at x.

TauCeti.IsNondegenerateCriticalPoint.exists_normal_form.{u} {E : Type u} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {x : E} [CompleteSpace E] {f : E → ℝ} {n : ℕ∞} (hf : ContDiff ℝ (↑n + 2) f)
  (h : TauCeti.IsNondegenerateCriticalPoint f x) (hn : n ≠ 0) :
  ∃ φ U,
    IsOpen U ∧
      0 ∈ U ∧
        φ 0 = 0 ∧
          ContDiffOn ℝ (↑n) φ U ∧
            HasFDerivAt φ (ContinuousLinearMap.id ℝ E) 0 ∧
              ∀ v ∈ U, f (x + v) = f x + 2⁻¹ * ((fderiv ℝ (fderiv ℝ f) x) (φ v)) (φ v)

Lean

Formalized in Tau Ceti as TauCeti.IsNondegenerateCriticalPoint.exists_normal_form.

Other forms

The Morse lemma, as a chart. Formalized in Tau Ceti as TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart.

TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart.{u} {E : Type u} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {x : E} [CompleteSpace E] {f : E → ℝ} {n : ℕ∞} (hf : ContDiff ℝ (↑n + 2) f)
  (h : TauCeti.IsNondegenerateCriticalPoint f x) (hn : n ≠ 0) :
  ∃ ψ,
    x ∈ ψ.source ∧
      ↑ψ x = 0 ∧
        ContDiffOn ℝ (↑n) (↑ψ) ψ.source ∧
          ContDiffOn ℝ (↑n) (↑ψ.symm) ψ.target ∧
            ∀ y ∈ ψ.source, f y = f x + 2⁻¹ * ((fderiv ℝ (fderiv ℝ f) x) (↑ψ y)) (↑ψ y)

Sources

• Tau Ceti documentation: TauCeti.IsNondegenerateCriticalPoint.exists_normal_form
• Source of TauCeti.IsNondegenerateCriticalPoint.exists_normal_form in TauCeti/Analysis/Calculus/Morse/NormalForm.lean

LeanTauCeti.IsNondegenerateCriticalPoint.exists_normal_form · TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart

Uses 1 · Used by 1

Proof usesTaylor's formula to second order

Used byThe local Morse lemma

TheoremMoser's identity#

Let ω₀, ω₁ be forms that are closed along the orbit t ↦ ψₜ x, t ∈ [0, 1], with ω₁ - ω₀ = dα there. If ψₜ moves along a time-dependent field Xₜ with ι_{Xₜ} ((1 - t) • ω₀ + t • ω₁) = -α near the orbit, and the derivative of ψₜ at x solves the variational equation, then ψ₁^* ω₁ = ψ₀^* ω₀ at x.

TauCeti.compContinuousLinearMap_fderiv_eq_of_curryLeft_eq_neg.{u_2, u_3} {E : Type u_2}
  {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  {k : ℕ} {ω₀ ω₁ : E → E [⋀^Fin (k + 1)]→L[ℝ] F} {α : E → E [⋀^Fin k]→L[ℝ] F} {ψ X : ℝ → E → E}
  {x : E} (hω₀ : ∀ t ∈ Set.Icc 0 1, DifferentiableAt ℝ ω₀ (ψ t x))
  (hω₁ : ∀ t ∈ Set.Icc 0 1, DifferentiableAt ℝ ω₁ (ψ t x))
  (hdω₀ : ∀ t ∈ Set.Icc 0 1, extDeriv ω₀ (ψ t x) = 0)
  (hdω₁ : ∀ t ∈ Set.Icc 0 1, extDeriv ω₁ (ψ t x) = 0)
  (hα : ∀ t ∈ Set.Icc 0 1, extDeriv α (ψ t x) = ω₁ (ψ t x) - ω₀ (ψ t x))
  (hX :
    ∀ t ∈ Set.Icc 0 1, (fun y => ((1 - t) • ω₀ y + t • ω₁ y).curryLeft (X t y)) =ᶠ[nhds (ψ t x)] -α)
  (hXd : ∀ t ∈ Set.Icc 0 1, DifferentiableAt ℝ (X t) (ψ t x))
  (hψ : ∀ t ∈ Set.Icc 0 1, HasDerivAt (fun s => ψ s x) (X t (ψ t x)) t)
  (hDψ :
    ∀ t ∈ Set.Icc 0 1,
      HasDerivAt (fun s => fderiv ℝ (ψ s) x) (fderiv ℝ (X t) (ψ t x) ∘SL fderiv ℝ (ψ t) x) t) :
  (ω₁ (ψ 1 x)).compContinuousLinearMap (fderiv ℝ (ψ 1) x) =
    (ω₀ (ψ 0 x)).compContinuousLinearMap (fderiv ℝ (ψ 0) x)

Lean

Formalized in Tau Ceti as TauCeti.compContinuousLinearMap_fderiv_eq_of_curryLeft_eq_neg.

Sources

• Tau Ceti documentation: TauCeti.compContinuousLinearMap_fderiv_eq_of_curryLeft_eq_neg
• Source of TauCeti.compContinuousLinearMap_fderiv_eq_of_curryLeft_eq_neg in TauCeti/Analysis/Calculus/Moser.lean

LeanTauCeti.compContinuousLinearMap_fderiv_eq_of_curryLeft_eq_neg

Uses 1 · Used by 1

Proof usesCartan's formula

Used byMoser's lemma, local form

TheoremNijenhuis–Lie-derivative identity#

if A x squares to -1, then for every differentiable vector field X, the derivative DX(x) cancels out of (L_{A X} A)(x) w - A x ((L_X A)(x) w), leaving the pointwise Nijenhuis expression of A on (X x, w).

TauCeti.lieDerivEndomorphism_apply_sub_apply.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {A : E → E →L[𝕜] E} {x : E}
  {X : E → E} (hA : DifferentiableAt 𝕜 A x) (hX : DifferentiableAt 𝕜 X x)
  (hsq : ∀ (u : E), (A x) ((A x) u) = -u) (w : E) :
  (TauCeti.lieDerivEndomorphism (fun y => (A y) (X y)) A x) w -
      (A x) ((TauCeti.lieDerivEndomorphism X A x) w) =
    ((fderiv 𝕜 A x) ((A x) (X x))) w - ((fderiv 𝕜 A x) ((A x) w)) (X x) +
        (A x) (((fderiv 𝕜 A x) w) (X x)) -
      (A x) (((fderiv 𝕜 A x) (X x)) w)

Lean

Formalized in Tau Ceti as TauCeti.lieDerivEndomorphism_apply_sub_apply.

Sources

• Tau Ceti documentation: TauCeti.lieDerivEndomorphism_apply_sub_apply
• Source of TauCeti.lieDerivEndomorphism_apply_sub_apply in TauCeti/Analysis/Calculus/EndomorphismLieDeriv.lean

LeanTauCeti.lieDerivEndomorphism_apply_sub_apply

Used by 1

Used byRobbin–Salamon Corrigendum Lemma B (on arbitrary real normed spaces under C² regularity)

TheoremThe parametric Morse lemma, as a local chart#

The chart has a product source containing (a, 0), preserves the base parameter in both directions, and fixes the zero section. Its quadratic equation uses the vertical Hessian on that same zero section. The base and the fiber are Banach spaces, so the ordinary inverse function theorem applies to their product.

TauCeti.exists_parametric_morse_chart.{u_1, u_2} {P : Type u_1} {E : Type u_2}
  [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] {f : P × E → ℝ} {a : P} {n : ℕ∞} [CompleteSpace P] (hf : ContDiff ℝ (↑n + 2) f)
  (hcrit : ∀ᶠ (b : P) in nhds a, fderiv ℝ (fun v => f (b, v)) 0 = 0)
  (hH : (fderiv ℝ (fderiv ℝ fun v => f (a, v)) 0).IsInvertible) (hn : n ≠ 0) :
  ∃ ψ U V,
    IsOpen U ∧
      IsOpen V ∧
        a ∈ U ∧
          0 ∈ V ∧
            ψ.source = U ×ˢ V ∧
              (∀ (z : P × E), (↑ψ z).1 = z.1) ∧
                (∀ (b : P), ↑ψ (b, 0) = (b, 0)) ∧
                  (∀ z ∈ ψ.target, (↑ψ.symm z).1 = z.1) ∧
                    ContDiffOn ℝ (↑n) (↑ψ) ψ.source ∧
                      ContDiffOn ℝ (↑n) (↑ψ.symm) ψ.target ∧
                        ∀ z ∈ ψ.source,
                          f z =
                            f (z.1, 0) +
                              2⁻¹ * ((fderiv ℝ (fderiv ℝ fun v => f (z.1, v)) 0) (↑ψ z).2) (↑ψ z).2

Lean

Formalized in Tau Ceti as TauCeti.exists_parametric_morse_chart.

Sources

• Tau Ceti documentation: TauCeti.exists_parametric_morse_chart
• Source of TauCeti.exists_parametric_morse_chart in TauCeti/Analysis/Calculus/Morse/Parametric.lean

LeanTauCeti.exists_parametric_morse_chart

Uses 2

Proof usesThe inverse function theorem, with a C^n inverse on the whole target · Taylor's formula to second order

TheoremPeano's theorem on mixed partial derivatives, differentiating a time derivative in space#

Let u : E → ℝ → F, let s ⊆ ℝ be convex, and let t ∈ s be a point at which derivatives within s are unique. Suppose that near x in space and near t within s, the spatial derivative of u(·, τ) at y is v(y, τ), and that v(y, ·) has time derivative w(y, τ) within s, with w jointly continuous at (x, t). If g y is the time derivative of u(y, ·) within s at t for every y near x, then g is differentiable at x with derivative w(x, t): the spatial derivative of ∂ₜu exists and equals ∂ₜ D_y u.

TauCeti.hasFDerivAt_timeDeriv_of_continuousWithinAt.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {u : E → ℝ → F}
  {v w : E → ℝ → E →L[ℝ] F} {g : E → F} {s : Set ℝ} {x : E} {t : ℝ} (hs : Convex ℝ s) (ht : t ∈ s)
  (hst : UniqueDiffWithinAt ℝ s t)
  (hv : ∀ᶠ (p : E × ℝ) in nhds x ×ˢ nhdsWithin t s, HasFDerivAt (fun x => u x p.2) (v p.1 p.2) p.1)
  (hw : ∀ᶠ (p : E × ℝ) in nhds x ×ˢ nhdsWithin t s, HasDerivWithinAt (v p.1) (w p.1 p.2) s p.2)
  (hwc : ContinuousWithinAt (fun p => w p.1 p.2) (Set.univ ×ˢ s) (x, t))
  (hg : ∀ᶠ (y : E) in nhds x, HasDerivWithinAt (u y) (g y) s t) : HasFDerivAt g (w x t) x

Lean

Formalized in Tau Ceti as TauCeti.hasFDerivAt_timeDeriv_of_continuousWithinAt.

Other forms

Peano's theorem on mixed partial derivatives, differentiating a spatial derivative in time. Formalized in Tau Ceti as TauCeti.hasDerivWithinAt_spatialDeriv_of_continuousWithinAt.

TauCeti.hasDerivWithinAt_spatialDeriv_of_continuousWithinAt.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {u : E → ℝ → F}
  {v : ℝ → E →L[ℝ] F} {g : E → ℝ → F} {w : E → ℝ → E →L[ℝ] F} {s : Set ℝ} {x : E} {t : ℝ}
  (hs : Convex ℝ s) (ht : t ∈ s)
  (hv : ∀ᶠ (τ : ℝ) in nhdsWithin t s, HasFDerivAt (fun x => u x τ) (v τ) x)
  (hg : ∀ᶠ (p : E × ℝ) in nhds x ×ˢ nhdsWithin t s, HasDerivWithinAt (u p.1) (g p.1 p.2) s p.2)
  (hw : ∀ᶠ (p : E × ℝ) in nhds x ×ˢ nhdsWithin t s, HasFDerivAt (fun x => g x p.2) (w p.1 p.2) p.1)
  (hwc : ContinuousWithinAt (fun p => w p.1 p.2) (Set.univ ×ˢ s) (x, t)) :
  HasDerivWithinAt v (w x t) s t

Sources

• Tau Ceti documentation: TauCeti.hasFDerivAt_timeDeriv_of_continuousWithinAt
• Source of TauCeti.hasFDerivAt_timeDeriv_of_continuousWithinAt in TauCeti/Analysis/Calculus/FDeriv/MixedPartial.lean

LeanTauCeti.hasFDerivAt_timeDeriv_of_continuousWithinAt · TauCeti.hasDerivWithinAt_spatialDeriv_of_continuousWithinAt

TheoremThe Poincaré lemma#

A closed C^r form, r ≥ 1, on an open star-convex set is the exterior derivative of a C^r form, which can be chosen to vanish at the centre.

StarConvex.exists_contDiffOn_forall_extDeriv_eq.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E}
  {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} [CompleteSpace F] (hs : StarConvex ℝ x₀ s)
  (hso : IsOpen s) {r : ℕ∞} (hr : 1 ≤ r) (hω : ContDiffOn ℝ (↑r) ω s)
  (hclosed : ∀ y ∈ s, extDeriv ω y = 0) :
  ∃ α, ContDiffOn ℝ (↑r) α s ∧ α x₀ = 0 ∧ ∀ x ∈ s, extDeriv α x = ω x

Lean

Formalized in Tau Ceti as StarConvex.exists_contDiffOn_forall_extDeriv_eq.

Other forms

The Poincaré lemma. Formalized in Tau Ceti as StarConvex.extDeriv_poincareHomotopy.

StarConvex.extDeriv_poincareHomotopy.{u_1, u_2} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E} {s : Set E}
  {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} [CompleteSpace F] (hs : StarConvex ℝ x₀ s) (hso : IsOpen s)
  (hω : ContDiffOn ℝ 1 ω s) (hclosed : ∀ y ∈ s, extDeriv ω y = 0) {x : E} (hx : x ∈ s) :
  extDeriv (TauCeti.poincareHomotopy x₀ ω) x = ω x

The Poincaré lemma for forms invariant under a finite group. Formalized in Tau Ceti as Convex.exists_invariant_contDiffOn_forall_extDerivWithin_eq.

Convex.exists_invariant_contDiffOn_forall_extDerivWithin_eq.{u_1, u_2, u_3} {E : Type u_1}
  {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [CompleteSpace F] {n : ℕ} {G : Type u_3} [Group G] [Finite G] {ρ : ContRepresentation ℝ G E}
  {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} (hs : Convex ℝ s) (hsu : UniqueDiffOn ℝ s)
  (hsne : s.Nonempty) (hρs : ∀ (g : G), Set.MapsTo (⇑(ρ g)) s s) {r : ℕ∞} (hr : 1 ≤ r)
  (hωr : ContDiffOn ℝ (↑r) ω s) (hclosed : ∀ y ∈ s, extDerivWithin ω s y = 0)
  (hω : ∀ (g : G), ∀ y ∈ s, (ω ((ρ g) y)).compContinuousLinearMap (ρ g) = ω y) :
  ∃ α,
    ContDiffOn ℝ (↑r) α s ∧
      (∀ (g : G), ∀ y ∈ s, (α ((ρ g) y)).compContinuousLinearMap (ρ g) = α y) ∧
        ∀ y ∈ s, extDerivWithin α s y = ω y

The Poincaré lemma for invariant forms. Formalized in Tau Ceti as StarConvex.exists_invariant_contDiffOn_forall_extDeriv_eq.

StarConvex.exists_invariant_contDiffOn_forall_extDeriv_eq.{u_1, u_2, u_3} {E : Type u_1}
  {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [CompleteSpace F] {n : ℕ} {x₀ : E} {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} {G : Type u_3}
  [Monoid G] {ρ : ContRepresentation ℝ G E} (hs : StarConvex ℝ x₀ s) (hso : IsOpen s)
  (hρx₀ : ∀ (g : G), (ρ g) x₀ = x₀) (hρs : ∀ (g : G), Set.MapsTo (⇑(ρ g)) s s) {r : ℕ∞} (hr : 1 ≤ r)
  (hωr : ContDiffOn ℝ (↑r) ω s) (hclosed : ∀ y ∈ s, extDeriv ω y = 0)
  (hω : ∀ (g : G), ∀ y ∈ s, (ω ((ρ g) y)).compContinuousLinearMap (ρ g) = ω y) :
  ∃ α,
    ContDiffOn ℝ (↑r) α s ∧
      α x₀ = 0 ∧
        (∀ (g : G), ∀ y ∈ s, (α ((ρ g) y)).compContinuousLinearMap (ρ g) = α y) ∧
          ∀ y ∈ s, extDeriv α y = ω y

Sources

• Tau Ceti documentation: StarConvex.exists_contDiffOn_forall_extDeriv_eq
• Source of StarConvex.exists_contDiffOn_forall_extDeriv_eq in TauCeti/Analysis/Calculus/DifferentialForm/Poincare.lean

LeanStarConvex.exists_contDiffOn_forall_extDeriv_eq · StarConvex.extDeriv_poincareHomotopy · Convex.exists_invariant_contDiffOn_forall_extDerivWithin_eq · StarConvex.exists_invariant_contDiffOn_forall_extDeriv_eq

Uses 1 · Used by 2

Proof usesThe relative Poincaré lemma

Used byDarboux's theorem · The Poincaré lemma on manifolds

TheoremRademacher's theorem for locally Lipschitz functions#

a function between finite-dimensional real normed spaces which is locally Lipschitz on a set is differentiable within that set at almost every point of it.

LocallyLipschitzOn.ae_differentiableWithinAt_of_mem.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {s : Set E}
  [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E → F}
  (hf : LocallyLipschitzOn s f) : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Lean

Formalized in Tau Ceti as LocallyLipschitzOn.ae_differentiableWithinAt_of_mem.

Other forms

Rademacher's theorem for locally Lipschitz functions on an open set. Formalized in Tau Ceti as LocallyLipschitzOn.ae_differentiableAt_of_mem.

LocallyLipschitzOn.ae_differentiableAt_of_mem.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {s : Set E}
  [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E → F}
  (hf : LocallyLipschitzOn s f) (hs : IsOpen s) : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableAt ℝ f x

Sources

• Tau Ceti documentation: LocallyLipschitzOn.ae_differentiableWithinAt_of_mem
• Source of LocallyLipschitzOn.ae_differentiableWithinAt_of_mem in TauCeti/Analysis/Calculus/Rademacher.lean

LeanLocallyLipschitzOn.ae_differentiableWithinAt_of_mem · LocallyLipschitzOn.ae_differentiableAt_of_mem

Used by 14

Used byThe Poincaré–Wirtinger inequality for functions of bounded variation, localized to a subset · The coarea formula for total variation · The sharp BV Sobolev bound · The Sobolev inequality for functions of bounded variation · The Calderón–Zygmund estimate ‖D²u‖_p ≤ C ‖Δu‖_p · The trace operator of a bounded Lipschitz domain · Alexandrov's theorem · Lebesgue decomposition of the Monge–Ampère measure · Rademacher's theorem for extended-real convex functions · The Vitali covering lemma for sections · The Schwarz reflection principle · The interior Schauder estimate on small balls · Extension theorem for bounded Lipschitz domains · McCann's displacement convexity of internal energies

TheoremThe relative Poincaré lemma#

A C^r form, r ≥ 1, closed within a convex set with unique derivatives is the exterior derivative within the set of a C^r form, which can be chosen to vanish at any given point of the set. The set need not be open: a closed half-ball, the image of a boundary chart, is allowed.

Convex.exists_contDiffOn_forall_extDerivWithin_eq.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E}
  {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} [CompleteSpace F] (hs : Convex ℝ s)
  (hsu : UniqueDiffOn ℝ s) (hx₀ : x₀ ∈ s) {r : ℕ∞} (hr : 1 ≤ r) (hω : ContDiffOn ℝ (↑r) ω s)
  (hclosed : ∀ y ∈ s, extDerivWithin ω s y = 0) :
  ∃ α, ContDiffOn ℝ (↑r) α s ∧ α x₀ = 0 ∧ ∀ x ∈ s, extDerivWithin α s x = ω x

Lean

Formalized in Tau Ceti as Convex.exists_contDiffOn_forall_extDerivWithin_eq.

Other forms

The relative Poincaré lemma. Formalized in Tau Ceti as Convex.extDerivWithin_poincareHomotopy.

Convex.extDerivWithin_poincareHomotopy.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E}
  {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} [CompleteSpace F] (hs : Convex ℝ s)
  (hsu : UniqueDiffOn ℝ s) (hx₀ : x₀ ∈ s) (hω : ContDiffOn ℝ 1 ω s)
  (hclosed : ∀ y ∈ s, extDerivWithin ω s y = 0) {x : E} (hx : x ∈ s) :
  extDerivWithin (TauCeti.poincareHomotopy x₀ ω) s x = ω x

The relative Poincaré lemma on an adapted convex neighborhood. Formalized in Tau Ceti as Convex.exists_contDiffOn_relative_primitive.

Convex.exists_contDiffOn_relative_primitive.{u_1, u_2, u_3} {E : Type u_1} {N : Type u_2}
  {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [CompleteSpace F] {s : Set (E × N)}
  (hs : Convex ℝ s) (hso : IsOpen s) {r : ℕ∞} (hr : 1 ≤ r)
  {ω : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F} (hω : ContDiffOn ℝ (↑r) ω s)
  (hscale : ∀ x ∈ s, ∀ t ∈ Set.Icc 0 1, (x.1, t • x.2) ∈ s) (hclosed : ∀ x ∈ s, extDeriv ω x = 0)
  (hzero :
    ∀ (q : E),
      (q, 0) ∈ s → (ω (q, 0)).compContinuousLinearMap (ContinuousLinearMap.inl ℝ E N) = 0) :
  ∃ β, ContDiffOn ℝ (↑r) β s ∧ (∀ (q : E), β (q, 0) = 0) ∧ ∀ x ∈ s, extDeriv β x = ω x

Sources

• Tau Ceti documentation: Convex.exists_contDiffOn_forall_extDerivWithin_eq
• Source of Convex.exists_contDiffOn_forall_extDerivWithin_eq in TauCeti/Analysis/Calculus/DifferentialForm/Poincare.lean

LeanConvex.exists_contDiffOn_forall_extDerivWithin_eq · Convex.extDerivWithin_poincareHomotopy · Convex.exists_contDiffOn_relative_primitive

Used by 3

Used byThe Poincaré lemma · The Poincaré lemma on manifolds · The relative Darboux theorem in adapted coordinates

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.