Uniform weighted bounds for actual label sums #
The constants in UniformClass are chosen before the label. The spatial
sum estimates use the actual closed label windows and the existing finite
coloring, rather than the total number of labels in an active finite set.
structure
NavierStokes.LabelSumBounds.UniformClass
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData D)
(w : ι → ℕ → D → ℝ)
(α : ℝ)
(f : ι → ℕ → D → E)
:
The finite-jet constants and polynomial degrees are independent of both band and label. The majorant may retain a label-dependent envelope.
Instances For
@[reducible, inline]
noncomputable abbrev
NavierStokes.LabelSumBounds.UniformMeanClass
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData D)
(α : ℝ)
(f : ι → ℕ → D → E)
:
Uniform mean class: an abbreviation for UniformClass s (fun _ _ x => s.zeta x) α f.
Equations
- NavierStokes.LabelSumBounds.UniformMeanClass s α f = NavierStokes.LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => s.zeta x_2) α f
Instances For
@[reducible, inline]
noncomputable abbrev
NavierStokes.LabelSumBounds.UniformWaveClass
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData D)
(P : ι → ℕ → D → ℝ)
(α : ℝ)
(f : ι → ℕ → D → E)
:
Uniform wave class: an abbreviation for UniformClass s (fun l n x => Real.sqrt (s.zeta x) * P l n x) α f.
Equations
- NavierStokes.LabelSumBounds.UniformWaveClass s P α f = NavierStokes.LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => √(s.zeta x) * P l n x) α f
Instances For
theorem
NavierStokes.LabelSumBounds.UniformClass.each
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
{f : ι → ℕ → D → E}
(hf : UniformClass s w α f)
(l : ι)
:
WeightedClasses.MemClass s (w l) α (f l)
theorem
NavierStokes.LabelSumBounds.UniformClass.reindex
{ι : Type u_1}
{κ : Type u_2}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
{f : ι → ℕ → D → E}
(hf : UniformClass s w α f)
(a : κ → ι)
:
UniformClass s (fun (l : κ) => w (a l)) α fun (l : κ) => f (a l)
theorem
NavierStokes.LabelSumBounds.UniformClass.zero
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
(hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w l n x)
:
UniformClass s w α fun (x : ι) (x_1 : ℕ) (x_2 : D) => 0
theorem
NavierStokes.LabelSumBounds.UniformClass.congr
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
{f g : ι → ℕ → D → E}
(hf : UniformClass s w α f)
(hfg : ∀ (l : ι) (n : ℕ), Set.EqOn (f l n) (g l n) s.domain)
:
UniformClass s w α g
theorem
NavierStokes.LabelSumBounds.UniformClass.mono_weight
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w v : ι → ℕ → D → ℝ}
{α : ℝ}
{f : ι → ℕ → D → E}
(hf : UniformClass s w α f)
(hv : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ v l n x)
(hwv : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, w l n x ≤ v l n x)
:
UniformClass s v α f
theorem
NavierStokes.LabelSumBounds.UniformClass.mono_exponent
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α β : ℝ}
{f : ι → ℕ → D → E}
(hf : UniformClass s w α f)
(hβα : β ≤ α)
:
UniformClass s w β f
theorem
NavierStokes.LabelSumBounds.UniformClass.add
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
{f g : ι → ℕ → D → E}
(hf : UniformClass s w α f)
(hg : UniformClass s w α g)
:
UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => f l n x + g l n x
theorem
NavierStokes.LabelSumBounds.UniformClass.map
{ι : Type u_1}
{E : Type u_3}
{F : Type u_4}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
{f : ι → ℕ → D → E}
(hf : UniformClass s w α f)
(L : E →L[ℝ] F)
:
UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => L (f l n x)
theorem
NavierStokes.LabelSumBounds.UniformClass.neg
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
{f : ι → ℕ → D → E}
(hf : UniformClass s w α f)
:
UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => -f l n x
theorem
NavierStokes.LabelSumBounds.UniformClass.sub
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
{f g : ι → ℕ → D → E}
(hf : UniformClass s w α f)
(hg : UniformClass s w α g)
:
UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => f l n x - g l n x
theorem
NavierStokes.LabelSumBounds.UniformClass.sum
{ι : Type u_1}
{κ : Type u_2}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
(F : Finset κ)
(f : κ → ι → ℕ → D → E)
(hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w l n x)
(hf : ∀ k ∈ F, UniformClass s w α (f k))
:
UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => ∑ k ∈ F, f k l n x
theorem
NavierStokes.LabelSumBounds.bilinear_jet_bound
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
(L : E →L[ℝ] F →L[ℝ] G)
{U : Set D}
(hU : IsOpen U)
{f : D → E}
{g : D → F}
(hf : ContDiffOn ℝ (↑⊤) f U)
(hg : ContDiffOn ℝ (↑⊤) g U)
{x : D}
(hx : x ∈ U)
{m j : ℕ}
(hj : j ≤ m)
{A B : ℝ}
(hA : 0 ≤ A)
(hB : 0 ≤ B)
(ha : ∀ i ≤ m, ‖iteratedFDeriv ℝ i f x‖ ≤ A)
(hb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g x‖ ≤ B)
:
Pointwise finite-jet Leibniz estimate. The two bounds may be frozen values of variable envelopes at this point.
theorem
NavierStokes.LabelSumBounds.UniformClass.bilinear
{ι : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{s : WeightedClasses.StripData D}
{w v : ι → ℕ → D → ℝ}
{α β : ℝ}
{f : ι → ℕ → D → E}
{g : ι → ℕ → D → F}
(hf : UniformClass s w α f)
(hg : UniformClass s v β g)
(L : E →L[ℝ] F →L[ℝ] G)
:
UniformClass s (fun (l : ι) (n : ℕ) (x : D) => w l n x * v l n x) (α + β) fun (l : ι) (n : ℕ) (x : D) =>
(L (f l n x)) (g l n x)
theorem
NavierStokes.LabelSumBounds.uniform_wave_bilinear_mean
{ι : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α β : ℝ}
{f : ι → ℕ → D → E}
{g : ι → ℕ → D → F}
(hf : UniformWaveClass s P α f)
(hg : UniformWaveClass s P β g)
(hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x)
(hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1)
(L : E →L[ℝ] F →L[ℝ] G)
:
UniformMeanClass s (α + β) fun (l : ι) (n : ℕ) (x : D) => (L (f l n x)) (g l n x)
Closed, enlarged label windows #
@[reducible, inline]
Window point: an abbreviation for ℝ × SlotColoring.Position.
Instances For
The first coordinate is the logarithmic dyadic coordinate. The
window includes a two-level closed band and the actual two-mesh spatial
box used by SlotColoring.
Equations
- NavierStokes.LabelSumBounds.closedWindow d l = Set.Icc (↑l.1 - 2) (↑l.1 + 2) ×ˢ NavierStokes.SlotColoring.physicalBox d l
Instances For
theorem
NavierStokes.LabelSumBounds.closedWindow_closed
(d : ℝ)
(l : SlotColoring.Label)
:
IsClosed (closedWindow d l)
theorem
NavierStokes.LabelSumBounds.closedWindow_adjacency
{d : ℝ}
{l k : SlotColoring.Label}
{x : WindowPoint}
(hl : 1 ≤ l.1)
(hk : 1 ≤ k.1)
(hne : l ≠ k)
(hxl : x ∈ closedWindow d l)
(hxk : x ∈ closedWindow d k)
:
SlotColoring.Adj d l k
theorem
NavierStokes.LabelSumBounds.closedWindow_color_injective
(d : ℝ)
(x : WindowPoint)
:
Set.InjOn SlotColoring.colorData {l : SlotColoring.Label | 1 ≤ l.1 ∧ x ∈ closedWindow d l}
The already constructed coloring remains injective on these closed enlargements. Endpoints do not require a separate exceptional case.
theorem
NavierStokes.LabelSumBounds.closedWindow_card_le
(d : ℝ)
(x : WindowPoint)
(F : Finset SlotColoring.Label)
(hF : ∀ l ∈ F, 1 ≤ l.1 ∧ x ∈ closedWindow d l)
:
theorem
NavierStokes.LabelSumBounds.labelRegion_subset_closedWindow
{d : ℝ}
{l : SlotColoring.Label}
{x : WindowPoint}
(hl : 1 ≤ l.1)
(hx : x ∈ PhysicalWaveSum.labelRegion d l)
(hq : 0 < x.1)
:
The genuine closed dyadic-mask and slow-mask supports lie inside the enlargement; the inclusion also applies to every derivative support.
theorem
NavierStokes.LabelSumBounds.physicalMask_tsupport_closedWindow
{d : ℝ}
{l : SlotColoring.Label}
{x : WindowPoint}
(hl : 1 ≤ l.1)
(hq : 0 < x.1)
(hx : x ∈ tsupport (PhysicalWaveSum.physicalMask d l))
:
theorem
NavierStokes.LabelSumBounds.physicalMask_jet_tsupport_closedWindow
{d : ℝ}
{l : SlotColoring.Label}
{x : WindowPoint}
(hl : 1 ≤ l.1)
(hq : 0 < x.1)
(m : ℕ)
(hx : x ∈ tsupport (iteratedFDeriv ℝ m (PhysicalWaveSum.physicalMask d l)))
:
theorem
NavierStokes.LabelSumBounds.window_card_le
{ι : Type u_1}
{d : ℝ}
{x : WindowPoint}
(F : Finset ι)
(label : ι → SlotColoring.Label)
(hinj : Set.InjOn label ↑F)
(hF : ∀ l ∈ F, 1 ≤ (label l).1 ∧ x ∈ closedWindow d (label l))
:
theorem
NavierStokes.LabelSumBounds.jet_zero_off_window
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : Set D}
(hU : IsOpen U)
{x : D}
(hx : x ∈ U)
{d : ℝ}
{label : SlotColoring.Label}
{χ : D → WindowPoint}
(hχ : ContinuousAt χ x)
{f : D → E}
(hs : ∀ y ∈ U, f y ≠ 0 → χ y ∈ closedWindow d label)
(hout : χ x ∉ closedWindow d label)
(m : ℕ)
:
theorem
NavierStokes.LabelSumBounds.finite_sum_jet_bound
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : Set D}
(hU : IsOpen U)
{x : D}
(hx : x ∈ U)
(F : Finset ι)
(label : ι → SlotColoring.Label)
(hinj : Set.InjOn label ↑F)
(hlevel : ∀ l ∈ F, 1 ≤ (label l).1)
(d : ℝ)
(χ : D → WindowPoint)
(hχ : ContinuousAt χ x)
(f : ι → D → E)
(m : ℕ)
(hf : ∀ l ∈ F, ContDiffAt ℝ (↑m) (f l) x)
(hs : ∀ l ∈ F, ∀ y ∈ U, f l y ≠ 0 → χ y ∈ closedWindow d (label l))
{B : ℝ}
(hB : 0 ≤ B)
(hb : ∀ l ∈ F, χ x ∈ closedWindow d (label l) → ‖iteratedFDeriv ℝ m (f l) x‖ ≤ B)
:
A finite active family may have arbitrarily many labels in total.
Only its at-most-2250 locally supported derivatives contribute at x.
theorem
NavierStokes.LabelSumBounds.window_sum_memClass
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{w : ℕ → D → ℝ}
{α : ℝ}
(labels : ℕ → Finset ι)
(label : ℕ → ι → SlotColoring.Label)
(hinj : ∀ (n : ℕ), Set.InjOn (label n) ↑(labels n))
(hlevel : ∀ (n : ℕ), ∀ l ∈ labels n, 1 ≤ (label n l).1)
(d : ℝ)
(χ : ℕ → D → WindowPoint)
(hχ : ∀ (n : ℕ), ContinuousOn (χ n) s.domain)
{f : ι → ℕ → D → E}
(hf : UniformClass s (fun (x : ι) => w) α f)
(hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x)
(hs : ∀ (n : ℕ), ∀ l ∈ labels n, ∀ x ∈ s.domain, f l n x ≠ 0 → χ n x ∈ closedWindow d (label n l))
:
WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => ∑ l ∈ labels n, f l n x
The actual band-dependent finite label sum retains its weighted exponent and polynomial degree. The coefficient constant is multiplied by the fixed overlap bound, not by the active set's total cardinality.
Uniform estimates for the actual angular covariance #
theorem
NavierStokes.LabelSumBounds.uniform_realCoefficients
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α : ℝ}
(a : ι → ℕ → HarmonicFields.Coefficients D)
(ha : ∀ (j : ℤ), UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => (a l n).coeff j x)
(j : ℤ)
:
UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => (HarmonicResidual.realCoefficients (a l n)).coeff j x
theorem
NavierStokes.LabelSumBounds.uniform_angularProduct
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α β : ℝ}
(a b : ι → ℕ → HarmonicFields.Coefficients D)
(F : Finset ℤ)
(hF : ∀ (l : ι) (n : ℕ), (a l n).support ⊆ F)
(ha : ∀ j ∈ F, UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => (a l n).coeff j x)
(hb : ∀ j ∈ F, UniformWaveClass s P β fun (l : ι) (n : ℕ) (x : D) => (b l n).coeff (-j) x)
(hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x)
(hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1)
(k : ι → ℕ → ℝ)
(phase : ι → ℕ → D → ℝ)
(kp : ι → ℕ → ℤ)
(hkp : ∀ (l : ι) (n : ℕ), kp l n ≠ 0)
:
UniformMeanClass s (α + β) fun (l : ι) (n : ℕ) (x : D) =>
HarmonicFields.angularMean fun (θ : ℝ) =>
HarmonicFields.field (a l n) (k l n) (phase l n) (kp l n) (x, θ) * HarmonicFields.field (b l n) (k l n) (phase l n) (kp l n) (x, θ)
theorem
NavierStokes.LabelSumBounds.uniform_realAngularProduct
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α β : ℝ}
(a b : ι → ℕ → HarmonicFields.Coefficients D)
(N : ℕ)
(hband : ∀ (l : ι) (n : ℕ), HarmonicFields.BandLimited (a l n) N)
(ha : ∀ (j : ℤ), UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => (a l n).coeff j x)
(hb : ∀ (j : ℤ), UniformWaveClass s P β fun (l : ι) (n : ℕ) (x : D) => (b l n).coeff j x)
(hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x)
(hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1)
(k : ι → ℕ → ℝ)
(phase : ι → ℕ → D → ℝ)
(kp : ι → ℕ → ℤ)
(hkp : ∀ (l : ι) (n : ℕ), kp l n ≠ 0)
:
UniformMeanClass s (α + β) fun (l : ι) =>
CorrectionState.angularAverage fun (n : ℕ) (p : D × ℝ) =>
(HarmonicFields.field (a l n) (k l n) (phase l n) (kp l n) p).re * (HarmonicFields.field (b l n) (k l n) (phase l n) (kp l n) p).re
Real projection includes the conjugate harmonics. Angular integration is evaluated before taking slow derivatives, so no phase derivative or carrier frequency is paid in this covariance estimate.
theorem
NavierStokes.LabelSumBounds.uniform_mixedBlockCovariance
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α β : ℝ}
(a b : ι → CorrectionState.HarmonicBlock D)
(N : ℕ)
(hband : ∀ (l : ι), (a l).BandLimited N)
(hfreq : ∀ (l : ι), (b l).frequency = (a l).frequency)
(hphase : ∀ (l : ι), (b l).phase = (a l).phase)
(hangular : ∀ (l : ι), (b l).angularFrequency = (a l).angularFrequency)
(ha : ∀ (i : Fin 3) (j : ℤ), UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((a l).velocity n i).coeff j x)
(hb : ∀ (i : Fin 3) (j : ℤ), UniformWaveClass s P β fun (l : ι) (n : ℕ) (x : D) => ((b l).velocity n i).coeff j x)
(hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x)
(hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1)
(hkp : ∀ (l : ι) (n : ℕ), (a l).angularFrequency n ≠ 0)
(i j : Fin 3)
:
UniformMeanClass s (α + β) fun (l : ι) => CorrectionState.bilinearCovariance (a l).oscillation (b l).oscillation i j
theorem
NavierStokes.LabelSumBounds.uniform_blockCovariance
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α : ℝ}
(a : ι → CorrectionState.HarmonicBlock D)
(N : ℕ)
(hband : ∀ (l : ι), (a l).BandLimited N)
(ha : ∀ (i : Fin 3) (j : ℤ), UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((a l).velocity n i).coeff j x)
(hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x)
(hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1)
(hkp : ∀ (l : ι) (n : ℕ), (a l).angularFrequency n ≠ 0)
(i j : Fin 3)
:
UniformMeanClass s (α + α) fun (l : ι) => CorrectionState.bilinearCovariance (a l).oscillation (a l).oscillation i j
Actual finite sums and support-induced covariance diagonality #
noncomputable def
NavierStokes.LabelSumBounds.fieldSum
{ι : Type u_1}
{D : Type}
(labels : ℕ → Finset ι)
(u : ι → CorrectionState.Oscillation D)
:
Field sum, defined pointwise by ∑ l ∈ labels n, u l n p i.
Equations
- NavierStokes.LabelSumBounds.fieldSum labels u n p i = ∑ l ∈ labels n, u l n p i
Instances For
noncomputable def
NavierStokes.LabelSumBounds.AngularContinuous
{D : Type}
(u : CorrectionState.Oscillation D)
:
Angular continuous, given by ∀ n x i, Continuous (fun θ : ℝ => u n (x, θ) i).
Equations
- NavierStokes.LabelSumBounds.AngularContinuous u = ∀ (n : ℕ) (x : D) (i : Fin 3), Continuous fun (θ : ℝ) => u n (x, θ) i
Instances For
noncomputable def
NavierStokes.LabelSumBounds.SupportedOscillations
{ι : Type u_1}
{D : Type}
{d h : ℝ}
{vr vt : TorusInverse.Plane}
(sys : PartitionedCovariance.SlotSystem d h vr vt)
(label : ℕ → ι → SlotColoring.Label)
(χ : ℕ → D → WindowPoint)
(Y : ℕ → D → TorusInverse.Plane)
(U : Set D)
(u : ι → CorrectionState.Oscillation D)
:
Actual support in a slow-label window and its padded native slot, viewed through one common auxiliary coordinate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.LabelSumBounds.supported_cross_product_zero
{ι : Type u_1}
{D : Type}
{d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
{label : ℕ → ι → SlotColoring.Label}
{χ : ℕ → D → WindowPoint}
{Y : ℕ → D → TorusInverse.Plane}
{U : Set D}
{u v : ι → CorrectionState.Oscillation D}
(hu : SupportedOscillations sys label χ Y U u)
(hv : SupportedOscillations sys label χ Y U v)
{l k : ι}
{n : ℕ}
(hl : 1 ≤ (label n l).1)
(hk : 1 ≤ (label n k).1)
(hne : label n l ≠ label n k)
{x : D}
(hx : x ∈ U)
(θ : ℝ)
(i j : Fin 3)
:
theorem
NavierStokes.LabelSumBounds.covariance_fieldSum_eq
{ι : Type u_1}
{D : Type}
(labels : ℕ → Finset ι)
(u v : ι → CorrectionState.Oscillation D)
(hu : ∀ (l : ι), AngularContinuous (u l))
(hv : ∀ (l : ι), AngularContinuous (v l))
{U : Set D}
(hcross :
∀ (n : ℕ),
∀ l ∈ labels n, ∀ k ∈ labels n, l ≠ k → ∀ x ∈ U, ∀ (θ : ℝ) (i j : Fin 3), u l n (x, θ) i * v k n (x, θ) j = 0)
(n : ℕ)
{x : D}
(hx : x ∈ U)
(i j : Fin 3)
:
CorrectionState.bilinearCovariance (fieldSum labels u) (fieldSum labels v) i j n x = ∑ l ∈ labels n, CorrectionState.bilinearCovariance (u l) (v l) i j n x
theorem
NavierStokes.LabelSumBounds.supported_covariance_fieldSum_eq
{ι : Type u_1}
{D : Type}
{d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
(labels : ℕ → Finset ι)
(label : ℕ → ι → SlotColoring.Label)
(hinj : ∀ (n : ℕ), Set.InjOn (label n) ↑(labels n))
(hlevel : ∀ (n : ℕ), ∀ l ∈ labels n, 1 ≤ (label n l).1)
(χ : ℕ → D → WindowPoint)
(Y : ℕ → D → TorusInverse.Plane)
{U : Set D}
(u v : ι → CorrectionState.Oscillation D)
(hu : ∀ (l : ι), AngularContinuous (u l))
(hv : ∀ (l : ι), AngularContinuous (v l))
(hsu : SupportedOscillations sys label χ Y U u)
(hsv : SupportedOscillations sys label χ Y U v)
(n : ℕ)
{x : D}
(hx : x ∈ U)
(i j : Fin 3)
:
CorrectionState.bilinearCovariance (fieldSum labels u) (fieldSum labels v) i j n x = ∑ l ∈ labels n, CorrectionState.bilinearCovariance (u l) (v l) i j n x
theorem
NavierStokes.LabelSumBounds.covariance_window_support
{ι : Type u_1}
{D : Type}
{d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
{label : ℕ → ι → SlotColoring.Label}
{χ : ℕ → D → WindowPoint}
{Y : ℕ → D → TorusInverse.Plane}
{U : Set D}
{u v : ι → CorrectionState.Oscillation D}
(hsu : SupportedOscillations sys label χ Y U u)
(l : ι)
(n : ℕ)
{x : D}
(hx : x ∈ U)
(i j : Fin 3)
(hne : CorrectionState.bilinearCovariance (u l) (v l) i j n x ≠ 0)
:
theorem
NavierStokes.LabelSumBounds.supported_covariance_sum_mem
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{α d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
(labels : ℕ → Finset ι)
(label : ℕ → ι → SlotColoring.Label)
(hinj : ∀ (n : ℕ), Set.InjOn (label n) ↑(labels n))
(hlevel : ∀ (n : ℕ), ∀ l ∈ labels n, 1 ≤ (label n l).1)
(χ : ℕ → D → WindowPoint)
(hχ : ∀ (n : ℕ), ContinuousOn (χ n) s.domain)
(Y : ℕ → D → TorusInverse.Plane)
(u v : ι → CorrectionState.Oscillation D)
(hu : ∀ (l : ι), AngularContinuous (u l))
(hv : ∀ (l : ι), AngularContinuous (v l))
(hsu : SupportedOscillations sys label χ Y s.domain u)
(hsv : SupportedOscillations sys label χ Y s.domain v)
(hcov : ∀ (i j : Fin 3), UniformMeanClass s α fun (l : ι) => CorrectionState.bilinearCovariance (u l) (v l) i j)
(i j : Fin 3)
:
WeightedClasses.MeanClass s α (CorrectionState.bilinearCovariance (fieldSum labels u) (fieldSum labels v) i j)
Generic covariance adapter. The next theorem supplies the uniform single-label estimates directly from harmonic coefficients.
theorem
NavierStokes.LabelSumBounds.harmonic_covariance_sum_mem
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α β d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
(labels : ℕ → Finset ι)
(label : ℕ → ι → SlotColoring.Label)
(hinj : ∀ (n : ℕ), Set.InjOn (label n) ↑(labels n))
(hlevel : ∀ (n : ℕ), ∀ l ∈ labels n, 1 ≤ (label n l).1)
(χ : ℕ → D → WindowPoint)
(hχ : ∀ (n : ℕ), ContinuousOn (χ n) s.domain)
(Y : ℕ → D → TorusInverse.Plane)
(a b : ι → CorrectionState.HarmonicBlock D)
(N : ℕ)
(hband : ∀ (l : ι), (a l).BandLimited N)
(hfreq : ∀ (l : ι), (b l).frequency = (a l).frequency)
(hphase : ∀ (l : ι), (b l).phase = (a l).phase)
(hangular : ∀ (l : ι), (b l).angularFrequency = (a l).angularFrequency)
(ha : ∀ (i : Fin 3) (j : ℤ), UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((a l).velocity n i).coeff j x)
(hb : ∀ (i : Fin 3) (j : ℤ), UniformWaveClass s P β fun (l : ι) (n : ℕ) (x : D) => ((b l).velocity n i).coeff j x)
(hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x)
(hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1)
(hkp : ∀ (l : ι) (n : ℕ), (a l).angularFrequency n ≠ 0)
(hsu : SupportedOscillations sys label χ Y s.domain fun (l : ι) => (a l).oscillation)
(hsv : SupportedOscillations sys label χ Y s.domain fun (l : ι) => (b l).oscillation)
(i j : Fin 3)
:
WeightedClasses.MeanClass s (α + β)
(CorrectionState.bilinearCovariance (fieldSum labels fun (l : ι) => (a l).oscillation)
(fieldSum labels fun (l : ι) => (b l).oscillation) i j)
Uniform coefficients and genuine native-slot support prove the class of the actual covariance of the assembled finite active label sums. Different labels may have different phases and carriers.
Support adapters for the actual native wave construction #
theorem
NavierStokes.LabelSumBounds.SupportedOscillations.add
{ι : Type u_1}
{D : Type}
{d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
{label : ℕ → ι → SlotColoring.Label}
{χ : ℕ → D → WindowPoint}
{Y : ℕ → D → TorusInverse.Plane}
{U : Set D}
{u v : ι → CorrectionState.Oscillation D}
(hu : SupportedOscillations sys label χ Y U u)
(hv : SupportedOscillations sys label χ Y U v)
:
SupportedOscillations sys label χ Y U fun (l : ι) => u l + v l
theorem
NavierStokes.LabelSumBounds.SupportedOscillations.sub
{ι : Type u_1}
{D : Type}
{d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
{label : ℕ → ι → SlotColoring.Label}
{χ : ℕ → D → WindowPoint}
{Y : ℕ → D → TorusInverse.Plane}
{U : Set D}
{u v : ι → CorrectionState.Oscillation D}
(hu : SupportedOscillations sys label χ Y U u)
(hv : SupportedOscillations sys label χ Y U v)
:
SupportedOscillations sys label χ Y U fun (l : ι) => u l - v l
theorem
NavierStokes.LabelSumBounds.covered_product_supported
{ι : Type u_1}
{D : Type}
{d h : ℝ}
{vr vt : TorusInverse.Plane}
(sys : PartitionedCovariance.SlotSystem d h vr vt)
(label : ℕ → ι → SlotColoring.Label)
(χ : ℕ → D → WindowPoint)
(Y : ℕ → D → TorusInverse.Plane)
(U : Set D)
(a : ι → ℕ → D → ℝ → Fin 3 → ℝ)
(f : ι → ℕ → D → ℝ → Fin 3 → TorusInverse.Plane → ℝ)
(ha : ∀ (l : ι) (n : ℕ), ∀ x ∈ U, ∀ (θ : ℝ) (i : Fin 3), a l n x θ i ≠ 0 → χ n x ∈ closedWindow d (label n l))
(hf :
∀ (l : ι) (n : ℕ),
∀ x ∈ U,
∀ (θ : ℝ) (i : Fin 3),
Function.support (f l n x θ i) ⊆ PartitionedCovariance.slotSet h sys.radius vr vt (label n l))
:
SupportedOscillations sys label χ Y U fun (l : ι) (n : ℕ) (p : D × ℝ) (i : Fin 3) =>
a l n p.1 p.2 i * PartitionedCovariance.covered (SlotColoring.nativeIndex h (label n l).1) (f l n p.1 p.2 i) (Y n p.1)
A native covered profile and a supported slow factor give the exact support predicate used above. This also covers derivatives of the slow mask, since their closed supports lie in the same window.
theorem
NavierStokes.LabelSumBounds.native_wave_supported
{ι : Type u_1}
{D : Type}
{d h : ℝ}
{vr vt : TorusInverse.Plane}
(sys : PartitionedCovariance.SlotSystem d h vr vt)
(label : ℕ → ι → SlotColoring.Label)
(hlevel : ∀ (n : ℕ) (l : ι), 1 ≤ (label n l).1)
(q : ℕ → D → ℝ)
(position : ℕ → D → SlotColoring.Position)
(Y : ℕ → D → TorusInverse.Plane)
(U : Set D)
(hq : ∀ (n : ℕ), ∀ x ∈ U, 0 < q n x)
(scale : ι → ℕ → D → Fin 3 → ℝ)
(f : ι → ℕ → D → Fin 3 → TorusInverse.Plane → ℝ)
(mode : ι → ℕ → ℤ)
(phase : ι → ℕ → D → TorusInverse.Plane → ℝ)
(hf :
∀ (l : ι) (n : ℕ),
∀ x ∈ U, ∀ (i : Fin 3), Function.support (f l n x i) ⊆ PartitionedCovariance.slotSet h sys.radius vr vt (label n l))
:
SupportedOscillations sys label (fun (n : ℕ) (x : D) => (SquaredPartition.logCoordinate (q n x), position n x)) Y U
fun (l : ι) (n : ℕ) (p : D × ℝ) (i : Fin 3) =>
PartitionedCovariance.wave
(scale l n p.1 i * PartitionedCovariance.physicalMask d (label n l) (q n p.1) (position n p.1))
(SlotColoring.nativeIndex h (label n l).1) (f l n p.1 i) (mode l n) (phase l n p.1) (Y n p.1) p.2
The actual physical mask automatically supplies the slow-window condition for a covered native wave, with arbitrary phase and amplitude.
The signed tail-label convention used by PrimaryFieldAssembly is
injective and has positive levels for every chosen start N ≥ 1.
The full signed covariance remainder, below CorrectionStep #
noncomputable def
NavierStokes.LabelSumBounds.symmetricCovariance
{D : Type}
(u v : CorrectionState.Oscillation D)
:
Tensor D
Symmetric covariance, given by bilinearCovariance u v + bilinearCovariance v u.
Equations
Instances For
noncomputable def
NavierStokes.LabelSumBounds.signedRemainder
{D : Type}
(primary old tangent curl : CorrectionState.Oscillation D)
:
Tensor D
Definitionally the same five terms used by CorrectionStep.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.LabelSumBounds.AngularContinuous.add
{D : Type}
{u v : CorrectionState.Oscillation D}
(hu : AngularContinuous u)
(hv : AngularContinuous v)
:
AngularContinuous (u + v)
theorem
NavierStokes.LabelSumBounds.AngularContinuous.sub
{D : Type}
{u v : CorrectionState.Oscillation D}
(hu : AngularContinuous u)
(hv : AngularContinuous v)
:
AngularContinuous (u - v)
theorem
NavierStokes.LabelSumBounds.covariance_add_left
{D : Type}
{u v w : CorrectionState.Oscillation D}
(hu : AngularContinuous u)
(hv : AngularContinuous v)
(hw : AngularContinuous w)
:
theorem
NavierStokes.LabelSumBounds.covariance_add_right
{D : Type}
{u v w : CorrectionState.Oscillation D}
(hu : AngularContinuous u)
(hv : AngularContinuous v)
(hw : AngularContinuous w)
:
theorem
NavierStokes.LabelSumBounds.covariance_sub_left
{D : Type}
{u v w : CorrectionState.Oscillation D}
(hu : AngularContinuous u)
(hv : AngularContinuous v)
(hw : AngularContinuous w)
:
theorem
NavierStokes.LabelSumBounds.covariance_sub_right
{D : Type}
{u v w : CorrectionState.Oscillation D}
(hu : AngularContinuous u)
(hv : AngularContinuous v)
(hw : AngularContinuous w)
:
theorem
NavierStokes.LabelSumBounds.signedRemainder_exact
{D : Type}
(primary old tangent curl : CorrectionState.Oscillation D)
(hp : AngularContinuous primary)
(ho : AngularContinuous old)
(ht : AngularContinuous tangent)
(hc : AngularContinuous curl)
:
signedRemainder primary old tangent curl = symmetricCovariance (old - primary) tangent + symmetricCovariance old curl + CorrectionState.bilinearCovariance (tangent + curl) (tangent + curl)
structure
NavierStokes.LabelSumBounds.SameCarrier
{D : Type}
(a b : CorrectionState.HarmonicBlock D)
:
Same carrier data, collecting frequency, phase, angular.
Instances For
noncomputable def
NavierStokes.LabelSumBounds.addBlock
{D : Type}
(a b : CorrectionState.HarmonicBlock D)
:
Add block, given by { a with velocity := fun n i => a.velocity n i + b.velocity n i pressure := fun n => a.pressure n + b.pressure n }.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.LabelSumBounds.subBlock
{D : Type}
(a b : CorrectionState.HarmonicBlock D)
:
Sub block, given by { a with velocity := fun n i => a.velocity n i - b.velocity n i pressure := fun n => a.pressure n - b.pressure n }.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.LabelSumBounds.addBlock_oscillation
{D : Type}
(a b : CorrectionState.HarmonicBlock D)
(h : SameCarrier a b)
:
theorem
NavierStokes.LabelSumBounds.subBlock_oscillation
{D : Type}
(a b : CorrectionState.HarmonicBlock D)
(h : SameCarrier a b)
:
theorem
NavierStokes.LabelSumBounds.addBlock_band
{D : Type}
{a b : CorrectionState.HarmonicBlock D}
{N : ℕ}
(ha : a.BandLimited N)
(hb : b.BandLimited N)
:
(addBlock a b).BandLimited N
theorem
NavierStokes.LabelSumBounds.subBlock_band
{D : Type}
{a b : CorrectionState.HarmonicBlock D}
{N : ℕ}
(ha : a.BandLimited N)
(hb : b.BandLimited N)
:
(subBlock a b).BandLimited N
theorem
NavierStokes.LabelSumBounds.uniform_symmetricCovariance
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α β : ℝ}
(a b : ι → CorrectionState.HarmonicBlock D)
(N : ℕ)
(hband : ∀ (l : ι), (a l).BandLimited N)
(hcarrier : ∀ (l : ι), SameCarrier (a l) (b l))
(ha : ∀ (i : Fin 3) (j : ℤ), UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((a l).velocity n i).coeff j x)
(hb : ∀ (i : Fin 3) (j : ℤ), UniformWaveClass s P β fun (l : ι) (n : ℕ) (x : D) => ((b l).velocity n i).coeff j x)
(hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x)
(hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1)
(hkp : ∀ (l : ι) (n : ℕ), (a l).angularFrequency n ≠ 0)
(i j : Fin 3)
:
UniformMeanClass s (α + β) fun (l : ι) => symmetricCovariance (a l).oscillation (b l).oscillation i j
structure
NavierStokes.LabelSumBounds.SignedFamily
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(P : ι → ℕ → D → ℝ)
(α δ β η : ℝ)
:
Type u_1
Input coefficient bounds with one witness uniform in all spatial labels. The improved old-minus-primary bound is explicitly retained.
- primary : ι → CorrectionState.HarmonicBlock D
Primary of
SignedFamily, of typeι → HarmonicBlock D. - old : ι → CorrectionState.HarmonicBlock D
Old of
SignedFamily, of typeι → HarmonicBlock D. - tangent : ι → CorrectionState.HarmonicBlock D
Tangent of
SignedFamily, of typeι → HarmonicBlock D. - curl : ι → CorrectionState.HarmonicBlock D
Curl of
SignedFamily, of typeι → HarmonicBlock D. - bandwidth : ℕ
Bandwidth of
SignedFamily, of typeℕ. - primary_band (l : ι) : (self.primary l).BandLimited self.bandwidth
- old_band (l : ι) : (self.old l).BandLimited self.bandwidth
- tangent_band (l : ι) : (self.tangent l).BandLimited self.bandwidth
- curl_band (l : ι) : (self.curl l).BandLimited self.bandwidth
- primary_carrier (l : ι) : SameCarrier (self.old l) (self.primary l)
- tangent_carrier (l : ι) : SameCarrier (self.old l) (self.tangent l)
- curl_carrier (l : ι) : SameCarrier (self.old l) (self.curl l)
Instances For
theorem
NavierStokes.LabelSumBounds.SignedFamily.uniform_remainder
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α δ β η γ : ℝ}
(f : SignedFamily s P α δ β η)
(hβη : β ≤ η)
(hγd : γ ≤ δ + β)
(hγc : γ ≤ α + η)
(hγs : γ ≤ 2 * β)
(i j : Fin 3)
:
UniformMeanClass s γ fun (l : ι) =>
signedRemainder (f.primary l).oscillation (f.old l).oscillation (f.tangent l).oscillation (f.curl l).oscillation i j
theorem
NavierStokes.LabelSumBounds.fieldSum_angularContinuous
{ι : Type u_1}
{D : Type}
(labels : ℕ → Finset ι)
(u : ι → CorrectionState.Oscillation D)
(hu : ∀ (l : ι), AngularContinuous (u l))
:
AngularContinuous (fieldSum labels u)
theorem
NavierStokes.LabelSumBounds.supported_signedRemainder_fieldSum_eq
{ι : Type u_1}
{D : Type}
{d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
(labels : ℕ → Finset ι)
(label : ℕ → ι → SlotColoring.Label)
(hinj : ∀ (n : ℕ), Set.InjOn (label n) ↑(labels n))
(hlevel : ∀ (n : ℕ), ∀ l ∈ labels n, 1 ≤ (label n l).1)
(χ : ℕ → D → WindowPoint)
(Y : ℕ → D → TorusInverse.Plane)
{U : Set D}
(p o t c : ι → CorrectionState.Oscillation D)
(hp : ∀ (l : ι), AngularContinuous (p l))
(ho : ∀ (l : ι), AngularContinuous (o l))
(ht : ∀ (l : ι), AngularContinuous (t l))
(hc : ∀ (l : ι), AngularContinuous (c l))
(hsp : SupportedOscillations sys label χ Y U p)
(hso : SupportedOscillations sys label χ Y U o)
(hst : SupportedOscillations sys label χ Y U t)
(hsc : SupportedOscillations sys label χ Y U c)
(n : ℕ)
{x : D}
(hx : x ∈ U)
(i j : Fin 3)
:
signedRemainder (fieldSum labels p) (fieldSum labels o) (fieldSum labels t) (fieldSum labels c) i j n x = ∑ l ∈ labels n, signedRemainder (p l) (o l) (t l) (c l) i j n x
theorem
NavierStokes.LabelSumBounds.signedRemainder_window_support
{ι : Type u_1}
{D : Type}
{d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
{label : ℕ → ι → SlotColoring.Label}
{χ : ℕ → D → WindowPoint}
{Y : ℕ → D → TorusInverse.Plane}
{U : Set D}
{p o t c : ι → CorrectionState.Oscillation D}
(hp : SupportedOscillations sys label χ Y U p)
(ho : SupportedOscillations sys label χ Y U o)
(ht : SupportedOscillations sys label χ Y U t)
(hc : SupportedOscillations sys label χ Y U c)
(l : ι)
(n : ℕ)
{x : D}
(hx : x ∈ U)
(i j : Fin 3)
(hne : signedRemainder (p l) (o l) (t l) (c l) i j n x ≠ 0)
:
theorem
NavierStokes.LabelSumBounds.SignedFamily.remainder_sum_mem
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α δ β η γ : ℝ}
(f : SignedFamily s P α δ β η)
(hβη : β ≤ η)
(hγd : γ ≤ δ + β)
(hγc : γ ≤ α + η)
(hγs : γ ≤ 2 * β)
{d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
(labels : ℕ → Finset ι)
(label : ℕ → ι → SlotColoring.Label)
(hinj : ∀ (n : ℕ), Set.InjOn (label n) ↑(labels n))
(hlevel : ∀ (n : ℕ), ∀ l ∈ labels n, 1 ≤ (label n l).1)
(χ : ℕ → D → WindowPoint)
(hχ : ∀ (n : ℕ), ContinuousOn (χ n) s.domain)
(Y : ℕ → D → TorusInverse.Plane)
(hp : SupportedOscillations sys label χ Y s.domain fun (l : ι) => (f.primary l).oscillation)
(ho : SupportedOscillations sys label χ Y s.domain fun (l : ι) => (f.old l).oscillation)
(ht : SupportedOscillations sys label χ Y s.domain fun (l : ι) => (f.tangent l).oscillation)
(hc : SupportedOscillations sys label χ Y s.domain fun (l : ι) => (f.curl l).oscillation)
(i j : Fin 3)
:
WeightedClasses.MeanClass s γ
(signedRemainder (fieldSum labels fun (l : ι) => (f.primary l).oscillation)
(fieldSum labels fun (l : ι) => (f.old l).oscillation) (fieldSum labels fun (l : ι) => (f.tangent l).oscillation)
(fieldSum labels fun (l : ι) => (f.curl l).oscillation) i j)
The full signed remainder of the actual assembled fields satisfies the fixed target exponent, uniformly over arbitrary finite active label sets. The local overlap bound is independent of stage and total size.
theorem
NavierStokes.LabelSumBounds.uniform_coefficients_of_nonzero
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α : ℝ}
(a : ι → CorrectionState.HarmonicBlock D)
(ha :
∀ (i : Fin 3) (j : ℤ), j ≠ 0 → UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((a l).velocity n i).coeff j x)
(hz : ∀ (l : ι) (n : ℕ) (i : Fin 3), ((a l).velocity n i).coeff 0 = 0)
(hP : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x)
(i : Fin 3)
(j : ℤ)
:
UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((a l).velocity n i).coeff j x
theorem
NavierStokes.LabelSumBounds.covariance_increment_exact
{D : Type}
(u v : CorrectionState.Oscillation D)
(hu : AngularContinuous u)
(hv : AngularContinuous v)
:
theorem
NavierStokes.LabelSumBounds.harmonic_covariance_increment_sum_mem
{ι : Type u_1}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α β : ℝ}
(hαβ : α ≤ β)
{d h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem d h vr vt}
(labels : ℕ → Finset ι)
(label : ℕ → ι → SlotColoring.Label)
(hinj : ∀ (n : ℕ), Set.InjOn (label n) ↑(labels n))
(hlevel : ∀ (n : ℕ), ∀ l ∈ labels n, 1 ≤ (label n l).1)
(χ : ℕ → D → WindowPoint)
(hχ : ∀ (n : ℕ), ContinuousOn (χ n) s.domain)
(Y : ℕ → D → TorusInverse.Plane)
(a b : ι → CorrectionState.HarmonicBlock D)
(N : ℕ)
(hNa : ∀ (l : ι), (a l).BandLimited N)
(hNb : ∀ (l : ι), (b l).BandLimited N)
(hcarrier : ∀ (l : ι), SameCarrier (a l) (b l))
(ha : ∀ (i : Fin 3) (j : ℤ), UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((a l).velocity n i).coeff j x)
(hb : ∀ (i : Fin 3) (j : ℤ), UniformWaveClass s P β fun (l : ι) (n : ℕ) (x : D) => ((b l).velocity n i).coeff j x)
(hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x)
(hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1)
(hkp : ∀ (l : ι) (n : ℕ), (a l).angularFrequency n ≠ 0)
(hsu : SupportedOscillations sys label χ Y s.domain fun (l : ι) => (a l).oscillation)
(hsv : SupportedOscillations sys label χ Y s.domain fun (l : ι) => (b l).oscillation)
(i j : Fin 3)
:
WeightedClasses.MeanClass s (α + β) fun (n : ℕ) (x : D) =>
CorrectionState.bilinearCovariance
((fieldSum labels fun (l : ι) => (a l).oscillation) + fieldSum labels fun (l : ι) => (b l).oscillation)
((fieldSum labels fun (l : ι) => (a l).oscillation) + fieldSum labels fun (l : ι) => (b l).oscillation) i j n x - CorrectionState.bilinearCovariance (fieldSum labels fun (l : ι) => (a l).oscillation)
(fieldSum labels fun (l : ι) => (a l).oscillation) i j n x
The actual exact-minus-principal covariance after adding a supported
curl correction. Taking α=1/2 and β=1-κ gives 3/2-κ, with no factor
depending on the total number of active labels.
Joint-index input estimates and native derivative supports #
theorem
NavierStokes.LabelSumBounds.uniformClass_of_envelopeJets
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{V : PhaseJetBounds.Domain (ℕ × ι) D}
{W : ℕ × ι → D → ℝ}
{a : ℕ × ι → D → E}
(ha : PrimaryPulseBounds.EnvelopeJets V W a)
{w : ι → ℕ → D → ℝ}
{α K : ℝ}
{q : ℕ}
(hK : 1 ≤ K)
(hscale : ∀ (n : ℕ) (l : ι), V.scale (n, l) ≤ K * s.slow n ^ q)
(hdom : ∀ (n : ℕ) (l : ι), s.domain ⊆ V.carrier (n, l))
(hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w l n x)
(hW : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, W (n, l) x ≤ s.epsilon n ^ α * w l n x)
:
UniformClass s w α fun (l : ι) (n : ℕ) => a (n, l)
Joint (band,label) envelope estimates yield the required quantifier
order directly. A uniform polynomial change of slow scale is allowed.
Neither constants nor polynomial degrees are chosen after the label.
theorem
NavierStokes.LabelSumBounds.uniformWaveClass_of_envelopeJets
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{V : PhaseJetBounds.Domain (ℕ × ι) D}
{W : ℕ × ι → D → ℝ}
{a : ℕ × ι → D → E}
(ha : PrimaryPulseBounds.EnvelopeJets V W a)
{P : ι → ℕ → D → ℝ}
{α K : ℝ}
{q : ℕ}
(hK : 1 ≤ K)
(hscale : ∀ (n : ℕ) (l : ι), V.scale (n, l) ≤ K * s.slow n ^ q)
(hdom : ∀ (n : ℕ) (l : ι), s.domain ⊆ V.carrier (n, l))
(hP : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x)
(hW : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, W (n, l) x ≤ s.epsilon n ^ α * (√(s.zeta x) * P l n x))
:
UniformWaveClass s P α fun (l : ι) (n : ℕ) => a (n, l)
theorem
NavierStokes.LabelSumBounds.uniformClass_of_polynomialJets
{ι : Type u_1}
{E : Type u_3}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{V : PhaseJetBounds.Domain (ℕ × ι) D}
{a : ℕ × ι → D → E}
(ha : PhaseJetBounds.PolynomialJets V a)
{K : ℝ}
{q : ℕ}
(hK : 1 ≤ K)
(hscale : ∀ (n : ℕ) (l : ι), V.scale (n, l) ≤ K * s.slow n ^ q)
(hdom : ∀ (n : ℕ) (l : ι), s.domain ⊆ V.carrier (n, l))
:
theorem
NavierStokes.LabelSumBounds.slotSet_isCompact
(h r : ℝ)
(vr vt : TorusInverse.Plane)
(l : SlotColoring.Label)
:
IsCompact (PartitionedCovariance.slotSet h r vr vt l)
theorem
NavierStokes.LabelSumBounds.native_jet_tsupport_subset
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{h r : ℝ}
{vr vt : TorusInverse.Plane}
{l : SlotColoring.Label}
{f : TorusInverse.Plane → E}
(hf : Function.support f ⊆ PartitionedCovariance.slotSet h r vr vt l)
(m : ℕ)
:
tsupport (iteratedFDeriv ℝ m f) ⊆ PartitionedCovariance.slotSet h r vr vt l
Native derivatives stay inside the same closed padded slot, including
entry and exit. Periodizing such a derivative can therefore reuse
PartitionedCovariance.covered_support and the original slot separation.