LocalPeriodicCorrector.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The explicit angular corrector over its open domain of admissibility.

lemma OAI.ClosedSurfaceR4.PeriodicCorrector.contDiffOn_spanSolve line 20

theorem OAI.ClosedSurfaceR4.PeriodicCorrector.solve_smooth_family_on_formula line 37

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_on_formula (O : Set A) (hO : IsOpen O) (S : A → Submodule ℝ E) (Y C X₀ : A → E)
    (hY : ContDiffOn ℝ ∞ Y O) (hC : ContDiffOn ℝ ∞ C O) (hX₀ : ContDiffOn ℝ ∞ X₀ O)
    (hdet : ∀ p ∈ O, gramDet (Y p) (C p) ≠ 0)
    (hPY : ∀ p ∈ O, ∀ w, w ∈ S p → inner ℝ (Y p) w = 0)
    (hPC : ∀ p ∈ O, ∀ w, w ∈ S p → inner ℝ (C p) w = 0)
    (hPX : ∀ p ∈ O, ∀ w, w ∈ S p → inner ℝ (X₀ p) w = 0)
    (V : A → C(Period, E)) (hVmem : ∀ p ∈ O, ∀ t, V p t ∈ S p)
    (hV : ContDiffOn ℝ ∞ (fun z : A × ℝ => V z.1 (z.2 : Period)) (O ×ˢ Set.univ))
    (q : A → ℝ) (hq : ContDiffOn ℝ ∞ q O) (hqpos : ∀ p ∈ O, 0 < q p)
    (hcircle : ∀ p ∈ O, ∀ t, inner ℝ (V p t) (V p t) = q p)
    (h K e : A → C(Period, ℝ))
    (hhs : ContDiffOn ℝ ∞ (fun z : A × ℝ => h z.1 (z.2 : Period)) (O ×ˢ Set.univ))
…

Mentions: OAI.ClosedSurfaceR4.PeriodicCorrector.gramDet

theorem OAI.ClosedSurfaceR4.PeriodicCorrector.solve_smooth_family_on line 221