CovarianceCorrector.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

The covariance solve in paper 094-01, Section 6, equations covariance-equation and covariance-solve. The averaging operator below is the actual normalized Haar integral on the period circle. The finite linear solve is proved invertible using constant positive speed and connectedness.

abbrev OAI.ClosedSurfaceR4.CovarianceCorrector.Period line 19
def OAI.ClosedSurfaceR4.CovarianceCorrector.average line 24
Source documentation
Normalized average over one period.
```
def average (f : Period → E) : E := ∫ t, f t ∂AddCircle.haarAddCircle
…
```
Mentions: OAI.ClosedSurfaceR4.CovarianceCorrector.Period
lemma OAI.ClosedSurfaceR4.CovarianceCorrector.integrable_of_continuous line 27
lemma OAI.ClosedSurfaceR4.CovarianceCorrector.average_add line 33
lemma OAI.ClosedSurfaceR4.CovarianceCorrector.average_sub line 38
lemma OAI.ClosedSurfaceR4.CovarianceCorrector.average_const line 42
lemma OAI.ClosedSurfaceR4.CovarianceCorrector.average_const_smul line 46
lemma OAI.ClosedSurfaceR4.CovarianceCorrector.average_smul_const line 49
lemma OAI.ClosedSurfaceR4.CovarianceCorrector.average_inner_right line 52
def OAI.ClosedSurfaceR4.CovarianceCorrector.covariance line 65
Source documentation
The covariance operator applied to a vector.
```
def covariance (V : Period → E) (v m : E) : E :=
…
```
Mentions: OAI.ClosedSurfaceR4.CovarianceCorrector.Period
def OAI.ClosedSurfaceR4.CovarianceCorrector.correctedScalar line 68
def OAI.ClosedSurfaceR4.CovarianceCorrector.correctedVector line 72
def OAI.ClosedSurfaceR4.CovarianceCorrector.fluctuation line 76
lemma OAI.ClosedSurfaceR4.CovarianceCorrector.average_centered_inner line 78
lemma OAI.ClosedSurfaceR4.CovarianceCorrector.average_centered_tensor line 85
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.average_correctedScalar line 101
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.average_weighted_correctedScalar line 116
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.average_correctedVector line 140
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.corrected_projection line 154
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.exists_covariance_corrector line 178
Source documentation
The actual periodic covariance equation has a continuous zero-mean solution as soon as the finite-dimensional covariance operator is onto. In the manuscript, positivity of Id - Σ/q supplies precisely this last linear algebra input.
```
theorem exists_covariance_corrector {V : Period → E} (hV : Continuous V)
    {v : E} (hv : average V = v) {r : Period → ℝ} (hr : Continuous r)
    (hr0 : average r = 0) {q : ℝ} (hq : q ≠ 0)
    (hcircle : ∀ t, inner ℝ (V t) (V t) = q)
    (hsurj : Function.Surjective (fun m : E => m - q⁻¹ • covariance V v m)) :
    ∃ W : Period → E, Continuous W ∧ average W = 0 ∧
      fluctuation (fun t => inner ℝ (V t) (W t)) = r := by
…
```
Mentions: OAI.ClosedSurfaceR4.CovarianceCorrector.Period, OAI.ClosedSurfaceR4.CovarianceCorrector.average, OAI.ClosedSurfaceR4.CovarianceCorrector.covariance, OAI.ClosedSurfaceR4.CovarianceCorrector.fluctuation
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.constant_of_constant_square line 195
Source documentation
A continuous scalar function on the period circle cannot switch between the two roots of a fixed square without taking intermediate values.
```
theorem constant_of_constant_square {a : Period → ℝ} (ha : Continuous a)
    (hsq : ∀ t, a t ^ 2 = a 0 ^ 2) : a = fun _ => a 0 := by
…
```
Mentions: OAI.ClosedSurfaceR4.CovarianceCorrector.Period
def OAI.ClosedSurfaceR4.CovarianceCorrector.covarianceLinearMap line 208
Source documentation
The covariance defines a linear operator on the orthogonal complement.
```
def covarianceLinearMap (V : Period → E) (hV : Continuous V) (v : E) : E →ₗ[ℝ] E where
…
```
Mentions: OAI.ClosedSurfaceR4.CovarianceCorrector.Period
def OAI.ClosedSurfaceR4.CovarianceCorrector.meanOperator line 221
lemma OAI.ClosedSurfaceR4.CovarianceCorrector.meanOperator_apply line 225
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.covariance_inner line 229
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.average_centered_square line 238
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.meanOperator_kernel_trivial line 264
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.meanOperator_surjective line 317
theorem OAI.ClosedSurfaceR4.CovarianceCorrector.exists_covariance_corrector_unconditional line 330
Source documentation
The finite covariance solve, with its invertibility now proved from the constant positive speed and connectedness of the periodic parameter space.
```
theorem exists_covariance_corrector_unconditional [FiniteDimensional ℝ E]
    {V : Period → E} (hV : Continuous V) {v : E} (hv : average V = v)
    {r : Period → ℝ} (hr : Continuous r) (hr0 : average r = 0)
    {q : ℝ} (hq : 0 < q) (hcircle : ∀ t, inner ℝ (V t) (V t) = q) :
    ∃ W : Period → E, Continuous W ∧ average W = 0 ∧
      fluctuation (fun t => inner ℝ (V t) (W t)) = r :=
…
```
Mentions: OAI.ClosedSurfaceR4.CovarianceCorrector.Period, OAI.ClosedSurfaceR4.CovarianceCorrector.average, OAI.ClosedSurfaceR4.CovarianceCorrector.fluctuation

theorem OAI.ClosedSurfaceR4.CovarianceCorrector.exists_smooth_covariance_corrector line 342

Source documentation

Smooth periodic input gives a smooth periodic corrector. Smoothness here is stated on the real lift, so no manifold structure on the quotient circle is hidden in the statement.

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

Mentions: OAI.ClosedSurfaceR4.CovarianceCorrector.Period, OAI.ClosedSurfaceR4.CovarianceCorrector.average, OAI.ClosedSurfaceR4.CovarianceCorrector.fluctuation