Uniform primary weights and curl estimates

A single enumeration of the joint band/label index transfers the existing weighted analysis without losing any inverse-edge factors. The reindexed strip retains the same domain, edge distance, and vanishing weight. Every constant is chosen before both the original band and the label.

noncomputable def NavierStokes.UniformPrimaryWeights.reindexedStrip {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (e : ℕ → ℕ × ι) : WeightedClasses.StripData D

Only the discrete scales are reindexed. The spatial edge geometry and its possibly vanishing weight are exactly the original ones.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.UniformPrimaryWeights.pull {ι : Type u_1} {E : Type u_2} {D : Type} (e : ℕ → ℕ × ι) (f : ι → ℕ → D → E) : ℕ → D → E

Pull, defined pointwise by f (e k).2 (e k).1.

Equations

• NavierStokes.UniformPrimaryWeights.pull e f k = f (e k).2 (e k).1

@[simp]

theorem NavierStokes.UniformPrimaryWeights.reindexed_growth {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (e : ℕ → ℕ × ι) (k : ℕ) (x : D) : (reindexedStrip s e).growth k x = s.growth (e k).1 x

@[simp]

theorem NavierStokes.UniformPrimaryWeights.reindexed_majorant {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (e : ℕ → ℕ × ι) (w : ι → ℕ → D → ℝ) (α C : ℝ) (p k : ℕ) (x : D) : WeightedClasses.majorant (reindexedStrip s e) (pull e w) α C p k x = WeightedClasses.majorant s (w (e k).2) α C p (e k).1 x

theorem NavierStokes.UniformPrimaryWeights.pull_class {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformClass s w α f) (e : ℕ → ℕ × ι) : WeightedClasses.MemClass (reindexedStrip s e) (pull e w) α (pull e f)

theorem NavierStokes.UniformPrimaryWeights.uniform_of_pull {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {f : ι → ℕ → D → E} {e : ℕ → ℕ × ι} (he : Function.Surjective e) (hf : WeightedClasses.MemClass (reindexedStrip s e) (pull e w) α (pull e f)) : LabelSumBounds.UniformClass s w α f

Surjectivity is the reason the constants also control every original label. It is never replaced by a separate bound for each label.

noncomputable def NavierStokes.UniformPrimaryWeights.enumeration (ι : Type u_5) [Countable ι] [Nonempty ι] : ℕ → ℕ × ι

Enumeration, given by Classical.choose (exists_surjective_nat (ℕ × ι)).

Equations

• NavierStokes.UniformPrimaryWeights.enumeration ι = Classical.choose ⋯

theorem NavierStokes.UniformPrimaryWeights.enumeration_surjective (ι : Type u_5) [Countable ι] [Nonempty ι] : Function.Surjective (enumeration ι)

noncomputable def NavierStokes.UniformPrimaryWeights.jointDomain {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) : PhaseJetBounds.Domain (ℕ × ι) D

The actual slow scale on the joint index, in the (band,label) order used by the phase and ODE constructions.

Equations

• NavierStokes.UniformPrimaryWeights.jointDomain s = { scale := fun (q : ℕ × ι) => s.slow q.1, carrier := fun (x : ℕ × ι) => s.domain, isOpen := ⋯, one_le_scale := ⋯ }

theorem NavierStokes.UniformPrimaryWeights.pull_polynomial {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {f : ι → ℕ → D → E} (hf : PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) => f q.2 q.1) (e : ℕ → ℕ × ι) : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain (reindexedStrip s e)) (pull e f)

theorem NavierStokes.UniformPrimaryWeights.polynomial_on_joint {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {V : PhaseJetBounds.Domain (ℕ × ι) D} {f : ℕ × ι → D → E} (hf : PhaseJetBounds.PolynomialJets V f) {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)) : PhaseJetBounds.PolynomialJets (jointDomain s) f

Restrict genuine joint phase/ODE jets to the common strip, allowing a uniform polynomial change of slow scale.

noncomputable def NavierStokes.UniformPrimaryWeights.UniformInverseControl {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (w g : ι → ℕ → D → ℝ) : Prop

This version retains the full inverse-edge polynomial in the majorant; it is not a polynomial-in-S replacement of the weight.

Equations

• NavierStokes.UniformPrimaryWeights.UniformInverseControl s w g = ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, w l n x / g l n x ≤ C * s.growth n x ^ p

theorem NavierStokes.UniformPrimaryWeights.pull_inverseControl {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w g : ι → ℕ → D → ℝ} (h : UniformInverseControl s w g) (e : ℕ → ℕ × ι) : SignedCovariance.InverseControl (reindexedStrip s e) (pull e w) (pull e g)

theorem NavierStokes.UniformPrimaryWeights.inverseControl_of_lower {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w g : ι → ℕ → D → ℝ} (hg : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 < g l n x) {c : ℝ} (hc : 0 < c) (p : ℕ) (hlower : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, c * w l n x / s.growth n x ^ p ≤ g l n x) : UniformInverseControl s w g

theorem NavierStokes.UniformPrimaryWeights.sqrt_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} {w g : ι → ℕ → D → ℝ} (hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 < w l n x) (hp : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 < g l n x) (hg : LabelSumBounds.UniformClass s w 0 g) (hlower : UniformInverseControl s w g) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => √(w l n x)) 0 fun (l : ι) (n : ℕ) (x : D) => √(g l n x)

Positivity is pointwise on the open strip. There is no positive minimum of the weight, even when it vanishes at the boundary.

theorem NavierStokes.UniformPrimaryWeights.signed_quotient_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} {w g r : ι → ℕ → D → ℝ} {β : ℝ} (hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 < w l n x) (hp : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 < g l n x) (hg : LabelSumBounds.UniformClass s w 0 g) (hr : LabelSumBounds.UniformClass s w β r) (hlower : UniformInverseControl s w g) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => √(w l n x)) β fun (l : ι) (n : ℕ) (x : D) => r l n x / (2 * √(g l n x))

