All-jet bounds for actual nonlinear wave interactions

Only stripped coefficients are placed in the weighted classes. The carrier is retained in the exact differential identities and is removed before estimating.

theorem NavierStokes.WaveInteractionBounds.class_congr {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (hfg : ∀ (n : ℕ), Set.EqOn (f n) (g n) s.domain) : WeightedClasses.MemClass s w α g

theorem NavierStokes.WaveInteractionBounds.class_neg {D : 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) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => -f n x

theorem NavierStokes.WaveInteractionBounds.class_sub {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (hg : WeightedClasses.MemClass s w α g) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => f n x - g n x

theorem NavierStokes.WaveInteractionBounds.class_cmul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w v : ℕ → D → ℝ} {α β : ℝ} {f g : ℕ → D → ℂ} (hf : WeightedClasses.MemClass s w α f) (hg : WeightedClasses.MemClass s v β g) : WeightedClasses.MemClass s (fun (n : ℕ) (x : D) => w n x * v n x) (α + β) fun (n : ℕ) (x : D) => f n x * g n x

theorem NavierStokes.WaveInteractionBounds.class_conj {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → ℂ} (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => star (f n x)

theorem NavierStokes.WaveInteractionBounds.class_const_cmul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → ℂ} (hf : WeightedClasses.MemClass s w α f) (c : ℂ) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => c * f n x

theorem NavierStokes.WaveInteractionBounds.unweighted_cmul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {f g : ℕ → D → ℂ} (hf : WeightedClasses.UnweightedClass s α f) (hg : WeightedClasses.MemClass s w β g) : WeightedClasses.MemClass s w (α + β) fun (n : ℕ) (x : D) => f n x * g n x

theorem NavierStokes.WaveInteractionBounds.mean_wave_cmul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β : ℝ} {f g : ℕ → D → ℂ} (hf : WeightedClasses.MeanClass s α f) (hg : WeightedClasses.WaveClass s P β g) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) : WeightedClasses.WaveClass s P (α + β) fun (n : ℕ) (x : D) => f n x * g n x

theorem NavierStokes.WaveInteractionBounds.wave_mean_cmul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β : ℝ} {f g : ℕ → D → ℂ} (hf : WeightedClasses.WaveClass s P α f) (hg : WeightedClasses.MeanClass s β g) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) : WeightedClasses.WaveClass s P (α + β) fun (n : ℕ) (x : D) => f n x * g n x

theorem NavierStokes.WaveInteractionBounds.wave_cmul_mean {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β : ℝ} {f g : ℕ → D → ℂ} (hf : WeightedClasses.WaveClass s P α f) (hg : WeightedClasses.WaveClass s P β g) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : WeightedClasses.MeanClass s (α + β) fun (n : ℕ) (x : D) => f n x * g n x

theorem NavierStokes.WaveInteractionBounds.wave_cmul_wave {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β : ℝ} {f g : ℕ → D → ℂ} (hf : WeightedClasses.WaveClass s P α f) (hg : WeightedClasses.WaveClass s P β g) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : WeightedClasses.WaveClass s P (α + β) fun (n : ℕ) (x : D) => f n x * g n x

theorem NavierStokes.WaveInteractionBounds.class_along {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → E} {V : ℕ → D → D} (hf : WeightedClasses.MemClass s w α f) (hV : WeightedClasses.UnweightedClass s β V) : WeightedClasses.MemClass s w (α + β) fun (n : ℕ) => HarmonicCalculus.along (V n) (f n)

Evaluation of the actual derivative field at an actual vector field.

theorem NavierStokes.WaveInteractionBounds.bandBound_const {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (c : ℝ) : WeightedClasses.BandBound s 0 fun (x : ℕ) => c

structure NavierStokes.WaveInteractionBounds.Geometry {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (κ : ℝ) : Type u_1

Actual geometric coefficient fields, rather than assumed derivative closure.

• radius : ℕ → D → ℝ

  Radius of Geometry, of type ℕ → D → ℝ.

• radial : ℕ → D → D

  Radial of Geometry, of type ℕ → D → D.

• angular : ℕ → D → D

  Angular of Geometry, of type ℕ → D → D.

• axial : ℕ → D → D

  Axial of Geometry, of type ℕ → D → D.

• radius_pos (n : ℕ) (x : D) : x ∈ s.domain → 0 < self.radius n x
• radial_class : WeightedClasses.UnweightedClass s (-κ) self.radial
• axial_class : WeightedClasses.UnweightedClass s 1 self.axial
• inverse_radius_class : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (self.radius n x)⁻¹

theorem NavierStokes.WaveInteractionBounds.graph_vector_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} {M : ℕ → ℝ} {a : D → ℝ} (hκ : 0 ≤ κ) (hM : WeightedClasses.BandBound s (-κ) M) (ha : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) => a) (e v : D) : WeightedClasses.UnweightedClass s (-κ) fun (n : ℕ) (x : D) => e + M n • a x • v

theorem NavierStokes.WaveInteractionBounds.axial_vector_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (v : D) : WeightedClasses.UnweightedClass s 1 fun (n : ℕ) (x : D) => s.epsilon n • v

@[reducible, inline]

abbrev NavierStokes.WaveInteractionBounds.Family (D : Type u_4) : Type u_4

Family: an abbreviation for ℕ → D → ComplexVector.

Equations

• NavierStokes.WaveInteractionBounds.Family D = (ℕ → D → NavierStokes.HarmonicCalculus.ComplexVector)

