SmoothPeriodicCorrector.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The periodic corrector constructed smoothly over finite-dimensional families of geometric data.

def OAI.ClosedSurfaceR4.PeriodicCorrector.correctorFamily line 24

theorem OAI.ClosedSurfaceR4.PeriodicCorrector.solve_smooth_family line 35

Source documentation

A smooth family of solutions of the angular equations, with zero mean. The varying subspace is used only for orthogonality and membership; the actual covariance solve takes place in the fixed ambient Euclidean space.

theorem solve_smooth_family (S : A → Submodule ℝ E) (Y C X₀ : A → E)
    (hY : ContDiff ℝ ∞ Y) (hC : ContDiff ℝ ∞ C) (hX₀ : ContDiff ℝ ∞ X₀)
    (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 K e : A → C(Period, ℝ))
    (hhs : ContDiff ℝ ∞ (fun z : A × ℝ => h z.1 (z.2 : Period)))
…

Mentions: OAI.ClosedSurfaceR4.PeriodicCorrector.gramDet