OAI/Geometry/SurfaceImmersion/Correction/PeriodicCorrectorSystem.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.PeriodicCorrector.solve_system line 19

   Source documentation

   Solve the two angular equations and the prescribed C pairing. The slow Y equation follows by slow_pairing_constraint when K=H_y-j.

   theorem solve_system (P : Submodule ℝ E) (Y C X₀ : E)
       (hD : gramDet Y C ≠ 0)
       (hPY : ∀ w : P, inner ℝ Y (w : E) = 0)
       (hPC : ∀ w : P, inner ℝ C (w : E) = 0)
       (hPX : ∀ w : P, inner ℝ X₀ (w : E) = 0)
       {V : Period → P} (hV : Continuous V) {v : P} (hv : average V = v)
       (hVs : ContDiff ℝ ∞ (fun t : ℝ => V (t : Period)))
       {q : ℝ} (hq : 0 < q) (hcircle : ∀ t, inner ℝ (V t) (V t) = q)
       {H K h k' e : Period → ℝ}
       (hH : Continuous H) (hK : Continuous K) (hh : Continuous h)
       (hk' : Continuous k') (he : Continuous e)
       (hHs : ContDiff ℝ ∞ (fun t : ℝ => H (t : Period)))
   …

   Mentions: OAI.ClosedSurfaceR4.PeriodicCorrector.gramDet

2. theorem OAI.ClosedSurfaceR4.PeriodicCorrector.solve_angular_corrector line 113

   Source documentation

   The angular correction exists for arbitrary smooth mean-zero data. The primitive and derivative data used internally are constructed on the circle.

   theorem solve_angular_corrector (P : Submodule ℝ E) (Y C X₀ : E)
       (hdet : gramDet Y C ≠ 0)
       (hPY : ∀ w : P, inner ℝ Y (w : E) = 0)
       (hPC : ∀ w : P, inner ℝ C (w : E) = 0)
       (hPX : ∀ w : P, inner ℝ X₀ (w : E) = 0)
       {V : Period → P} (hV : Continuous V) {v : P} (hv : average V = v)
       (hVs : ContDiff ℝ ∞ (fun t : ℝ => V (t : Period)))
       {q : ℝ} (hq : 0 < q) (hcircle : ∀ t, inner ℝ (V t) (V t) = q)
       {h K e : Period → ℝ} (hh : Continuous h) (hK : Continuous K)
       (he : Continuous e)
       (hhs : ContDiff ℝ ∞ (fun t : ℝ => h (t : Period)))
       (hKs : ContDiff ℝ ∞ (fun t : ℝ => K (t : Period)))
   …

   Mentions: OAI.ClosedSurfaceR4.PeriodicCorrector.gramDet