def NavierStokes.WaveInteractionBounds.WaveVector {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (P : ℕ → D → ℝ) (α : ℝ) (a : Family D) : Prop

Wave vector, given by ∀ i, WaveClass s P α (fun n x => a n x i).

Equations

• NavierStokes.WaveInteractionBounds.WaveVector s P α a = ∀ (i : Fin 3), NavierStokes.WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => a n x i

def NavierStokes.WaveInteractionBounds.MeanVector {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (μ : ℝ) (a : Family D) : Prop

Mean vector, given by MeanClass s (μ + 1) (fun n x => a n x 0) ∧ MeanClass s μ (fun n x => a n x 1) ∧ MeanClass s μ (fun n x => a n x 2).

Equations

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

theorem NavierStokes.WaveInteractionBounds.meanVector_component {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {μ : ℝ} {a : Family D} (ha : MeanVector s μ a) (i : Fin 3) : WeightedClasses.MeanClass s μ fun (n : ℕ) (x : D) => a n x i

def NavierStokes.WaveInteractionBounds.AngularIndependent {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (G : Geometry s κ) (a : Family D) : Prop

Angular independent, given by ∀ n i x, x ∈ s.domain → along (G.angular n) (fun y => a n y i) x = 0.

Equations

• NavierStokes.WaveInteractionBounds.AngularIndependent G a = ∀ (n : ℕ) (i : Fin 3), ∀ x ∈ s.domain, NavierStokes.HarmonicCalculus.along (G.angular n) (fun (y : D) => a n y i) x = 0

noncomputable def NavierStokes.WaveInteractionBounds.strippedTransport {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (G : Geometry s κ) (a b : Family D) : Family D

Stripped transport as an element of Family D.

Equations

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

theorem NavierStokes.WaveInteractionBounds.transport_eq_stripped {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (G : Geometry s κ) (a b : Family D) (hb : AngularIndependent G b) (n : ℕ) {x : D} (hx : x ∈ s.domain) : LinearWaveResidual.transport (G.radius n) (G.radial n) (G.angular n) (G.axial n) (a n) (b n) x = strippedTransport G a b n x

theorem NavierStokes.WaveInteractionBounds.generator_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {a : Family D} (ha : ∀ (i : Fin 3), WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => a n x i) (i : Fin 3) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => HarmonicCalculus.angularGenerator (a n x) i

theorem NavierStokes.WaveInteractionBounds.inverse_radius_complex {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (G : Geometry s κ) : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (↑(G.radius n x))⁻¹

theorem NavierStokes.WaveInteractionBounds.class_div_radius {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} (G : Geometry s κ) {f : ℕ → D → ℂ} (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => f n x / ↑(G.radius n x)

theorem NavierStokes.WaveInteractionBounds.strippedTransport_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w v : ℕ → D → ℝ} {α β κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {a b : Family D} (ha : ∀ (i : Fin 3), WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => a n x i) (hb : ∀ (i : Fin 3), WeightedClasses.MemClass s v β fun (n : ℕ) (x : D) => b n x i) (i : Fin 3) : WeightedClasses.MemClass s (fun (n : ℕ) (x : D) => w n x * v n x) (α + β - κ) fun (n : ℕ) (x : D) => strippedTransport G a b n x i

theorem NavierStokes.WaveInteractionBounds.strippedDivergence_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {a : Family D} (ha : ∀ (i : Fin 3), WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => a n x i) : WeightedClasses.MemClass s w (α - κ) fun (n : ℕ) => HarmonicCalculus.strippedDivergence (G.radius n) (G.radial n) (G.axial n) (a n)

theorem NavierStokes.WaveInteractionBounds.mean_wave_weight {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MemClass s (fun (n : ℕ) (x : D) => s.zeta x * (√(s.zeta x) * P n x)) α f) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) : WeightedClasses.WaveClass s P α f

theorem NavierStokes.WaveInteractionBounds.wave_mean_weight {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MemClass s (fun (n : ℕ) (x : D) => √(s.zeta x) * P n x * s.zeta x) α f) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) : WeightedClasses.WaveClass s P α f

theorem NavierStokes.WaveInteractionBounds.wave_square_weight_mean {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MemClass s (fun (n : ℕ) (x : D) => √(s.zeta x) * P n x * (√(s.zeta x) * P n x)) α f) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : WeightedClasses.MeanClass s α f

theorem NavierStokes.WaveInteractionBounds.wave_square_weight_wave {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MemClass s (fun (n : ℕ) (x : D) => √(s.zeta x) * P n x * (√(s.zeta x) * P n x)) α f) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : WeightedClasses.WaveClass s P α f

theorem NavierStokes.WaveInteractionBounds.mean_advects_stripped_wave {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α μ κ : ℝ} (G : Geometry s κ) (hκ : κ ≤ 1) {m a : Family D} (hm : MeanVector s μ m) (ha : WaveVector s P α a) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (i : Fin 3) : WeightedClasses.WaveClass s P (α + μ) fun (n : ℕ) (x : D) => strippedTransport G m a n x i

theorem NavierStokes.WaveInteractionBounds.wave_advects_stripped_mean {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α μ κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {m a : Family D} (hm : MeanVector s μ m) (ha : WaveVector s P α a) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (i : Fin 3) : WeightedClasses.WaveClass s P (α + μ - κ) fun (n : ℕ) (x : D) => strippedTransport G a m n x i

theorem NavierStokes.WaveInteractionBounds.carrier_add {D : Type u_1} (κ κ' : ℝ) (Φ : D → ℝ) (x : D) : HarmonicCalculus.carrier κ Φ x * HarmonicCalculus.carrier κ' Φ x = HarmonicCalculus.carrier (κ + κ') Φ x

theorem NavierStokes.WaveInteractionBounds.carrier_zero {D : Type u_1} (Φ : D → ℝ) (x : D) : HarmonicCalculus.carrier 0 Φ x = 1

theorem NavierStokes.WaveInteractionBounds.transport_mode_left {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (κ : ℝ) (Φ : D → ℝ) (a b : D → HarmonicCalculus.ComplexVector) (x : D) (i : Fin 3) : LinearWaveResidual.transport R Vr Vθ Vz (HarmonicCalculus.vectorMode κ Φ a) b x i = LinearWaveResidual.transport R Vr Vθ Vz a b x i * HarmonicCalculus.carrier κ Φ x

theorem NavierStokes.WaveInteractionBounds.transport_mode_right {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (κ : ℝ) {Φ : D → ℝ} (a : D → HarmonicCalculus.ComplexVector) {b : D → HarmonicCalculus.ComplexVector} {x : D} (hΦ : DifferentiableAt ℝ Φ x) (hb : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => b y i) x) (i : Fin 3) : LinearWaveResidual.transport R Vr Vθ Vz a (HarmonicCalculus.vectorMode κ Φ b) x i = (LinearWaveResidual.transport R Vr Vθ Vz a b x i + HarmonicCalculus.phaseFactor κ * HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (a x) * b x i) * HarmonicCalculus.carrier κ Φ x

theorem NavierStokes.WaveInteractionBounds.transport_modes {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (κ κ' : ℝ) {Φ : D → ℝ} (a : D → HarmonicCalculus.ComplexVector) {b : D → HarmonicCalculus.ComplexVector} {x : D} (hΦ : DifferentiableAt ℝ Φ x) (hb : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => b y i) x) (i : Fin 3) : LinearWaveResidual.transport R Vr Vθ Vz (HarmonicCalculus.vectorMode κ Φ a) (HarmonicCalculus.vectorMode κ' Φ b) x i = (LinearWaveResidual.transport R Vr Vθ Vz a b x i + HarmonicCalculus.phaseFactor κ' * HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (a x) * b x i) * HarmonicCalculus.carrier (κ + κ') Φ x

The exact phase-sum coefficient of the actual bilinear differential operator.

theorem NavierStokes.WaveInteractionBounds.normalDot_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {N : ℕ → D → EuclideanSpace ℝ (Fin 3)} {a : Family D} (hN : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (N n x).ofLp i) (ha : ∀ (i : Fin 3), WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => a n x i) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => HarmonicCalculus.normalDot (N n x) (a n x)

theorem NavierStokes.WaveInteractionBounds.phaseFactor_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {ν : ℕ → ℝ} {f : ℕ → D → ℂ} (hf : WeightedClasses.MemClass s w α f) (hν : WeightedClasses.BandBound s β ν) : WeightedClasses.MemClass s w (α + β) fun (n : ℕ) (x : D) => HarmonicCalculus.phaseFactor (ν n) * f n x

noncomputable def NavierStokes.WaveInteractionBounds.waveMeanCoefficient {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (G : Geometry s κ) (Φ : ℕ → D → ℝ) (ν : ℕ → ℝ) (m a : Family D) : Family D

Wave mean coefficient as an element of Family D.

Equations

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

theorem NavierStokes.WaveInteractionBounds.wave_mean_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α μ κ : ℝ} (G : Geometry s κ) (hκ0 : 0 ≤ κ) (hκ1 : κ ≤ 1 / 2) {Φ : ℕ → D → ℝ} {ν : ℕ → ℝ} {m a : Family D} (hm : MeanVector s μ m) (ha : WaveVector s P α a) (hN : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (HarmonicCalculus.phaseNormal (G.radius n) (G.radial n) (G.angular n) (G.axial n) (Φ n) x).ofLp i) (hν : WeightedClasses.BandBound s (-(1 / 2)) ν) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) : WaveVector s P (α + μ - 1 / 2) (waveMeanCoefficient G Φ ν m a)

Both cross-advections, with the radial mean improvement explicitly used.

theorem NavierStokes.WaveInteractionBounds.wave_mean_identity {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (G : Geometry s κ) (Φ : ℕ → D → ℝ) (ν : ℕ → ℝ) (m a : Family D) (hmθ : AngularIndependent G m) (haθ : AngularIndependent G a) (n : ℕ) {x : D} (hx : x ∈ s.domain) (hΦ : DifferentiableAt ℝ (Φ n) x) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => a n y i) x) (i : Fin 3) : LinearWaveResidual.transport (G.radius n) (G.radial n) (G.angular n) (G.axial n) (m n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) x i + LinearWaveResidual.transport (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) (m n) x i = waveMeanCoefficient G Φ ν m a n x i * HarmonicCalculus.carrier (ν n) (Φ n) x

theorem NavierStokes.WaveInteractionBounds.phaseFactor_ratio (ν ξ : ℝ) (hν : ν ≠ 0) : ↑(ξ / ν) * HarmonicCalculus.phaseFactor ν = HarmonicCalculus.phaseFactor ξ

theorem NavierStokes.WaveInteractionBounds.switched_longitudinal {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (ν ξ : ℝ) (hν : ν ≠ 0) {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {x : D} (hΦ : DifferentiableAt ℝ Φ x) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => a y i) x) (haθ : HarmonicCalculus.along Vθ (fun (y : D) => a y 1) x = 0) (hdiv : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (HarmonicCalculus.vectorMode ν Φ a) x = 0) : HarmonicCalculus.phaseFactor ξ * HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (a x) = (ξ / ν) • -HarmonicCalculus.strippedDivergence R Vr Vz a x

The exact divergence cancellation, before taking any norm or any jet.

noncomputable def NavierStokes.WaveInteractionBounds.sameCoefficient {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (G : Geometry s κ) (Φ : ℕ → D → ℝ) (ξ : ℕ → ℝ) (a b : Family D) : Family D

Same coefficient as an element of Family D.

Equations

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

theorem NavierStokes.WaveInteractionBounds.same_label_identity {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (G : Geometry s κ) (Φ : ℕ → D → ℝ) (ν ξ : ℕ → ℝ) (a b : Family D) (hbθ : AngularIndependent G b) (n : ℕ) {x : D} (hx : x ∈ s.domain) (hΦ : DifferentiableAt ℝ (Φ n) x) (hb : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => b n y i) x) (i : Fin 3) : LinearWaveResidual.transport (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) (HarmonicCalculus.vectorMode (ξ n) (Φ n) (b n)) x i = sameCoefficient G Φ ξ a b n x i * HarmonicCalculus.carrier (ν n + ξ n) (Φ n) x

theorem NavierStokes.WaveInteractionBounds.same_label_raw_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {Φ : ℕ → D → ℝ} {ν ξ : ℕ → ℝ} {a b : Family D} (ha : WaveVector s P α a) (hb : WaveVector s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hν : ∀ (n : ℕ), ν n ≠ 0) (hratio : WeightedClasses.BandBound s 0 fun (n : ℕ) => ξ n / ν n) (haθ : AngularIndependent G a) (hdiv : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.cylindricalDivergence (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) x = 0) (i : Fin 3) : WeightedClasses.MemClass s (fun (n : ℕ) (x : D) => √(s.zeta x) * P n x * (√(s.zeta x) * P n x)) (α + β - κ) fun (n : ℕ) (x : D) => sameCoefficient G Φ ξ a b n x i

All derivatives of the longitudinal contraction are estimated through the actual divergence identity, including derivatives of the phase normal.

theorem NavierStokes.WaveInteractionBounds.same_label_wave_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {Φ : ℕ → D → ℝ} {ν ξ : ℕ → ℝ} {a b : Family D} (ha : WaveVector s P α a) (hb : WaveVector s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hν : ∀ (n : ℕ), ν n ≠ 0) (hratio : WeightedClasses.BandBound s 0 fun (n : ℕ) => ξ n / ν n) (haθ : AngularIndependent G a) (hdiv : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.cylindricalDivergence (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) x = 0) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : WaveVector s P (α + β - κ) (sameCoefficient G Φ ξ a b)

theorem NavierStokes.WaveInteractionBounds.same_label_mean_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {Φ : ℕ → D → ℝ} {ν ξ : ℕ → ℝ} {a b : Family D} (ha : WaveVector s P α a) (hb : WaveVector s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hν : ∀ (n : ℕ), ν n ≠ 0) (hratio : WeightedClasses.BandBound s 0 fun (n : ℕ) => ξ n / ν n) (haθ : AngularIndependent G a) (hdiv : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.cylindricalDivergence (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) x = 0) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (i : Fin 3) : WeightedClasses.MeanClass s (α + β - κ) fun (n : ℕ) (x : D) => sameCoefficient G Φ ξ a b n x i

theorem NavierStokes.WaveInteractionBounds.int_abs_cast_one_le {j : ℤ} (hj : j ≠ 0) : 1 ≤ |↑j|

theorem NavierStokes.WaveInteractionBounds.harmonic_ratio_bound {j l : ℤ} {M : ℝ} (hj : j ≠ 0) (hM : 0 ≤ M) (hl : |↑l| ≤ M) : |↑l / ↑j| ≤ M

theorem NavierStokes.WaveInteractionBounds.bandBound_harmonic_ratio {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) {j l : ℕ → ℤ} {M : ℝ} (hj : ∀ (n : ℕ), j n ≠ 0) (hM : 0 ≤ M) (hl : ∀ (n : ℕ), |↑(l n)| ≤ M) : WeightedClasses.BandBound s 0 fun (n : ℕ) => ↑(l n) / ↑(j n)

theorem NavierStokes.WaveInteractionBounds.frequency_ratio {k : ℝ} (hk : k ≠ 0) {j : ℤ} (hj : j ≠ 0) (l : ℤ) : k * ↑l / (k * ↑j) = ↑l / ↑j

theorem NavierStokes.WaveInteractionBounds.bandBound_frequency_ratio {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) {k : ℕ → ℝ} {j l : ℕ → ℤ} {M : ℝ} (hk : ∀ (n : ℕ), k n ≠ 0) (hj : ∀ (n : ℕ), j n ≠ 0) (hM : 0 ≤ M) (hl : ∀ (n : ℕ), |↑(l n)| ≤ M) : WeightedClasses.BandBound s 0 fun (n : ℕ) => k n * ↑(l n) / (k n * ↑(j n))

theorem NavierStokes.WaveInteractionBounds.bandBound_frequency {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {β : ℝ} {k : ℕ → ℝ} {j : ℕ → ℤ} {M : ℝ} (hk : WeightedClasses.BandBound s β k) (hM : 0 ≤ M) (hj : ∀ (n : ℕ), |↑(j n)| ≤ M) : WeightedClasses.BandBound s β fun (n : ℕ) => k n * ↑(j n)

theorem NavierStokes.WaveInteractionBounds.harmonic_stage_add {j l : ℤ} {M : ℝ} (stage : ℕ) (hj : |↑j| ≤ 2 ^ stage * M) (hl : |↑l| ≤ 2 ^ stage * M) : |↑(j + l)| ≤ 2 ^ (stage + 1) * M

Fixed-stage frequency growth is finite and independent of the band.

theorem NavierStokes.WaveInteractionBounds.harmonic_stage_neg {j : ℤ} {M : ℝ} (stage : ℕ) (hj : |↑j| ≤ 2 ^ stage * M) : |↑(-j)| ≤ 2 ^ stage * M

noncomputable def NavierStokes.WaveInteractionBounds.conjugateFamily {D : Type u_1} (a : Family D) : Family D

Conjugate family, defined pointwise by star (a n x i).

Equations

• NavierStokes.WaveInteractionBounds.conjugateFamily a n x i = star (a n x i)

theorem NavierStokes.WaveInteractionBounds.conjugate_wave {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} {a : Family D} (ha : WaveVector s P α a) : WaveVector s P α (conjugateFamily a)

theorem NavierStokes.WaveInteractionBounds.carrier_neg {D : Type u_1} (ν : ℝ) (Φ : D → ℝ) (x : D) : HarmonicCalculus.carrier (-ν) Φ x = star (HarmonicCalculus.carrier ν Φ x)

theorem NavierStokes.WaveInteractionBounds.vectorMode_conjugate {D : Type u_1} (ν : ℝ) (Φ : D → ℝ) (a : D → HarmonicCalculus.ComplexVector) (x : D) (i : Fin 3) : HarmonicCalculus.vectorMode (-ν) Φ (fun (y : D) (j : Fin 3) => star (a y j)) x i = star (HarmonicCalculus.vectorMode ν Φ a x i)

theorem NavierStokes.WaveInteractionBounds.opposite_identity {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (G : Geometry s κ) (Φ : ℕ → D → ℝ) (ν : ℕ → ℝ) (a b : Family D) (hbθ : AngularIndependent G b) (n : ℕ) {x : D} (hx : x ∈ s.domain) (hΦ : DifferentiableAt ℝ (Φ n) x) (hb : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => b n y i) x) (i : Fin 3) : LinearWaveResidual.transport (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) (HarmonicCalculus.vectorMode (-ν n) (Φ n) (b n)) x i = sameCoefficient G Φ (fun (n : ℕ) => -ν n) a b n x i

theorem NavierStokes.WaveInteractionBounds.opposite_mean_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {Φ : ℕ → D → ℝ} {ν : ℕ → ℝ} {a b : Family D} (ha : WaveVector s P α a) (hb : WaveVector s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hν : ∀ (n : ℕ), ν n ≠ 0) (haθ : AngularIndependent G a) (hdiv : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.cylindricalDivergence (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) x = 0) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (i : Fin 3) : WeightedClasses.MeanClass s (α + β - κ) fun (n : ℕ) (x : D) => sameCoefficient G Φ (fun (n : ℕ) => -ν n) a b n x i

theorem NavierStokes.WaveInteractionBounds.conjugate_opposite_mean_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {Φ : ℕ → D → ℝ} {ν : ℕ → ℝ} {a b : Family D} (ha : WaveVector s P α a) (hb : WaveVector s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hν : ∀ (n : ℕ), ν n ≠ 0) (haθ : AngularIndependent G a) (hdiv : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.cylindricalDivergence (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) x = 0) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (i : Fin 3) : WeightedClasses.MeanClass s (α + β - κ) fun (n : ℕ) (x : D) => (sameCoefficient G Φ (fun (n : ℕ) => -ν n) a (conjugateFamily b) n x i).re

theorem NavierStokes.WaveInteractionBounds.finite_wave_sum {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} {ι : Type u_4} (t : Finset ι) (a : ι → Family D) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (ha : ∀ j ∈ t, WaveVector s P α (a j)) : WaveVector s P α fun (n : ℕ) (x : D) (i : Fin 3) => ∑ j ∈ t, a j n x i

theorem NavierStokes.WaveInteractionBounds.same_label_harmonic_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ M : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {Φ : ℕ → D → ℝ} {k : ℕ → ℝ} {j l : ℕ → ℤ} {a b : Family D} (ha : WaveVector s P α a) (hb : WaveVector s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hk : ∀ (n : ℕ), k n ≠ 0) (hj : ∀ (n : ℕ), j n ≠ 0) (hM : 0 ≤ M) (hl : ∀ (n : ℕ), |↑(l n)| ≤ M) (haθ : AngularIndependent G a) (hdiv : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.cylindricalDivergence (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (k n * ↑(j n)) (Φ n) (a n)) x = 0) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : WaveVector s P (α + β - κ) (sameCoefficient G Φ (fun (n : ℕ) => k n * ↑(l n)) a b)

A nonzero integer first harmonic and a bounded second harmonic give the precise uniform ratio needed by the divergence cancellation.

theorem NavierStokes.WaveInteractionBounds.mul_along_zero {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {f g : D → ℂ} {x : D} (hx : x ∈ U) (hf : ContinuousAt f x) (hfg : ∀ y ∈ U, f y * g y = 0) (V : D → D) : f x * HarmonicCalculus.along V g x = 0

Vanishing of a product on an open set forces the differentiated second factor to vanish wherever the first factor is nonzero.

theorem NavierStokes.WaveInteractionBounds.transport_zero_of_products {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (R : D → ℝ) (Vr Vθ Vz : D → D) {a b : D → HarmonicCalculus.ComplexVector} (ha : ∀ (i : Fin 3), ContinuousOn (fun (y : D) => a y i) U) (hab : ∀ (i j : Fin 3), ∀ y ∈ U, a y i * b y j = 0) {x : D} (hx : x ∈ U) : LinearWaveResidual.transport R Vr Vθ Vz a b x = 0

theorem NavierStokes.WaveInteractionBounds.cross_transport_every_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {γ κ : ℝ} (G : Geometry s κ) {a b : Family D} (ha : ∀ (n : ℕ) (i : Fin 3), ContinuousOn (fun (y : D) => a n y i) s.domain) (hab : ∀ (n : ℕ) (i j : Fin 3), ∀ x ∈ s.domain, a n x i * b n x j = 0) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) : WaveVector s P γ fun (n : ℕ) => LinearWaveResidual.transport (G.radius n) (G.radial n) (G.angular n) (G.axial n) (a n) (b n)

theorem NavierStokes.WaveInteractionBounds.slot_complex_product_zero {d h : ℝ} {vr vt : PartitionedCovariance.Plane} (sys : PartitionedCovariance.SlotSystem d h vr vt) {L M : SlotColoring.Label} (hL : 1 ≤ L.1) (hM : 1 ≤ M.1) (hne : L ≠ M) {f g : PartitionedCovariance.Plane → ℝ} (hf : Function.support f ⊆ PartitionedCovariance.slotSet h sys.radius vr vt L) (hg : Function.support g ⊆ PartitionedCovariance.slotSet h sys.radius vr vt M) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (Y : PartitionedCovariance.Plane) (a b : ℂ) : ↑(PartitionedCovariance.physicalMask d L q x * PartitionedCovariance.covered (SlotColoring.nativeIndex h L.1) f Y) * a * (↑(PartitionedCovariance.physicalMask d M q x * PartitionedCovariance.covered (SlotColoring.nativeIndex h M.1) g Y) * b) = 0

noncomputable def NavierStokes.WaveInteractionBounds.slotField {D : Type u_1} (d h : ℝ) (L : SlotColoring.Label) (q : D → ℝ) (X : D → SlotColoring.Position) (Y : D → PartitionedCovariance.Plane) (f : Fin 3 → PartitionedCovariance.Plane → ℝ) (a : D → HarmonicCalculus.ComplexVector) : D → HarmonicCalculus.ComplexVector

The actual physical partition masks and covered native slot profiles, with arbitrary complex component multipliers (including harmonic carriers).

Equations

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

theorem NavierStokes.WaveInteractionBounds.slot_transport_zero {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {d h : ℝ} {vr vt : PartitionedCovariance.Plane} (sys : PartitionedCovariance.SlotSystem d h vr vt) {L M : SlotColoring.Label} (hL : 1 ≤ L.1) (hM : 1 ≤ M.1) (hne : L ≠ M) (q : D → ℝ) (X : D → SlotColoring.Position) (Y : D → PartitionedCovariance.Plane) (hq : ∀ y ∈ U, 0 < q y) (f g : Fin 3 → PartitionedCovariance.Plane → ℝ) (a b : D → HarmonicCalculus.ComplexVector) (hf : ∀ (i : Fin 3), Function.support (f i) ⊆ PartitionedCovariance.slotSet h sys.radius vr vt L) (hg : ∀ (i : Fin 3), Function.support (g i) ⊆ PartitionedCovariance.slotSet h sys.radius vr vt M) (ha : ∀ (i : Fin 3), ContinuousOn (fun (y : D) => slotField d h L q X Y f a y i) U) (R : D → ℝ) (Vr Vθ Vz : D → D) {x : D} (hx : x ∈ U) : LinearWaveResidual.transport R Vr Vθ Vz (slotField d h L q X Y f a) (slotField d h M q X Y g b) x = 0

theorem NavierStokes.WaveInteractionBounds.transport_realLift {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (u : D → Fin 3 → ℝ) {v : D → Fin 3 → ℝ} {x : D} (hv : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => v y i) x) (i : Fin 3) : LinearWaveResidual.transport R Vr Vθ Vz (LinearWaveResidual.realLift u) (LinearWaveResidual.realLift v) x i = ↑(LinearWaveResidual.realTransport R Vr Vθ Vz u v x i)

The complex operator restricts to the real cylindrical bilinear operator.

theorem NavierStokes.WaveInteractionBounds.transport_real_parts {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (u : D → HarmonicCalculus.ComplexVector) {v : D → HarmonicCalculus.ComplexVector} {x : D} (hv : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => v y i) x) (i : Fin 3) : LinearWaveResidual.realTransport R Vr Vθ Vz (fun (y : D) (j : Fin 3) => (u y j).re) (fun (y : D) (j : Fin 3) => (v y j).re) x i = ((LinearWaveResidual.transport R Vr Vθ Vz u v x i).re + (LinearWaveResidual.transport R Vr Vθ Vz u (fun (y : D) (j : Fin 3) => star (v y j)) x i).re) / 2

Real bilinear products require both ordinary and conjugate harmonic pairs.

theorem NavierStokes.WaveInteractionBounds.conjugate_angularIndependent {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} (G : Geometry s κ) {a : Family D} (ha : WaveVector s P α a) (haθ : AngularIndependent G a) : AngularIndependent G (conjugateFamily a)

theorem NavierStokes.WaveInteractionBounds.real_modes_identity {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {β κ : ℝ} (G : Geometry s κ) (Φ : ℕ → D → ℝ) (ν ξ : ℕ → ℝ) (a b : Family D) (hb : WaveVector s P β b) (hbθ : AngularIndependent G b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (n : ℕ) {x : D} (hx : x ∈ s.domain) (i : Fin 3) : LinearWaveResidual.realTransport (G.radius n) (G.radial n) (G.angular n) (G.axial n) (fun (y : D) (j : Fin 3) => (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n) y j).re) (fun (y : D) (j : Fin 3) => (HarmonicCalculus.vectorMode (ξ n) (Φ n) (b n) y j).re) x i = ((sameCoefficient G Φ ξ a b n x i * HarmonicCalculus.carrier (ν n + ξ n) (Φ n) x).re + (sameCoefficient G Φ (fun (n : ℕ) => -ξ n) a (conjugateFamily b) n x i * HarmonicCalculus.carrier (ν n - ξ n) (Φ n) x).re) / 2

Exact real reconstruction: the two output harmonics are the sum and difference of the two input harmonics. No angular averaging is assumed.

theorem NavierStokes.WaveInteractionBounds.real_equal_modes_identity {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {β κ : ℝ} (G : Geometry s κ) (Φ : ℕ → D → ℝ) (ν : ℕ → ℝ) (a b : Family D) (hb : WaveVector s P β b) (hbθ : AngularIndependent G b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (n : ℕ) {x : D} (hx : x ∈ s.domain) (i : Fin 3) : LinearWaveResidual.realTransport (G.radius n) (G.radial n) (G.angular n) (G.axial n) (fun (y : D) (j : Fin 3) => (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n) y j).re) (fun (y : D) (j : Fin 3) => (HarmonicCalculus.vectorMode (ν n) (Φ n) (b n) y j).re) x i = (sameCoefficient G Φ ν a b n x i * HarmonicCalculus.carrier (2 * ν n) (Φ n) x).re / 2 + (sameCoefficient G Φ (fun (n : ℕ) => -ν n) a (conjugateFamily b) n x i).re / 2

Equal input frequencies have an exact doubled-frequency term and an opposite-frequency mean term, each with its real reconstruction factor.

theorem NavierStokes.WaveInteractionBounds.real_mean_coefficient_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {Φ : ℕ → D → ℝ} {ν : ℕ → ℝ} {a b : Family D} (ha : WaveVector s P α a) (hb : WaveVector s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hν : ∀ (n : ℕ), ν n ≠ 0) (haθ : AngularIndependent G a) (hdiv : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.cylindricalDivergence (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) x = 0) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (i : Fin 3) : WeightedClasses.MeanClass s (α + β - κ) fun (n : ℕ) (x : D) => (sameCoefficient G Φ (fun (n : ℕ) => -ν n) a (conjugateFamily b) n x i).re / 2

theorem NavierStokes.WaveInteractionBounds.divergence_congr {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (R : D → ℝ) (Vr Vθ Vz : D → D) {a b : D → HarmonicCalculus.ComplexVector} (hab : Set.EqOn a b U) {x : D} (hx : x ∈ U) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz a x = HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz b x

theorem NavierStokes.WaveInteractionBounds.same_label_from_curl {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {Φ : ℕ → D → ℝ} {ν ξ : ℕ → ℝ} {a b B : Family D} (ha : WaveVector s P α a) (hb : WaveVector s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hν : ∀ (n : ℕ), ν n ≠ 0) (hratio : WeightedClasses.BandBound s 0 fun (n : ℕ) => ξ n / ν n) (haθ : AngularIndependent G a) (hG : ∀ (n : ℕ), CurlClassBounds.CylindricalGeometry s.domain (G.radius n) (G.radial n) (G.angular n) (G.axial n)) (hB : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (B n) s.domain) (hcurl : ∀ (n : ℕ), Set.EqOn (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) (CurlClassBounds.cylindricalCurl (G.radius n) (G.radial n) (G.angular n) (G.axial n) (B n)) s.domain) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : WaveVector s P (α + β - κ) (sameCoefficient G Φ ξ a b)

Exact curl realization supplies the solenoidality used in the saved half-power estimate. The equality is required on a neighborhood, so every derivative of the actual field participates in the identity.

theorem NavierStokes.WaveInteractionBounds.same_label_from_realized {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {Φ : ℕ → D → ℝ} {ν ξ : ℕ → ℝ} {a₀ b : Family D} (ha : WaveVector s P α fun (n : ℕ) => CurlClassBounds.realizedCoefficient (ν n) (G.radius n) (G.radial n) (G.angular n) (G.axial n) (Φ n) (a₀ n)) (hb : WaveVector s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hν : ∀ (n : ℕ), ν n ≠ 0) (hratio : WeightedClasses.BandBound s 0 fun (n : ℕ) => ξ n / ν n) (haθ : AngularIndependent G fun (n : ℕ) => CurlClassBounds.realizedCoefficient (ν n) (G.radius n) (G.radial n) (G.angular n) (G.axial n) (Φ n) (a₀ n)) (hG : ∀ (n : ℕ), CurlClassBounds.CylindricalGeometry s.domain (G.radius n) (G.radial n) (G.angular n) (G.axial n)) (ha₀ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a₀ n) s.domain) (hn : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.phaseNormal (G.radius n) (G.radial n) (G.angular n) (G.axial n) (Φ n) x ≠ 0) (ht : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal (G.radius n) (G.radial n) (G.angular n) (G.axial n) (Φ n) x) (a₀ n x) = 0) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : WaveVector s P (α + β - κ) (sameCoefficient G Φ ξ (fun (n : ℕ) => CurlClassBounds.realizedCoefficient (ν n) (G.radius n) (G.radial n) (G.angular n) (G.axial n) (Φ n) (a₀ n)) b)

A direct specialization to the manuscript's constructed vector potential. Its curl remainder is part of the realized coefficient on both sides.

theorem NavierStokes.WaveInteractionBounds.product_curl_zero {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (R : D → ℝ) (Vr Vθ Vz : D → D) {a b : D → HarmonicCalculus.ComplexVector} (ha : ∀ (i : Fin 3), ContinuousOn (fun (y : D) => a y i) U) (hab : ∀ (i j : Fin 3), ∀ y ∈ U, a y i * b y j = 0) {x : D} (hx : x ∈ U) (i j : Fin 3) : a x i * CurlClassBounds.cylindricalCurl R Vr Vθ Vz b x j = 0

Multiplying by the actual curl of the second field still vanishes on disjoint supports; this includes every coefficient derivative and frame term.

theorem NavierStokes.WaveInteractionBounds.curl_cross_products {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vθ Vz : D → D} (G : CurlClassBounds.CylindricalGeometry U R Vr Vθ Vz) {a b : D → HarmonicCalculus.ComplexVector} (ha : ContDiffOn ℝ (↑⊤) a U) (hb : ContDiffOn ℝ (↑⊤) b U) (hab : ∀ (i j : Fin 3), ∀ y ∈ U, a y i * b y j = 0) {x : D} (hx : x ∈ U) (i j : Fin 3) : CurlClassBounds.cylindricalCurl R Vr Vθ Vz a x i * CurlClassBounds.cylindricalCurl R Vr Vθ Vz b x j = 0

theorem NavierStokes.WaveInteractionBounds.curl_transport_zero {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vθ Vz : D → D} (G : CurlClassBounds.CylindricalGeometry U R Vr Vθ Vz) {a b : D → HarmonicCalculus.ComplexVector} (ha : ContDiffOn ℝ (↑⊤) a U) (hb : ContDiffOn ℝ (↑⊤) b U) (hab : ∀ (i j : Fin 3), ∀ y ∈ U, a y i * b y j = 0) {x : D} (hx : x ∈ U) : LinearWaveResidual.transport R Vr Vθ Vz (CurlClassBounds.cylindricalCurl R Vr Vθ Vz a) (CurlClassBounds.cylindricalCurl R Vr Vθ Vz b) x = 0

theorem NavierStokes.WaveInteractionBounds.curl_transport_every_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {γ κ : ℝ} (G : Geometry s κ) {a b : Family D} (hG : ∀ (n : ℕ), CurlClassBounds.CylindricalGeometry s.domain (G.radius n) (G.radial n) (G.angular n) (G.axial n)) (ha : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a n) s.domain) (hb : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (b n) s.domain) (hab : ∀ (n : ℕ) (i j : Fin 3), ∀ x ∈ s.domain, a n x i * b n x j = 0) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) : WaveVector s P γ fun (n : ℕ) => LinearWaveResidual.transport (G.radius n) (G.radial n) (G.angular n) (G.axial n) (CurlClassBounds.cylindricalCurl (G.radius n) (G.radial n) (G.angular n) (G.axial n) (a n)) (CurlClassBounds.cylindricalCurl (G.radius n) (G.radial n) (G.angular n) (G.axial n) (b n))

theorem NavierStokes.WaveInteractionBounds.slot_curl_transport_zero {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vθ Vz : D → D} (G : CurlClassBounds.CylindricalGeometry U R Vr Vθ Vz) {d h : ℝ} {vr vt : PartitionedCovariance.Plane} (sys : PartitionedCovariance.SlotSystem d h vr vt) {L M : SlotColoring.Label} (hL : 1 ≤ L.1) (hM : 1 ≤ M.1) (hne : L ≠ M) (q : D → ℝ) (X : D → SlotColoring.Position) (Y : D → PartitionedCovariance.Plane) (hq : ∀ y ∈ U, 0 < q y) (f g : Fin 3 → PartitionedCovariance.Plane → ℝ) (a b : D → HarmonicCalculus.ComplexVector) (hf : ∀ (i : Fin 3), Function.support (f i) ⊆ PartitionedCovariance.slotSet h sys.radius vr vt L) (hg : ∀ (i : Fin 3), Function.support (g i) ⊆ PartitionedCovariance.slotSet h sys.radius vr vt M) (ha : ContDiffOn ℝ (↑⊤) (slotField d h L q X Y f a) U) (hb : ContDiffOn ℝ (↑⊤) (slotField d h M q X Y g b) U) {x : D} (hx : x ∈ U) : LinearWaveResidual.transport R Vr Vθ Vz (CurlClassBounds.cylindricalCurl R Vr Vθ Vz (slotField d h L q X Y f a)) (CurlClassBounds.cylindricalCurl R Vr Vθ Vz (slotField d h M q X Y g b)) x = 0

The separated, covered slots make the actual curl-wave interaction zero. This remains true at the boundaries of the supports.

theorem NavierStokes.WaveInteractionBounds.realTransport_coordinates (u : ProblemStatement.Space → ProblemStatement.Space) {v : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hv : DifferentiableAt ℝ v q) (i : Fin 3) : LinearWaveResidual.realTransport (fun (y : ProblemStatement.Space) => y.ofLp 0) (fun (x : ProblemStatement.Space) => ProblemStatement.coordinateVector 0) (fun (x : ProblemStatement.Space) => ProblemStatement.coordinateVector 1) (fun (x : ProblemStatement.Space) => ProblemStatement.coordinateVector 2) (fun (y : ProblemStatement.Space) (j : Fin 3) => (u y).ofLp j) (fun (y : ProblemStatement.Space) (j : Fin 3) => (v y).ofLp j) q i = (LinearWaveResidual.bilinearAdvection u v q).ofLp i

theorem NavierStokes.WaveInteractionBounds.cartesian_transport_components {u v : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hv : DifferentiableAt ℝ v (CylindricalResidual.chart q)) (hr : 0 < q.ofLp 0) (i : Fin 3) : ((CylindricalResidual.frame (-q.ofLp 1)) ((fderiv ℝ v (CylindricalResidual.chart q)) (u (CylindricalResidual.chart q)))).ofLp i = LinearWaveResidual.realTransport (fun (y : ProblemStatement.Space) => y.ofLp 0) (fun (x : ProblemStatement.Space) => ProblemStatement.coordinateVector 0) (fun (x : ProblemStatement.Space) => ProblemStatement.coordinateVector 1) (fun (x : ProblemStatement.Space) => ProblemStatement.coordinateVector 2) (fun (y : ProblemStatement.Space) (j : Fin 3) => (CylindricalResidual.components u y).ofLp j) (fun (y : ProblemStatement.Space) (j : Fin 3) => (CylindricalResidual.components v y).ofLp j) q i

The real bilinear operator estimated above is obtained from the actual Cartesian derivative by the cylindrical frame, on positive radius.

noncomputable def NavierStokes.WaveInteractionBounds.fixedGeometry {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (R : D → ℝ) (Vr Vθ Vz : ℕ → D → D) (hR : ∀ x ∈ s.domain, 0 < R x) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hinv : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => (R x_1)⁻¹) : Geometry s κ

Fixed geometry, bundling radius, radial, angular, axial and the required compatibility proofs.

Equations

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

theorem NavierStokes.WaveInteractionBounds.realized_seed_pair_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ δ M : ℝ} (R : D → ℝ) (Vr Vθ Vz : ℕ → D → D) (hR : ∀ x ∈ s.domain, 0 < R x) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hθ : WeightedClasses.UnweightedClass s 0 Vθ) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hinv : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => (R x_1)⁻¹) {Φ : ℕ → D → ℝ} {ν ξ : ℕ → ℝ} {a₀ b₀ : Family D} (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) fun (n : ℕ) => HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n)) (ha₀ : WeightedClasses.WaveClass s P α a₀) (hb₀ : WeightedClasses.WaveClass s P β b₀) (hδ : 0 < δ) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, δ ≤ ‖HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n) x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n) x‖ ≤ M) (hκ : 0 ≤ κ) (hκhalf : κ ≤ 1 / 2) (hνinv : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / ν n) (hξinv : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / ξ n) (hν : ∀ (n : ℕ), ν n ≠ 0) (hratio : WeightedClasses.BandBound s 0 fun (n : ℕ) => ξ n / ν n) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hG : ∀ (n : ℕ), CurlClassBounds.CylindricalGeometry s.domain R (Vr n) (Vθ n) (Vz n)) (ht : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n) x) (a₀ n x) = 0) (haθ : ∀ (n : ℕ) (i : Fin 3), ∀ x ∈ s.domain, HarmonicCalculus.along (Vθ n) (fun (y : D) => CurlClassBounds.realizedCoefficient (ν n) R (Vr n) (Vθ n) (Vz n) (Φ n) (a₀ n) y i) x = 0) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : WaveVector s P (α + β - κ) (sameCoefficient (fixedGeometry R Vr Vθ Vz hR hr hz hinv) Φ ξ (fun (n : ℕ) => CurlClassBounds.realizedCoefficient (ν n) R (Vr n) (Vθ n) (Vz n) (Φ n) (a₀ n)) fun (n : ℕ) => CurlClassBounds.realizedCoefficient (ξ n) R (Vr n) (Vθ n) (Vz n) (Φ n) (b₀ n))

The input wave classes in the interaction estimate can themselves be generated from seed amplitudes by the proved curl-remainder bounds.

noncomputable def NavierStokes.WaveInteractionBounds.stageHarmonics (initial : Finset ℤ) : ℕ → Finset ℤ

Finite harmonic sets generated by retention, conjugation and quadratic interaction. The recursive definition retains zero harmonics as well.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.WaveInteractionBounds.stageHarmonics initial 0 = initial

theorem NavierStokes.WaveInteractionBounds.stageHarmonics_bound {initial : Finset ℤ} {M : ℝ} (hM : 0 ≤ M) (hinitial : ∀ j ∈ initial, |↑j| ≤ M) (stage : ℕ) {j : ℤ} (hj : j ∈ stageHarmonics initial stage) : |↑j| ≤ 2 ^ stage * M

theorem NavierStokes.WaveInteractionBounds.stage_frequency_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {β M : ℝ} {k : ℕ → ℝ} {initial : ℕ → Finset ℤ} {j : ℕ → ℤ} (hk : WeightedClasses.BandBound s β k) (hM : 0 ≤ M) (hinitial : ∀ (n : ℕ), ∀ l ∈ initial n, |↑l| ≤ M) (stage : ℕ) (hj : ∀ (n : ℕ), j n ∈ stageHarmonics (initial n) stage) : WeightedClasses.BandBound s β fun (n : ℕ) => k n * ↑(j n)

theorem NavierStokes.WaveInteractionBounds.same_label_curl_interaction {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α β κ : ℝ} (G : Geometry s κ) (hκ : 0 ≤ κ) {Φ : ℕ → D → ℝ} {ν ξ : ℕ → ℝ} {a b B : Family D} (ha : WaveVector s P α a) (hb : WaveVector s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (Φ n) s.domain) (hν : ∀ (n : ℕ), ν n ≠ 0) (hratio : WeightedClasses.BandBound s 0 fun (n : ℕ) => ξ n / ν n) (haθ : AngularIndependent G a) (hbθ : AngularIndependent G b) (hG : ∀ (n : ℕ), CurlClassBounds.CylindricalGeometry s.domain (G.radius n) (G.radial n) (G.angular n) (G.axial n)) (hB : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (B n) s.domain) (hcurl : ∀ (n : ℕ), Set.EqOn (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) (CurlClassBounds.cylindricalCurl (G.radius n) (G.radial n) (G.angular n) (G.axial n) (B n)) s.domain) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : ∃ (c : Family D), WaveVector s P (α + β - κ) c ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, LinearWaveResidual.transport (G.radius n) (G.radial n) (G.angular n) (G.axial n) (HarmonicCalculus.vectorMode (ν n) (Φ n) (a n)) (HarmonicCalculus.vectorMode (ξ n) (Φ n) (b n)) x = fun (i : Fin 3) => c n x i * HarmonicCalculus.carrier (ν n + ξ n) (Φ n) x

A complete ordered interaction endpoint: the coefficient is in the claimed all-jet class and reconstructs the actual differential product.