theorem NavierStokes.UniformPrimaryWeights.fderiv_class {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) => fderiv ℝ (f l n)

theorem NavierStokes.UniformPrimaryWeights.smul_class {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w v : ι → ℕ → D → ℝ} {α β : ℝ} {a : ι → ℕ → D → ℝ} {f : ι → ℕ → D → E} (ha : LabelSumBounds.UniformClass s v β a) (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => v l n x * w l n x) (β + α) fun (l : ι) (n : ℕ) (x : D) => a l n x • f l n x

theorem NavierStokes.UniformPrimaryWeights.mul_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w v : ι → ℕ → D → ℝ} {α β : ℝ} {a b : ι → ℕ → D → ℝ} (ha : LabelSumBounds.UniformClass s w α a) (hb : LabelSumBounds.UniformClass s v β b) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => w l n x * v l n x) (α + β) fun (l : ι) (n : ℕ) (x : D) => a l n x * b l n x

theorem NavierStokes.UniformPrimaryWeights.real_smul_class {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α β : ℝ} {a : ι → ℕ → D → ℝ} {f : ι → ℕ → D → E} (ha : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) β a) (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass s w (β + α) fun (l : ι) (n : ℕ) (x : D) => a l n x • f l n x

theorem NavierStokes.UniformPrimaryWeights.along_class {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α β : ℝ} {V : ι → ℕ → D → D} {f : ι → ℕ → D → E} (hV : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) β V) (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass s w (α + β) fun (l : ι) (n : ℕ) => HarmonicCalculus.along (V l n) (f l n)

theorem NavierStokes.UniformPrimaryWeights.class_of_single {ι : Type u_1} {E : Type u_2} {D : Type} [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 : ι) => w) α fun (x : ι) => f

noncomputable def NavierStokes.UniformPrimaryWeights.UniformBandBound {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (β : ℝ) (a : ι → ℕ → ℝ) : Prop

Uniform band bound, given by `∃ C : ℝ, 0 ≤ C ∧ ∃ p : ℕ, ∀ l n, ‖a l n‖ ≤ C * s.epsilon n ^ β

• s.slow n ^ p`.

Equations

• NavierStokes.UniformPrimaryWeights.UniformBandBound s β a = ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ), ‖a l n‖ ≤ C * s.epsilon n ^ β * s.slow n ^ p

