PeriodicCorrector.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The two components of the finite periodic corrector: the explicit solve in span(Y,C), and integration of the covariance correction in its orthogonal complement.

def OAI.ClosedSurfaceR4.PeriodicCorrector.gramDet line 22
def OAI.ClosedSurfaceR4.PeriodicCorrector.spanSolve line 26
Source documentation
The vector in span(Y,C) with prescribed pairings with Y and C.
```
def spanSolve (Y C : E) : (ℝ × ℝ) →L[ℝ] E :=
…
```
lemma OAI.ClosedSurfaceR4.PeriodicCorrector.spanSolve_pairings line 35
lemma OAI.ClosedSurfaceR4.PeriodicCorrector.average_spanSolve line 50
lemma OAI.ClosedSurfaceR4.PeriodicCorrector.average_fluctuation line 70

theorem OAI.ClosedSurfaceR4.PeriodicCorrector.exists_integrated_covariance line 77

Source documentation

A mean-zero prescribed fluctuation is realized by the angular derivative of an actual smooth mean-zero periodic function.

theorem exists_integrated_covariance [FiniteDimensional ℝ E]
    {V : Period → E} (hV : Continuous V) {v : E} (hv : average V = v)
    {r : Period → ℝ} (hr : Continuous r) (hr0 : average r = 0)
    (hVs : ContDiff ℝ ∞ (fun t : ℝ => V (t : Period)))
    (hrs : ContDiff ℝ ∞ (fun t : ℝ => r (t : Period)))
    {q : ℝ} (hq : 0 < q) (hcircle : ∀ t, inner ℝ (V t) (V t) = q) :
    ∃ Z W : Period → E, Continuous Z ∧ Continuous W ∧
      ContDiff ℝ ∞ (fun t : ℝ => Z (t : Period)) ∧
      ContDiff ℝ ∞ (fun t : ℝ => W (t : Period)) ∧
      average Z = 0 ∧ average W = 0 ∧
      (∀ t : ℝ, HasDerivAt (fun s : ℝ => Z (s : Period)) (W (t : Period)) t) ∧
      fluctuation (fun t => inner ℝ (V t) (W t)) = r := by
…

theorem OAI.ClosedSurfaceR4.PeriodicCorrector.slow_pairing_constraint line 97

Source documentation

Differentiating the first pairing gives the second slow constraint used in the triangular system, because Y_y=C.

theorem slow_pairing_constraint {Y U : ℝ → E} {H : ℝ → ℝ}
    {y : ℝ} {C U' : E} {H' j : ℝ}
    (hY : HasDerivAt Y C y) (hU : HasDerivAt U U' y)
    (hH : HasDerivAt H H' y)
    (he : ∀ t, inner ℝ (Y t) (U t) = H t)
    (hC : inner ℝ C (U y) = H' - j) :
    inner ℝ (Y y) U' = j := by
…