Covariance of actual finite real harmonic fields

Angular integration is evaluated exactly before applying the weighted product estimates. Real projection includes both conjugate harmonics. The constants are uniform over a fixed bound on the harmonic index.

theorem NavierStokes.HarmonicCovariance.angularProduct_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β : ℝ} (a b : ℕ → HarmonicFields.Coefficients D) (F : Finset ℤ) (hF : ∀ (n : ℕ), (a n).support ⊆ F) (ha : ∀ j ∈ F, WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => (a n).coeff j x) (hb : ∀ j ∈ F, WeightedClasses.WaveClass s P β fun (n : ℕ) (x : D) => (b n).coeff (-j) x) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (k : ℕ → ℝ) (phase : ℕ → D → ℝ) (kp : ℕ → ℤ) (hkp : ∀ (n : ℕ), kp n ≠ 0) : WeightedClasses.MeanClass s (α + β) fun (n : ℕ) (x : D) => HarmonicFields.angularMean fun (θ : ℝ) => HarmonicFields.field (a n) (k n) (phase n) (kp n) (x, θ) * HarmonicFields.field (b n) (k n) (phase n) (kp n) (x, θ)

The zero harmonic of a genuine finite harmonic product has the sum of its input orders. A common finite set, rather than a support cardinality bound, makes the estimate uniform in the band.

theorem NavierStokes.HarmonicCovariance.realCoefficients_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} (a : ℕ → HarmonicFields.Coefficients D) (ha : ∀ (j : ℤ), WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => (a n).coeff j x) (j : ℤ) : WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => (HarmonicResidual.realCoefficients (a n)).coeff j x

theorem NavierStokes.HarmonicCovariance.realAngularProduct_eq {D : Type} (a b : HarmonicFields.Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (x : D) : (HarmonicResidual.realAngularMean fun (θ : ℝ) => (HarmonicFields.field a k Φ kp (x, θ)).re * (HarmonicFields.field b k Φ kp (x, θ)).re) = (HarmonicFields.angularMean fun (θ : ℝ) => HarmonicFields.field (HarmonicResidual.realCoefficients a) k Φ kp (x, θ) * HarmonicFields.field (HarmonicResidual.realCoefficients b) k Φ kp (x, θ)).re

theorem NavierStokes.HarmonicCovariance.realAngularProduct_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β : ℝ} (a b : ℕ → HarmonicFields.Coefficients D) (N : ℕ) (hband : ∀ (n : ℕ), HarmonicFields.BandLimited (a n) N) (ha : ∀ (j : ℤ), WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => (a n).coeff j x) (hb : ∀ (j : ℤ), WeightedClasses.WaveClass s P β fun (n : ℕ) (x : D) => (b n).coeff j x) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (hkp : ∀ (n : ℕ), kp n ≠ 0) : WeightedClasses.MeanClass s (α + β) (CorrectionState.angularAverage fun (n : ℕ) (p : D × ℝ) => (HarmonicFields.field (a n) (k n) (Φ n) (kp n) p).re * (HarmonicFields.field (b n) (k n) (Φ n) (kp n) p).re)

Real angular covariance is estimated from the actual conjugate-pair coefficients. The harmonic bound is on the index, uniformly in the band.

theorem NavierStokes.HarmonicCovariance.blockCovariance_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} (b : CorrectionState.HarmonicBlock D) (N : ℕ) (hband : b.BandLimited N) (hcoef : ∀ (i : Fin 3) (j : ℤ), WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => (b.velocity n i).coeff j x) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (hkp : ∀ (n : ℕ), b.angularFrequency n ≠ 0) (i j : Fin 3) : WeightedClasses.MeanClass s (α + α) (CorrectionState.bilinearCovariance b.oscillation b.oscillation i j)