theorem NavierStokes.UniformPrimaryWeights.pull_bandBound {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {β : ℝ} {a : ι → ℕ → ℝ} (ha : UniformBandBound s β a) (e : ℕ → ℕ × ι) : WeightedClasses.BandBound (reindexedStrip s e) β fun (k : ℕ) => a (e k).2 (e k).1

theorem NavierStokes.UniformPrimaryWeights.band_smul_class {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α β : ℝ} [Countable ι] [Nonempty ι] {a : ι → ℕ → ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformClass s w α f) (ha : UniformBandBound s β a) : LabelSumBounds.UniformClass s w (α + β) fun (l : ι) (n : ℕ) (x : D) => a l n • f l n x

theorem NavierStokes.UniformPrimaryWeights.polynomial_class {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {f : ι → ℕ → D → E} (hf : PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) => f q.2 q.1) : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 f

theorem NavierStokes.UniformPrimaryWeights.covariance_weights_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} {r : ι → ℕ → ℝ} {H : ι → ℕ → D → SmoothCovariance.Mat2} {T : ι → ℕ → D → SmoothCovariance.Vec2} {w : ι → ℕ → D → ℝ} (hr : PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) (x : D) => r q.2 q.1) (hrne : ∀ (l : ι) (n : ℕ), r l n ≠ 0) (hH : ∀ (i j : Fin 2), PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) (x : D) => H q.2 q.1 x i j) (hT : ∀ (i : Fin 2), LabelSumBounds.UniformClass s w 0 fun (l : ι) (n : ℕ) (x : D) => T l n x i) {b M : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hdet : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (r l n) (H l n x))|) (hentry : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |r l n * H l n x i j| ≤ M) (j : Fin 2) : LabelSumBounds.UniformClass s w 0 fun (l : ι) (n : ℕ) (x : D) => SmoothCovariance.weights (H l n x) (T l n x) j

The inverse matrix is differentiated after reindexing the genuine integrated entries. The determinant gap and entry bound are common to all labels; the target retains its full vanishing weight.

theorem NavierStokes.UniformPrimaryWeights.covariance_amplitudes_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} {r : ι → ℕ → ℝ} {H : ι → ℕ → D → SmoothCovariance.Mat2} {T : ι → ℕ → D → SmoothCovariance.Vec2} {w : ι → ℕ → D → ℝ} (hr : PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) (x : D) => r q.2 q.1) (hrne : ∀ (l : ι) (n : ℕ), r l n ≠ 0) (hH : ∀ (i j : Fin 2), PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) (x : D) => H q.2 q.1 x i j) (hT : ∀ (i : Fin 2), LabelSumBounds.UniformClass s w 0 fun (l : ι) (n : ℕ) (x : D) => T l n x i) {b M c : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hc : 0 < c) (hdet : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (r l n) (H l n x))|) (hentry : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |r l n * H l n x i j| ≤ M) (hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 < w l n x) (hlower : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ (j : Fin 2), c * w l n x ≤ SmoothCovariance.weights (H l n x) (T l n x) j) (j : Fin 2) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => √(w l n x)) 0 fun (l : ι) (n : ℕ) (x : D) => SmoothCovariance.amplitudes (H l n x) (T l n x) j

theorem NavierStokes.UniformPrimaryWeights.sqrt_slow_polynomial {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) : PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) (x : D) => √(s.slow q.1)

The exact normalization used by the primary covariance.

theorem NavierStokes.UniformPrimaryWeights.primaryCoefficient_waveClass {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {H : ι → ℕ → D → SmoothCovariance.Mat2} {T : ι → ℕ → D → SmoothCovariance.Vec2} {mask : ι → ℕ → D → ℝ} {v : ι → ℕ → D → ProblemStatement.Space} (hH : ∀ (i j : Fin 2), PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) (x : D) => H q.2 q.1 x i j) (hT : ∀ (i : Fin 2), LabelSumBounds.UniformMeanClass s 0 fun (l : ι) (n : ℕ) (x : D) => T l n x i) (hmask : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 mask) (hv : LabelSumBounds.UniformClass s P 0 v) {b M c : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hc : 0 < c) (hdet : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (√(s.slow n)) (H l n x))|) (hentry : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |√(s.slow n) * H l n x i j| ≤ M) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hlower : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ (j : Fin 2), c * s.zeta x ≤ SmoothCovariance.weights (H l n x) (T l n x) j) (j : Fin 2) : LabelSumBounds.UniformWaveClass s P (1 / 2) fun (l : ι) => PrimaryPulseBounds.primaryCoefficient s (H l) (T l) (mask l) (v l) j

theorem NavierStokes.UniformPrimaryWeights.component_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {a : ι → ℕ → D → CurlClassBounds.ComplexVector} (ha : LabelSumBounds.UniformClass s w α a) (i : Fin 3) : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => a l n x i

