LocalFullPeriodicCorrector.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The complete periodic corrector with all hypotheses restricted to an open chart domain.

lemma OAI.ClosedSurfaceR4.PeriodicCorrector.directional_pairing_constraint_on line 19
def OAI.ClosedSurfaceR4.PeriodicCorrector.fullSolutionFormula line 39
Source documentation
The concrete full correction uses the genuine slow derivative of the normalized primitive in its transverse datum.
```
def fullSolutionFormula (v : A) (Y C X₀ : A → E) (V : A → C(Period, E))
    (q : A → ℝ) (h j e : A → C(Period, ℝ)) (z : A × ℝ) : E :=
…
```

theorem OAI.ClosedSurfaceR4.PeriodicCorrector.solve_full_smooth_family_on_formula line 49

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_on_formula (O : Set A) (hO : IsOpen O) (v : A) (S : A → Submodule ℝ E) (Y C X₀ : A → E)
    (hY : ContDiffOn ℝ ∞ Y O) (hC : ContDiffOn ℝ ∞ C O) (hX₀ : ContDiffOn ℝ ∞ X₀ O)
    (hYC : ∀ p ∈ O, fderiv ℝ Y p v = C p)
    (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 j e : A → C(Period, ℝ))
…

Mentions: OAI.ClosedSurfaceR4.PeriodicCorrector.gramDet

theorem OAI.ClosedSurfaceR4.PeriodicCorrector.solve_full_smooth_family_on line 142