theorem NavierStokes.HarmonicCovariance.mixedBlockCovariance_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β : ℝ} (a b : CorrectionState.HarmonicBlock D) (N : ℕ) (hband : a.BandLimited N) (hfreq : b.frequency = a.frequency) (hphase : b.phase = a.phase) (hangular : b.angularFrequency = a.angularFrequency) (ha : ∀ (i : Fin 3) (j : ℤ), WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => (a.velocity n i).coeff j x) (hb : ∀ (i : Fin 3) (j : ℤ), WeightedClasses.WaveClass s P β fun (n : ℕ) (x : D) => (b.velocity n i).coeff j x) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (hkp : ∀ (n : ℕ), a.angularFrequency n ≠ 0) (i j : Fin 3) : WeightedClasses.MeanClass s (α + β) (CorrectionState.bilinearCovariance a.oscillation b.oscillation i j)

theorem NavierStokes.HarmonicCovariance.angularAverage_add {D : Type} {f g : CorrectionState.OscillatoryScalar D} (hf : ∀ (n : ℕ) (x : D), Continuous fun (θ : ℝ) => f n (x, θ)) (hg : ∀ (n : ℕ) (x : D), Continuous fun (θ : ℝ) => g n (x, θ)) : CorrectionState.angularAverage (f + g) = CorrectionState.angularAverage f + CorrectionState.angularAverage g

theorem NavierStokes.HarmonicCovariance.angularProduct_add_error {D : Type} (A B C E : CorrectionState.OscillatoryScalar D) (hA : ∀ (n : ℕ) (x : D), Continuous fun (θ : ℝ) => A n (x, θ)) (hB : ∀ (n : ℕ) (x : D), Continuous fun (θ : ℝ) => B n (x, θ)) (hC : ∀ (n : ℕ) (x : D), Continuous fun (θ : ℝ) => C n (x, θ)) (hE : ∀ (n : ℕ) (x : D), Continuous fun (θ : ℝ) => E n (x, θ)) : CorrectionState.angularAverage ((A + C) * (B + E)) - CorrectionState.angularAverage (A * B) = CorrectionState.angularAverage (A * E) + CorrectionState.angularAverage (C * B) + CorrectionState.angularAverage (C * E)

theorem NavierStokes.HarmonicCovariance.realAngularProduct_curl_error_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {κ : ℝ} (hκ : κ ≤ 1 / 2) (a b da db : ℕ → HarmonicFields.Coefficients D) (N : ℕ) (hband : ∀ (n : ℕ), HarmonicFields.BandLimited (a n) N) (hdband : ∀ (n : ℕ), HarmonicFields.BandLimited (da n) N) (ha : ∀ (j : ℤ), WeightedClasses.WaveClass s P (1 / 2) fun (n : ℕ) (x : D) => (a n).coeff j x) (hb : ∀ (j : ℤ), WeightedClasses.WaveClass s P (1 / 2) fun (n : ℕ) (x : D) => (b n).coeff j x) (hda : ∀ (j : ℤ), WeightedClasses.WaveClass s P (1 - κ) fun (n : ℕ) (x : D) => (da n).coeff j x) (hdb : ∀ (j : ℤ), WeightedClasses.WaveClass s P (1 - κ) fun (n : ℕ) (x : D) => (db n).coeff j x) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (hkp : ∀ (n : ℕ), kp n ≠ 0) : WeightedClasses.MeanClass s (3 / 2 - κ) ((CorrectionState.angularAverage fun (n : ℕ) (p : D × ℝ) => (HarmonicFields.field (a n + da n) (k n) (Φ n) (kp n) p).re * (HarmonicFields.field (b n + db n) (k n) (Φ n) (kp n) p).re) - CorrectionState.angularAverage fun (n : ℕ) (p : D × ℝ) => (HarmonicFields.field (a n) (k n) (Φ n) (kp n) p).re * (HarmonicFields.field (b n) (k n) (Φ n) (kp n) p).re)

The error in the actual angular covariance has order 1.5-κ: the two primary-curl products and the curl-curl product are all retained.