theorem NavierStokes.UniformPrimaryWeights.vector_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {a : ι → ℕ → D → CurlClassBounds.ComplexVector} (ha : ∀ (i : Fin 3), LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => a l n x i) : LabelSumBounds.UniformClass s w α a

theorem NavierStokes.UniformPrimaryWeights.normalCoefficient_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} [Countable ι] [Nonempty ι] {N : ι → ℕ → D → CurlClassBounds.RealVector} {a : ι → ℕ → D → CurlClassBounds.ComplexVector} (hN : PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) => N q.2 q.1) (ha : LabelSumBounds.UniformClass s w α a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖N l n x‖) (hupper : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ‖N l n x‖ ≤ M) : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => CurlClassBounds.normalCoefficient (N l n x) (a l n x)

The normal inverse is computed from the actual jointly bounded normal, not supplied as a separately bounded potential coefficient.

theorem NavierStokes.UniformPrimaryWeights.cylindricalCurl_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α κ : ℝ} {R : ι → ℕ → D → ℝ} {Vr Vθ Vz : ι → ℕ → D → D} {a : ι → ℕ → D → CurlClassBounds.ComplexVector} (ha : LabelSumBounds.UniformClass s w α a) (hκ : 0 ≤ κ) (hr : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) (-κ) Vr) (hθ : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 Vθ) (hz : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 1 Vz) (hR : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 fun (l : ι) (n : ℕ) (x : D) => (R l n x)⁻¹) : LabelSumBounds.UniformClass s w (α - κ) fun (l : ι) (n : ℕ) => CurlClassBounds.cylindricalCurl (R l n) (Vr l n) (Vθ l n) (Vz l n) (a l n)

This version permits radius and direction fields to vary with both band and label. All cylindrical connection terms are retained.

theorem NavierStokes.UniformPrimaryWeights.curlRemainder_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α κ : ℝ} [Countable ι] [Nonempty ι] {R : ι → ℕ → D → ℝ} {Vr Vθ Vz : ι → ℕ → D → D} {K : ι → ℕ → ℝ} {a : ι → ℕ → D → CurlClassBounds.ComplexVector} (ha : LabelSumBounds.UniformClass s w α a) (hκ : 0 ≤ κ) (hr : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) (-κ) Vr) (hθ : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 Vθ) (hz : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 1 Vz) (hR : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 fun (l : ι) (n : ℕ) (x : D) => (R l n x)⁻¹) (hK : UniformBandBound s (1 / 2) fun (l : ι) (n : ℕ) => 1 / K l n) : LabelSumBounds.UniformClass s w (α + 1 / 2 - κ) fun (l : ι) (n : ℕ) => CurlClassBounds.curlRemainder (K l n) (R l n) (Vr l n) (Vθ l n) (Vz l n) (a l n)

theorem NavierStokes.UniformPrimaryWeights.normalCurlRemainder_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α κ : ℝ} [Countable ι] [Nonempty ι] {R : ι → ℕ → D → ℝ} {Vr Vθ Vz : ι → ℕ → D → D} {K : ι → ℕ → ℝ} {N : ι → ℕ → D → CurlClassBounds.RealVector} {a : ι → ℕ → D → CurlClassBounds.ComplexVector} (hN : PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) => N q.2 q.1) (ha : LabelSumBounds.UniformClass s w α a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖N l n x‖) (hupper : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ‖N l n x‖ ≤ M) (hκ : 0 ≤ κ) (hr : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) (-κ) Vr) (hθ : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 Vθ) (hz : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 1 Vz) (hR : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 fun (l : ι) (n : ℕ) (x : D) => (R l n x)⁻¹) (hK : UniformBandBound s (1 / 2) fun (l : ι) (n : ℕ) => 1 / K l n) : LabelSumBounds.UniformClass s w (α + 1 / 2 - κ) fun (l : ι) (n : ℕ) => CurlClassBounds.curlRemainder (K l n) (R l n) (Vr l n) (Vθ l n) (Vz l n) fun (x : D) => CurlClassBounds.normalCoefficient (N l n x) (a l n x)

theorem NavierStokes.UniformPrimaryWeights.harmonic_inverse_bandBound {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (j : ι → ℕ → ℤ) (hj : ∀ (l : ι) (n : ℕ), j l n ≠ 0) : UniformBandBound s (1 / 2) fun (l : ι) (n : ℕ) => 1 / (CurlClassBounds.carrierFrequency s n * ↑(j l n))

The half-power frequency gain is uniform even when the nonzero integer harmonic varies with the label.

noncomputable def NavierStokes.UniformPrimaryWeights.phaseMatrix {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ × ι → ℝ) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) : ι → ℕ → D → SmoothCovariance.Mat2

