Mean interactions from support-local phase estimates #
The phase normal is estimated only on the genuine native phase patch. Outside that patch the wave coefficients have zero germs, which force the actual mean interaction to have a zero germ as well.
@[reducible, inline]
abbrev
NavierStokes.LocalizedMeanInteraction.LocalMean
{D : Type}
{I : Type u_1}
{E : Type u_2}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData D)
(C : ℕ → I → Set D)
(α : ℝ)
(f : ℕ → I → D → E)
:
Local mean: an abbreviation for LocalClass s C (fun _ _ x => s.zeta x) α f.
Equations
- NavierStokes.LocalizedMeanInteraction.LocalMean s C α f = NavierStokes.LocalizedWaveBounds.LocalClass s C (fun (x : ℕ) (x_1 : I) (x_2 : D) => s.zeta x_2) α f
Instances For
noncomputable def
NavierStokes.LocalizedMeanInteraction.LocalMeanVector
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(C : ℕ → I → Set D)
(H : ℝ)
(m : ℕ → I → D → HarmonicCalculus.ComplexVector)
:
Local mean vector, constructed using LocalMean.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.LocalizedMeanInteraction.localMean_component
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{H : ℝ}
{m : ℕ → I → D → HarmonicCalculus.ComplexVector}
(hm : LocalMeanVector s C H m)
(i : Fin 3)
:
theorem
NavierStokes.LocalizedMeanInteraction.local_cmul
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{w v : ℕ → I → D → ℝ}
{α β : ℝ}
{f g : ℕ → I → D → ℂ}
(hf : LocalizedWaveBounds.LocalClass s C w α f)
(hg : LocalizedWaveBounds.LocalClass s C v β g)
:
theorem
NavierStokes.LocalizedMeanInteraction.local_mean_wave_cmul
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{P : ℕ → I → D → ℝ}
{α β : ℝ}
{f g : ℕ → I → D → ℂ}
(hf : LocalMean s C α f)
(hg : LocalizedWaveBounds.LocalWave s C P β g)
(hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1)
:
LocalizedWaveBounds.LocalWave s C P (α + β) fun (n : ℕ) (l : I) (x : D) => f n l x * g n l x
theorem
NavierStokes.LocalizedMeanInteraction.local_wave_mean_cmul
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{P : ℕ → I → D → ℝ}
{α β : ℝ}
{f g : ℕ → I → D → ℂ}
(hf : LocalizedWaveBounds.LocalWave s C P α f)
(hg : LocalMean s C β g)
(hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1)
:
LocalizedWaveBounds.LocalWave s C P (α + β) fun (n : ℕ) (l : I) (x : D) => f n l x * g n l x
theorem
NavierStokes.LocalizedMeanInteraction.local_along
{D : Type}
{I : Type u_1}
{E : Type u_2}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{w : ℕ → I → D → ℝ}
{α β : ℝ}
{f : ℕ → I → D → E}
{V : ℕ → I → D → D}
(hf : LocalizedWaveBounds.LocalClass s C w α f)
(hV : LocalizedWaveBounds.LocalUnweighted s C β V)
:
LocalizedWaveBounds.LocalClass s C w (α + β) fun (n : ℕ) (l : I) => HarmonicCalculus.along (V n l) (f n l)
theorem
NavierStokes.LocalizedMeanInteraction.local_div_radius
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{w : ℕ → I → D → ℝ}
{α κ : ℝ}
(G : WaveInteractionBounds.Geometry s κ)
{f : ℕ → I → D → ℂ}
(hf : LocalizedWaveBounds.LocalClass s C w α f)
:
LocalizedWaveBounds.LocalClass s C w α fun (n : ℕ) (l : I) (x : D) => f n l x / ↑(G.radius n x)
theorem
NavierStokes.LocalizedMeanInteraction.local_mean_advects_wave
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{P : ℕ → I → D → ℝ}
{α H κ : ℝ}
(G : WaveInteractionBounds.Geometry s κ)
(hκ : κ ≤ 1)
{m a : ℕ → I → D → HarmonicCalculus.ComplexVector}
(hm : LocalMeanVector s C H m)
(ha : ∀ (i : Fin 3), LocalizedWaveBounds.LocalWave s C P α fun (n : ℕ) (l : I) (x : D) => a n l x i)
(hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1)
(i : Fin 3)
:
LocalizedWaveBounds.LocalWave s C P (α + H) fun (n : ℕ) (l : I) (x : D) =>
WaveInteractionBounds.strippedTransport G (fun (n : ℕ) => m n l) (fun (n : ℕ) => a n l) n x i
theorem
NavierStokes.LocalizedMeanInteraction.local_wave_advects_mean
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{P : ℕ → I → D → ℝ}
{α H κ : ℝ}
(G : WaveInteractionBounds.Geometry s κ)
(hκ : 0 ≤ κ)
{m a : ℕ → I → D → HarmonicCalculus.ComplexVector}
(hm : LocalMeanVector s C H m)
(ha : ∀ (i : Fin 3), LocalizedWaveBounds.LocalWave s C P α fun (n : ℕ) (l : I) (x : D) => a n l x i)
(hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1)
(i : Fin 3)
:
LocalizedWaveBounds.LocalWave s C P (α + H - κ) fun (n : ℕ) (l : I) (x : D) =>
WaveInteractionBounds.strippedTransport G (fun (n : ℕ) => a n l) (fun (n : ℕ) => m n l) n x i
theorem
NavierStokes.LocalizedMeanInteraction.local_normalDot
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{w : ℕ → I → D → ℝ}
{α : ℝ}
{N : ℕ → I → D → EuclideanSpace ℝ (Fin 3)}
{a : ℕ → I → D → HarmonicCalculus.ComplexVector}
(hN : ∀ (i : Fin 3), LocalizedWaveBounds.LocalUnweighted s C 0 fun (n : ℕ) (l : I) (x : D) => (N n l x).ofLp i)
(ha : ∀ (i : Fin 3), LocalizedWaveBounds.LocalClass s C w α fun (n : ℕ) (l : I) (x : D) => a n l x i)
:
LocalizedWaveBounds.LocalClass s C w α fun (n : ℕ) (l : I) (x : D) => HarmonicCalculus.normalDot (N n l x) (a n l x)
theorem
NavierStokes.LocalizedMeanInteraction.local_waveMeanCoefficient
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{P : ℕ → I → D → ℝ}
{α H κ : ℝ}
(G : WaveInteractionBounds.Geometry s κ)
(hκ0 : 0 ≤ κ)
(hκ1 : κ ≤ 1 / 2)
{Φ : ℕ → I → D → ℝ}
{ν : ℕ → I → ℝ}
{m a : ℕ → I → D → HarmonicCalculus.ComplexVector}
(hm : LocalMeanVector s C H m)
(ha : ∀ (i : Fin 3), LocalizedWaveBounds.LocalWave s C P α fun (n : ℕ) (l : I) (x : D) => a n l x i)
(hN :
∀ (i : Fin 3),
LocalizedWaveBounds.LocalUnweighted s C 0 fun (n : ℕ) (l : I) (x : D) =>
(HarmonicCalculus.phaseNormal (G.radius n) (G.radial n) (G.angular n) (G.axial n) (Φ n l) x).ofLp i)
(hν : LocalizedWaveBounds.LocalUnweighted s C (-(1 / 2)) fun (n : ℕ) (l : I) (x : D) => ν n l)
(hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1)
(i : Fin 3)
:
LocalizedWaveBounds.LocalWave s C P (α + H - 1 / 2) fun (n : ℕ) (l : I) (x : D) =>
WaveInteractionBounds.waveMeanCoefficient G (fun (n : ℕ) => Φ n l) (fun (n : ℕ) => ν n l) (fun (n : ℕ) => m n l)
(fun (n : ℕ) => a n l) n x i
theorem
NavierStokes.LocalizedMeanInteraction.local_realCoefficient
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{P : ℕ → I → D → ℝ}
{α : ℝ}
(a : ℕ → I → HarmonicFields.Coefficients D)
(j : ℤ)
(ha : LocalizedWaveBounds.LocalWave s C P α fun (n : ℕ) (l : I) (x : D) => (a n l).coeff j x)
(han : LocalizedWaveBounds.LocalWave s C P α fun (n : ℕ) (l : I) (x : D) => (a n l).coeff (-j) x)
:
LocalizedWaveBounds.LocalWave s C P α fun (n : ℕ) (l : I) (x : D) =>
(HarmonicResidual.realCoefficients (a n l)).coeff j x
theorem
NavierStokes.LocalizedMeanInteraction.local_blockAmplitude
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{P : ℕ → I → D → ℝ}
{α : ℝ}
{b : I → CorrectionState.HarmonicBlock D}
(hb :
∀ (i : Fin 3) (j : ℤ),
j ≠ 0 → LocalizedWaveBounds.LocalWave s C P α fun (n : ℕ) (l : I) (x : D) => ((b l).velocity n i).coeff j x)
{j : ℤ}
(hj : j ≠ 0)
(i : Fin 3)
:
LocalizedWaveBounds.LocalWave s C P α fun (n : ℕ) (l : I) (x : D) =>
(HarmonicMeanInteraction.blockAmplitude (b l) n i).coeff j x
theorem
NavierStokes.LocalizedMeanInteraction.local_frequency_mul_const
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{β : ℝ}
{ν : ℕ → I → ℝ}
(hν : LocalizedWaveBounds.LocalUnweighted s C β fun (n : ℕ) (l : I) (x : D) => ν n l)
(r : ℝ)
:
LocalizedWaveBounds.LocalUnweighted s C β fun (n : ℕ) (l : I) (x : D) => ν n l * r
theorem
NavierStokes.LocalizedMeanInteraction.local_meanCross
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{P : ℕ → I → D → ℝ}
{α H κ : ℝ}
(c : CorrectionState.Context D)
(ho : MeanIncrementBounds.OperatorBounds s c.operators κ)
(hκ : κ ≤ 1 / 2)
(hR : ∀ x ∈ s.domain, 0 < c.operators.radius x)
{h : I → MeanIncrementBounds.Triple D}
{b : I → CorrectionState.HarmonicBlock D}
(hm : LocalMeanVector s C H fun (n : ℕ) (l : I) => HarmonicMeanInteraction.tripleField (h l) n)
(hb :
∀ (i : Fin 3) (j : ℤ),
j ≠ 0 → LocalizedWaveBounds.LocalWave s C P α fun (n : ℕ) (l : I) (x : D) => ((b l).velocity n i).coeff j x)
(hN :
∀ (i : Fin 3),
LocalizedWaveBounds.LocalUnweighted s C 0 fun (n : ℕ) (l : I) (x : D) =>
(HarmonicMeanInteraction.slowNormal c ho hR (b l).phase n x).ofLp i)
(hk : LocalizedWaveBounds.LocalUnweighted s C (-(1 / 2)) fun (n : ℕ) (l : I) (x : D) => (b l).frequency n)
(hkp : LocalizedWaveBounds.LocalUnweighted s C (-(1 / 2)) fun (n : ℕ) (l : I) (x : D) => ↑((b l).angularFrequency n))
{j : ℤ}
(hj : j ≠ 0)
(i : Fin 3)
:
LocalizedWaveBounds.LocalWave s C P (α + H - 1 / 2) fun (n : ℕ) (l : I) (x : D) =>
(HarmonicMeanInteraction.meanCross c (h l) (b l) n i).coeff j x
Zero germs and globalization #
theorem
NavierStokes.LocalizedMeanInteraction.realCoefficient_zero_germ
{D : Type}
[NormedAddCommGroup D]
{a : HarmonicFields.Coefficients D}
{j : ℤ}
{x : D}
(ha : a.coeff j =ᶠ[nhds x] fun (x : D) => 0)
(han : a.coeff (-j) =ᶠ[nhds x] fun (x : D) => 0)
:
theorem
NavierStokes.LocalizedMeanInteraction.crossCoefficients_zero_germ
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(g : HarmonicResidual.Frame D)
(k : ℝ)
(Φ : D → ℝ)
(kp : ℤ)
(m : D → HarmonicCalculus.ComplexVector)
(a : HarmonicResidual.VectorCoefficients D)
(j : ℤ)
{x : D}
(ha : ∀ (i : Fin 3), (a i).coeff j =ᶠ[nhds x] fun (x : D) => 0)
(i : Fin 3)
:
theorem
NavierStokes.LocalizedMeanInteraction.meanCross_zero_germ
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(h : MeanIncrementBounds.Triple D)
(b : CorrectionState.HarmonicBlock D)
(n : ℕ)
{j : ℤ}
{x : D}
(hz :
∀ (i : Fin 3),
((b.velocity n i).coeff j =ᶠ[nhds x] fun (x : D) => 0) ∧ (b.velocity n i).coeff (-j) =ᶠ[nhds x] fun (x : D) => 0)
(i : Fin 3)
:
theorem
NavierStokes.LocalizedMeanInteraction.realMeanCross_zero_germ
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(h : MeanIncrementBounds.Triple D)
(b : CorrectionState.HarmonicBlock D)
(n : ℕ)
{j : ℤ}
(hj : j ≠ 0)
{x : D}
(hz : ∀ (i : Fin 3) (k : ℤ), k ≠ 0 → (b.velocity n i).coeff k =ᶠ[nhds x] fun (x : D) => 0)
(i : Fin 3)
:
(HarmonicResidual.realCoefficients (HarmonicMeanInteraction.meanCross c h b n i)).coeff j =ᶠ[nhds x] fun (x : D) => 0
theorem
NavierStokes.LocalizedMeanInteraction.local_of_uniform
{D : Type}
{I : Type u_1}
{E : Type u_2}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{w : ℕ → I → D → ℝ}
{α : ℝ}
{f : I → ℕ → D → E}
(hf : LabelSumBounds.UniformClass s (fun (l : I) (n : ℕ) => w n l) α f)
:
LocalizedWaveBounds.LocalClass s C w α fun (n : ℕ) (l : I) => f l n
theorem
NavierStokes.LocalizedMeanInteraction.uniform_of_supported_local
{D : Type}
{I : Type u_1}
{E : Type u_2}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{w : ℕ → I → D → ℝ}
{α : ℝ}
{f : ℕ → I → D → E}
(hf : LocalizedWaveBounds.LocalClass s C w α f)
(hz : ∀ (n : ℕ) (l : I), ∀ x ∈ s.domain, x ∉ C n l → f n l =ᶠ[nhds x] fun (x : D) => 0)
:
LabelSumBounds.UniformClass s (fun (l : I) (n : ℕ) => w n l) α fun (l : I) (n : ℕ) => f n l
theorem
NavierStokes.LocalizedMeanInteraction.uniform_constant
{D : Type}
{I : Type u_1}
{E : Type u_2}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ℕ → D → ℝ}
{α : ℝ}
{f : ℕ → D → E}
(hf : WeightedClasses.MemClass s w α f)
:
LabelSumBounds.UniformClass s (fun (x : I) => w) α fun (x : I) => f
theorem
NavierStokes.LocalizedMeanInteraction.local_iUnion
{D : Type}
{I : Type u_1}
{E : Type u_2}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{J : Type u_3}
[Nonempty J]
{s : WeightedClasses.StripData D}
{C : ℕ → I → J → Set D}
{w : ℕ → I → D → ℝ}
{α : ℝ}
{f : ℕ → I → D → E}
(hf :
LocalizedWaveBounds.LocalClass s (fun (n : ℕ) (p : I × J) => C n p.1 p.2) (fun (n : ℕ) (p : I × J) => w n p.1) α
fun (n : ℕ) (p : I × J) => f n p.1)
:
LocalizedWaveBounds.LocalClass s (fun (n : ℕ) (l : I) => ⋃ (j : J), C n l j) w α f
A common coefficient estimated uniformly on every native copy patch is estimated on their union with the very same constants.
theorem
NavierStokes.LocalizedMeanInteraction.velocity_zero_germs_of_tsupport
{D : Type}
[NormedAddCommGroup D]
(b : CorrectionState.HarmonicBlock D)
{C : ℕ → Set D}
(hs : ∀ (n : ℕ) (i : Fin 3) (j : ℤ), j ≠ 0 → tsupport ((b.velocity n i).coeff j) ⊆ C n)
(n : ℕ)
{x : D}
(hx : x ∉ C n)
(i : Fin 3)
(j : ℤ)
(hj : j ≠ 0)
:
theorem
NavierStokes.LocalizedMeanInteraction.uniform_realMeanCross_class
{D : Type}
{I : Type u_1}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → I → Set D}
{P : ℕ → I → D → ℝ}
{α H κ : ℝ}
(c : CorrectionState.Context D)
(ho : MeanIncrementBounds.OperatorBounds s c.operators κ)
(hκ : κ ≤ 1 / 2)
(hR : ∀ x ∈ s.domain, 0 < c.operators.radius x)
{h : MeanIncrementBounds.Triple D}
(hh : MeanIncrementBounds.IncrementBounds s H h)
{b : I → CorrectionState.HarmonicBlock D}
(hb :
∀ (i : Fin 3) (j : ℤ),
j ≠ 0 →
LabelSumBounds.UniformClass s (fun (l : I) (n : ℕ) (x : D) => √(s.zeta x) * P n l x) α
fun (l : I) (n : ℕ) (x : D) => ((b l).velocity n i).coeff j x)
(hN :
∀ (i : Fin 3),
LocalizedWaveBounds.LocalUnweighted s C 0 fun (n : ℕ) (l : I) (x : D) =>
(HarmonicMeanInteraction.slowNormal c ho hR (b l).phase n x).ofLp i)
(hk : LocalizedWaveBounds.LocalUnweighted s C (-(1 / 2)) fun (n : ℕ) (l : I) (x : D) => (b l).frequency n)
(hkp : LocalizedWaveBounds.LocalUnweighted s C (-(1 / 2)) fun (n : ℕ) (l : I) (x : D) => ↑((b l).angularFrequency n))
(hz :
∀ (n : ℕ) (l : I),
∀ x ∈ s.domain, x ∉ C n l → ∀ (i : Fin 3) (j : ℤ), j ≠ 0 → ((b l).velocity n i).coeff j =ᶠ[nhds x] fun (x : D) => 0)
{j : ℤ}
(hj : j ≠ 0)
(i : Fin 3)
:
LabelSumBounds.UniformClass s (fun (l : I) (n : ℕ) (x : D) => √(s.zeta x) * P n l x) (α + H - 1 / 2)
fun (l : I) (n : ℕ) (x : D) =>
(HarmonicResidual.realCoefficients (HarmonicMeanInteraction.meanCross c h (b l) n i)).coeff j x
All constants precede the external label as well as the band. Only the actual phase patch carries a normal estimate.
theorem
NavierStokes.LocalizedMeanInteraction.realMeanCross_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → Set D}
{P : ℕ → D → ℝ}
{α H κ : ℝ}
(c : CorrectionState.Context D)
(ho : MeanIncrementBounds.OperatorBounds s c.operators κ)
(hκ : κ ≤ 1 / 2)
(hR : ∀ x ∈ s.domain, 0 < c.operators.radius x)
{h : MeanIncrementBounds.Triple D}
(hh : MeanIncrementBounds.IncrementBounds s H h)
{b : CorrectionState.HarmonicBlock D}
(hb : CorrectionState.HarmonicBlock.WaveBounds s P α b)
(hN :
∀ (i : Fin 3),
LocalizedWaveBounds.LocalUnweighted s (fun (n : ℕ) (x : Unit) => C n) 0 fun (n : ℕ) (x : Unit) (x_1 : D) =>
(HarmonicMeanInteraction.slowNormal c ho hR b.phase n x_1).ofLp i)
(hk : WeightedClasses.BandBound s (-(1 / 2)) b.frequency)
(hkp : WeightedClasses.BandBound s (-(1 / 2)) fun (n : ℕ) => ↑(b.angularFrequency n))
(hz :
∀ (n : ℕ),
∀ x ∈ s.domain, x ∉ C n → ∀ (i : Fin 3) (j : ℤ), j ≠ 0 → (b.velocity n i).coeff j =ᶠ[nhds x] fun (x : D) => 0)
{j : ℤ}
(hj : j ≠ 0)
(i : Fin 3)
:
WeightedClasses.WaveClass s P (α + H - 1 / 2) fun (n : ℕ) (x : D) =>
(HarmonicResidual.realCoefficients (HarmonicMeanInteraction.meanCross c h b n i)).coeff j x
The single-block endpoint on the original state domain.
The literal residual and interaction blocks #
theorem
NavierStokes.LocalizedMeanInteraction.interactionBlock_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → Set D}
{κ α β H : ℝ}
{P : ℕ → D → ℝ}
(c : CorrectionState.Context D)
(ho : MeanIncrementBounds.OperatorBounds s c.operators κ)
(hκ : κ ≤ 1 / 2)
(hR : ∀ x ∈ s.domain, 0 < c.operators.radius x)
{u : CorrectionState.State D}
(hm : MeanIncrementBounds.IncrementBounds s H u.mean)
{a b : CorrectionState.HarmonicBlock D}
{M N : ℕ}
(ha : CorrectionState.HarmonicBlock.WaveBounds s P α a)
(hb : CorrectionState.HarmonicBlock.WaveBounds s P β b)
(ha0 : HarmonicWaveInteraction.ZeroMode a)
(hb0 : HarmonicWaveInteraction.ZeroMode b)
(hM : a.BandLimited M)
(hN : b.BandLimited N)
(hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain)
(hk : ∀ (n : ℕ), a.frequency n ≠ 0)
(hda : HarmonicWaveInteraction.ModeSolenoidal s c a)
(hdb : HarmonicWaveInteraction.ModeSolenoidal s c (HarmonicWaveInteraction.withCarrier a b))
(hNormal :
∀ (i : Fin 3),
LocalizedWaveBounds.LocalUnweighted s (fun (n : ℕ) (x : Unit) => C n) 0 fun (n : ℕ) (x : Unit) (x_1 : D) =>
(HarmonicMeanInteraction.slowNormal c ho hR a.phase n x_1).ofLp i)
(hFreq : WeightedClasses.BandBound s (-(1 / 2)) a.frequency)
(hAng : WeightedClasses.BandBound s (-(1 / 2)) fun (n : ℕ) => ↑(a.angularFrequency n))
(hz :
∀ (n : ℕ),
∀ x ∈ s.domain, x ∉ C n → ∀ (i : Fin 3) (j : ℤ), j ≠ 0 → (b.velocity n i).coeff j =ᶠ[nhds x] fun (x : D) => 0)
(hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x)
(hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1)
:
CorrectionState.HarmonicBlock.WaveBounds s P (min (β + H - 1 / 2) (min (α + β - κ) (β + β - κ)))
(HarmonicWaveInteraction.interactionBlock c u a b)
The normal-free wave-wave estimate is combined with the newly localized mean-wave estimate, preserving both gains and their minimum.
theorem
NavierStokes.LocalizedMeanInteraction.residualBlock_mean_update_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → Set D}
{κ α H : ℝ}
{P : ℕ → D → ℝ}
(c : CorrectionState.Context D)
(ho : MeanIncrementBounds.OperatorBounds s c.operators κ)
(hκ : κ ≤ 1 / 2)
(hR : ∀ x ∈ s.domain, 0 < c.operators.radius x)
(s₀ s₁ : CorrectionState.State D)
(h : MeanIncrementBounds.Triple D)
(he : s₁.mean = MeanIncrementBounds.updated s₀.mean h)
(hbase : MeanIncrementBounds.SmoothTriple s.domain c.base)
(hmean : MeanIncrementBounds.SmoothTriple s.domain s₀.mean)
(hh : MeanIncrementBounds.IncrementBounds s H h)
(b : CorrectionState.HarmonicBlock D)
(hb : CorrectionState.HarmonicBlock.WaveBounds s P α b)
(hN :
∀ (i : Fin 3),
LocalizedWaveBounds.LocalUnweighted s (fun (n : ℕ) (x : Unit) => C n) 0 fun (n : ℕ) (x : Unit) (x_1 : D) =>
(HarmonicMeanInteraction.slowNormal c ho hR b.phase n x_1).ofLp i)
(hk : WeightedClasses.BandBound s (-(1 / 2)) b.frequency)
(hkp : WeightedClasses.BandBound s (-(1 / 2)) fun (n : ℕ) => ↑(b.angularFrequency n))
(hz :
∀ (n : ℕ),
∀ x ∈ s.domain, x ∉ C n → ∀ (i : Fin 3) (j : ℤ), j ≠ 0 → (b.velocity n i).coeff j =ᶠ[nhds x] fun (x : D) => 0)
(G A₀ A₁ : HarmonicResidual.BlockCoefficients D)
(hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A₁ n i - A₀ n i) 0)
{j : ℤ}
(hj : j ≠ 0)
(i : Fin 3)
:
WeightedClasses.WaveClass s P (α + H - 1 / 2) fun (n : ℕ) (x : D) =>
((HarmonicResidual.residualBlock c s₁ b G A₁).velocity n i).coeff j x - ((HarmonicResidual.residualBlock c s₀ b G A₀).velocity n i).coeff j x
theorem
NavierStokes.LocalizedMeanInteraction.residualDifferenceBlock_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{C : ℕ → Set D}
{κ α H : ℝ}
{P : ℕ → D → ℝ}
(c : CorrectionState.Context D)
(ho : MeanIncrementBounds.OperatorBounds s c.operators κ)
(hκ : κ ≤ 1 / 2)
(hR : ∀ x ∈ s.domain, 0 < c.operators.radius x)
(s₀ s₁ : CorrectionState.State D)
(h : MeanIncrementBounds.Triple D)
(he : s₁.mean = MeanIncrementBounds.updated s₀.mean h)
(hbase : MeanIncrementBounds.SmoothTriple s.domain c.base)
(hmean : MeanIncrementBounds.SmoothTriple s.domain s₀.mean)
(hh : MeanIncrementBounds.IncrementBounds s H h)
(b : CorrectionState.HarmonicBlock D)
(hb : CorrectionState.HarmonicBlock.WaveBounds s P α b)
(hN :
∀ (i : Fin 3),
LocalizedWaveBounds.LocalUnweighted s (fun (n : ℕ) (x : Unit) => C n) 0 fun (n : ℕ) (x : Unit) (x_1 : D) =>
(HarmonicMeanInteraction.slowNormal c ho hR b.phase n x_1).ofLp i)
(hk : WeightedClasses.BandBound s (-(1 / 2)) b.frequency)
(hkp : WeightedClasses.BandBound s (-(1 / 2)) fun (n : ℕ) => ↑(b.angularFrequency n))
(hz :
∀ (n : ℕ),
∀ x ∈ s.domain, x ∉ C n → ∀ (i : Fin 3) (j : ℤ), j ≠ 0 → (b.velocity n i).coeff j =ᶠ[nhds x] fun (x : D) => 0)
(G A₀ A₁ : HarmonicResidual.BlockCoefficients D)
(hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A₁ n i - A₀ n i) 0)
:
CorrectionState.HarmonicBlock.WaveBounds s P (α + H - 1 / 2)
(HarmonicMeanInteraction.residualDifferenceBlock c s₀ s₁ b G A₀ A₁)