FullPeriodicCorrector.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The three equations in the periodic corrector system of paper 094-01, equation (periodic-corrector-system), with smooth dependence on slow parameters.

theorem OAI.ClosedSurfaceR4.PeriodicCorrector.solve_full_smooth_family line 22

Source documentation

A mean-zero, jointly smooth solution of the complete periodic system. The transverse equation follows from differentiating the pairing with Y.

theorem solve_full_smooth_family (v : A) (S : A → Submodule ℝ E) (Y C X₀ : A → E)
    (hY : ContDiff ℝ ∞ Y) (hC : ContDiff ℝ ∞ C) (hX₀ : ContDiff ℝ ∞ X₀)
    (hYC : ∀ p, fderiv ℝ Y p v = C p)
    (hdet : ∀ p, gramDet (Y p) (C p) ≠ 0)
    (hPY : ∀ p w, w ∈ S p → inner ℝ (Y p) w = 0)
    (hPC : ∀ p w, w ∈ S p → inner ℝ (C p) w = 0)
    (hPX : ∀ p w, w ∈ S p → inner ℝ (X₀ p) w = 0)
    (V : A → C(Period, E)) (hVmem : ∀ p t, V p t ∈ S p)
    (hV : ContDiff ℝ ∞ (fun z : A × ℝ => V z.1 (z.2 : Period)))
    (q : A → ℝ) (hq : ContDiff ℝ ∞ q) (hqpos : ∀ p, 0 < q p)
    (hcircle : ∀ p t, inner ℝ (V p t) (V p t) = q p)
    (h j e : A → C(Period, ℝ))
…

Mentions: OAI.ClosedSurfaceR4.PeriodicCorrector.gramDet