The same actual integrated pulse matrix, now indexed jointly by band and label. Its entries are not independent input functions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.UniformPrimaryWeights.phaseFundamental {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (j : Fin 2) : ι → ℕ → D → ProblemStatement.Space

Phase fundamental, defined pointwise by normalizedPulse ((A j).frame (n, l)) ((A j).lam (n, l)) ((A j).u (n, l)) ((A j).L (n, l)) (χ (n, l) x).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.UniformPrimaryWeights.phaseEnvelope {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (j : Fin 2) : ι → ℕ → D → ℝ

Phase envelope, defined pointwise by referenceP ((A j).lam (n, l)) ((A j).u (n, l)) ((A j).L (n, l)) ((A j).L (n, l) * (χ (n, l) x).2).

Equations

• NavierStokes.UniformPrimaryWeights.phaseEnvelope A χ j l n x = NavierStokes.PrimaryPulseBounds.referenceP ((A j).lam (n, l)) ((A j).u (n, l)) ((A j).L (n, l)) ((A j).L (n, l) * (χ (n, l) x).2)

noncomputable def NavierStokes.UniformPrimaryWeights.phaseCutoffFundamental {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (j : Fin 2) : ι → ℕ → D → ProblemStatement.Space

Phase cutoff fundamental, defined pointwise by cutoffPulse ((A j).frame (n, l)) ((A j).lam (n, l)) ((A j).u (n, l)) ((A j).L (n, l)) (χ (n, l) x).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.UniformPrimaryWeights.phaseSlotEnvelope {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (j : Fin 2) : ι → ℕ → D → ℝ

Phase slot envelope, defined pointwise by GaussianTailFlat.referenceSlotEnvelope ((A j).lam (n, l)) ((A j).u (n, l)) ((A j).L (n, l)) (χ (n, l) x).2.

Equations

• NavierStokes.UniformPrimaryWeights.phaseSlotEnvelope A χ j l n x = NavierStokes.GaussianTailFlat.referenceSlotEnvelope ((A j).lam (n, l)) ((A j).u (n, l)) ((A j).L (n, l)) (χ (n, l) x).2

theorem NavierStokes.UniformPrimaryWeights.phaseMatrix_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} {s : WeightedClasses.StripData D} (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ × ι → ℝ) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (hscale : ∀ (q : ℕ × ι), U.scale q = s.slow q.1) (hχ : PhaseJetBounds.PolynomialJets (jointDomain s) χ) (hmap : ∀ (q : ℕ × ι), ∀ x ∈ s.domain, (χ q x).1 ∈ U.carrier q) (hpref : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets U fun (q : ℕ × ι) (x : PhaseCalculus.Slow) => pref j q) (i j : Fin 2) : PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) (x : D) => phaseMatrix A pref χ q.2 q.1 x i j

The matrix jets come from the actual parameter-dependent ODE and its actual middle-cutoff covariance integral, uniformly in both indices.

theorem NavierStokes.UniformPrimaryWeights.phaseFundamental_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} {s : WeightedClasses.StripData D} (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (hscale : ∀ (q : ℕ × ι), U.scale q = s.slow q.1) (hχ : PhaseJetBounds.PolynomialJets (jointDomain s) χ) (hmap : ∀ (q : ℕ × ι), ∀ x ∈ s.domain, χ q x ∈ U.carrier q ×ˢ Set.Ioo 0 1) (j : Fin 2) : LabelSumBounds.UniformClass s (phaseEnvelope A χ j) 0 (phaseFundamental A χ j)

theorem NavierStokes.UniformPrimaryWeights.phaseCutoffFundamental_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} {s : WeightedClasses.StripData D} (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (hscale : ∀ (q : ℕ × ι), U.scale q = s.slow q.1) (hχ : PhaseJetBounds.PolynomialJets (jointDomain s) χ) (hmap : ∀ (q : ℕ × ι), ∀ x ∈ s.domain, (χ q x).1 ∈ U.carrier q) (j : Fin 2) : LabelSumBounds.UniformClass s (phaseSlotEnvelope A χ j) 0 (phaseCutoffFundamental A χ j)

The actual smooth cutoff extension is controlled by the original Gaussian slot envelope, including its zero region.

theorem NavierStokes.UniformPrimaryWeights.phaseNormal_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} {s : WeightedClasses.StripData D} (A : PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (hscale : ∀ (q : ℕ × ι), U.scale q = s.slow q.1) (hχ : PhaseJetBounds.PolynomialJets (jointDomain s) χ) (hmap : ∀ (q : ℕ × ι), ∀ x ∈ s.domain, χ q x ∈ (U.slot A.V ⋯).carrier q) : (PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) (x : D) => A.phase.normal q (χ q x)) ∧ (∀ (q : ℕ × ι), ∀ x ∈ s.domain, A.b ≤ ‖A.phase.normal q (χ q x)‖) ∧ ∀ (q : ℕ × ι), ∀ x ∈ s.domain, ‖A.phase.normal q (χ q x)‖ ≤ A.M ^ 2 + 3 * A.M

Normal derivatives and the separated range are derived from the same joint phase data. The phase chart uses its actual unnormalized slot variable.

theorem NavierStokes.UniformPrimaryWeights.phase_primary_waveClass {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ × ι → ℝ) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (T : ι → ℕ → D → SmoothCovariance.Vec2) (mask : ι → ℕ → D → ℝ) (hscale : ∀ (q : ℕ × ι), U.scale q = s.slow q.1) (hχ : PhaseJetBounds.PolynomialJets (jointDomain s) χ) (hmap : ∀ (q : ℕ × ι), ∀ x ∈ s.domain, χ q x ∈ U.carrier q ×ˢ Set.Ioo 0 1) (hpref : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets U fun (q : ℕ × ι) (x : PhaseCalculus.Slow) => pref j q) (hT : ∀ (i : Fin 2), LabelSumBounds.UniformMeanClass s 0 fun (l : ι) (n : ℕ) (x : D) => T l n x i) (hmask : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 mask) {b M c : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hc : 0 < c) (hdet : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (√(s.slow n)) (phaseMatrix A pref χ l n x))|) (hentry : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |√(s.slow n) * phaseMatrix A pref χ l n x i j| ≤ M) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hlower : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ (j : Fin 2), c * s.zeta x ≤ SmoothCovariance.weights (phaseMatrix A pref χ l n x) (T l n x) j) (j : Fin 2) : LabelSumBounds.UniformWaveClass s (phaseEnvelope A χ j) (1 / 2) fun (l : ι) => PrimaryPulseBounds.primaryCoefficient s (phaseMatrix A pref χ l) (T l) (mask l) (phaseFundamental A χ j l) j

Uniform primary class from the actual joint phase/ODE construction. Only order-zero covariance separation and target data remain explicit.

theorem NavierStokes.UniformPrimaryWeights.cut_curl_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α κ : ℝ} (a : ι → LinearWaveBounds.WaveCoefficients D) (d : ι → LinearWaveBounds.GraphDirections D) (ψ : ι → ℕ → D → ℝ) (ha : LabelSumBounds.UniformWaveClass s P α fun (l : ι) => (a l).amplitude) (hψ : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 ψ) (hN : PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) => (a q.2).normal s (d q.2) q.1) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖(a l).normal s (d l) n x‖) (hupper : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ‖(a l).normal s (d l) n x‖ ≤ M) (hκ : 0 ≤ κ) (hr : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) (-κ) fun (l : ι) => (d l).radialField) (hθ : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 fun (l : ι) (x : ℕ) (x_1 : D) => (d l).angular) (hz : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 1 fun (l : ι) => (d l).axialField s) (hR : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 fun (l : ι) (n : ℕ) (x : D) => ((a l).radius n x)⁻¹) (hK : UniformBandBound s (1 / 2) fun (l : ι) (n : ℕ) => 1 / (a l).frequency n) : LabelSumBounds.UniformWaveClass s P (α + 1 / 2 - κ) fun (l : ι) => ((a l).withCutoff (ψ l)).curlCorrection s (d l)

Direct binding to the actual externally-cut LinearWaveBounds coefficient. The cutoff occurs exactly once and every geometric class is uniform in the label.

theorem NavierStokes.UniformPrimaryWeights.phase_cutoff_coefficient_eq {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} (s : WeightedClasses.StripData D) (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ × ι → ℝ) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (T : ι → ℕ → D → SmoothCovariance.Vec2) (mask : ι → ℕ → D → ℝ) (j : Fin 2) (l : ι) (n : ℕ) (x : D) : PrimaryPulseBounds.primaryCoefficient s (phaseMatrix A pref χ l) (T l) (mask l) (phaseCutoffFundamental A χ j l) j n x = GaussianTailFlat.profile (χ (n, l) x).2 • PrimaryPulseBounds.primaryCoefficient s (phaseMatrix A pref χ l) (T l) (mask l) (phaseFundamental A χ j l) j n x

The Gaussian profile appears once in the actual coefficient.

theorem NavierStokes.UniformPrimaryWeights.phase_cutoff_primary_waveClass {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain (ℕ × ι) PhaseCalculus.Slow} [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} (A : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ × ι → ℝ) (χ : ℕ × ι → D → PhaseCalculus.Slow × ℝ) (T : ι → ℕ → D → SmoothCovariance.Vec2) (mask : ι → ℕ → D → ℝ) (hscale : ∀ (q : ℕ × ι), U.scale q = s.slow q.1) (hχ : PhaseJetBounds.PolynomialJets (jointDomain s) χ) (hmap : ∀ (q : ℕ × ι), ∀ x ∈ s.domain, (χ q x).1 ∈ U.carrier q) (hpref : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets U fun (q : ℕ × ι) (x : PhaseCalculus.Slow) => pref j q) (hT : ∀ (i : Fin 2), LabelSumBounds.UniformMeanClass s 0 fun (l : ι) (n : ℕ) (x : D) => T l n x i) (hmask : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 mask) {b M c : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hc : 0 < c) (hdet : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (√(s.slow n)) (phaseMatrix A pref χ l n x))|) (hentry : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |√(s.slow n) * phaseMatrix A pref χ l n x i j| ≤ M) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hlower : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ (j : Fin 2), c * s.zeta x ≤ SmoothCovariance.weights (phaseMatrix A pref χ l n x) (T l n x) j) (j : Fin 2) : LabelSumBounds.UniformWaveClass s (phaseSlotEnvelope A χ j) (1 / 2) fun (l : ι) => PrimaryPulseBounds.primaryCoefficient s (phaseMatrix A pref χ l) (T l) (mask l) (phaseCutoffFundamental A χ j l) j

Global slot-cutoff primary estimate: the actual cutoff extension and its Gaussian envelope both vanish outside the slot. The edge weight is still exactly sqrt zeta.

theorem NavierStokes.UniformPrimaryWeights.curlCorrection_class {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α κ : ℝ} (a : ι → LinearWaveBounds.WaveCoefficients D) (d : ι → LinearWaveBounds.GraphDirections D) (ha : LabelSumBounds.UniformWaveClass s P α fun (l : ι) => (a l).amplitude) (hN : PhaseJetBounds.PolynomialJets (jointDomain s) fun (q : ℕ × ι) => (a q.2).normal s (d q.2) q.1) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖(a l).normal s (d l) n x‖) (hupper : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ‖(a l).normal s (d l) n x‖ ≤ M) (hκ : 0 ≤ κ) (hr : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) (-κ) fun (l : ι) => (d l).radialField) (hθ : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 fun (l : ι) (x : ℕ) (x_1 : D) => (d l).angular) (hz : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 1 fun (l : ι) => (d l).axialField s) (hR : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : D) => 1) 0 fun (l : ι) (n : ℕ) (x : D) => ((a l).radius n x)⁻¹) (hK : UniformBandBound s (1 / 2) fun (l : ι) (n : ℕ) => 1 / (a l).frequency n) : LabelSumBounds.UniformWaveClass s P (α + 1 / 2 - κ) fun (l : ι) => (a l).curlCorrection s (d l)

Apply this directly to a.withCutoff when the stronger Gaussian slot-envelope bound has already been derived for its actual amplitude.

theorem NavierStokes.UniformPrimaryWeights.primary_curl_exponent {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {κ : ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformWaveClass s P (1 / 2 + 1 / 2 - κ) f) : LabelSumBounds.UniformWaveClass s P (1 - κ) f

The primary half-power yields the advertised 1-kappa curl bound.

theorem NavierStokes.UniformPrimaryWeights.primary_curl_budget {ι : Type u_1} {E : Type u_2} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {κ : ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformWaveClass s P (1 - κ) f) (hκ : κ ≤ 8 / 25) : LabelSumBounds.UniformWaveClass s P (17 / 25) f