Actual harmonic wave-update interactions

The nonlinear terms are finite convolutions of actual differentiated fields. All-jet classes are lifted and restricted by proved norm-one linear pullbacks before applying the full cylindrical divergence cancellation.

Actual harmonic residual changes under a mean increment

The wave and its pressure are held fixed. Every coefficient below belongs to the actual differential residual in HarmonicResidual; excluded errors are kept as separate additive differences.

@[simp]

theorem NavierStokes.HarmonicMeanInteraction.coeff_add {D : Type} (a b : HarmonicFields.Coefficients D) (j : ℤ) (x : D) : (a + b).coeff j x = a.coeff j x + b.coeff j x

@[simp]

theorem NavierStokes.HarmonicMeanInteraction.coeff_sub {D : Type} (a b : HarmonicFields.Coefficients D) (j : ℤ) (x : D) : (a - b).coeff j x = a.coeff j x - b.coeff j x

@[simp]

theorem NavierStokes.HarmonicMeanInteraction.coeff_neg {D : Type} (a : HarmonicFields.Coefficients D) (j : ℤ) (x : D) : (-a).coeff j x = -a.coeff j x

@[simp]

theorem NavierStokes.HarmonicMeanInteraction.coeff_zero {D : Type} (j : ℤ) (x : D) : (AddMonoidAlgebra.coeff 0) j x = 0

@[simp]

theorem NavierStokes.HarmonicMeanInteraction.constant_mul {D : Type} (f : D → ℂ) (a : HarmonicFields.Coefficients D) (j : ℤ) (x : D) : (HarmonicFields.constantCoefficient f * a).coeff j x = f x * a.coeff j x

@[simp]

theorem NavierStokes.HarmonicMeanInteraction.mul_constant {D : Type} (a : HarmonicFields.Coefficients D) (f : D → ℂ) (j : ℤ) (x : D) : (a * HarmonicFields.constantCoefficient f).coeff j x = a.coeff j x * f x

theorem NavierStokes.HarmonicMeanInteraction.constant_mul_constant {D : Type} (f g : D → ℂ) : HarmonicFields.constantCoefficient f * HarmonicFields.constantCoefficient g = HarmonicFields.constantCoefficient fun (x : D) => f x * g x

theorem NavierStokes.HarmonicMeanInteraction.constant_add {D : Type} (f g : D → ℂ) : HarmonicFields.constantCoefficient f + HarmonicFields.constantCoefficient g = HarmonicFields.constantCoefficient fun (x : D) => f x + g x

theorem NavierStokes.HarmonicMeanInteraction.differentiate_constant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (V : D → D) (k : ℝ) (Φ : D → ℝ) (f : D → ℂ) : HarmonicFields.differentiate V k Φ (HarmonicFields.constantCoefficient f) = HarmonicFields.constantCoefficient (HarmonicCalculus.along V f)

theorem NavierStokes.HarmonicMeanInteraction.angularDifferentiate_constant {D : Type} (kp : ℤ) (f : D → ℂ) : HarmonicFields.angularDifferentiate kp (HarmonicFields.constantCoefficient f) = 0

theorem NavierStokes.HarmonicMeanInteraction.rotate_constant {D : Type} (m : D → HarmonicCalculus.ComplexVector) (i : Fin 3) : HarmonicResidual.rotate (HarmonicResidual.constantVector m) i = HarmonicFields.constantCoefficient fun (x : D) => HarmonicCalculus.angularGenerator (m x) i

theorem NavierStokes.HarmonicMeanInteraction.rotate_apply {D : Type} (a : HarmonicResidual.VectorCoefficients D) (j : ℤ) (x : D) (i : Fin 3) : (HarmonicResidual.rotate a i).coeff j x = HarmonicCalculus.angularGenerator (fun (l : Fin 3) => (a l).coeff j x) i

theorem NavierStokes.HarmonicMeanInteraction.transport_constant_left {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (m : D → HarmonicCalculus.ComplexVector) (a : HarmonicResidual.VectorCoefficients D) (j : ℤ) (x : D) (i : Fin 3) : (HarmonicResidual.transport g k Φ kp (HarmonicResidual.constantVector m) a i).coeff j x = m x 0 * HarmonicFields.derivativeCoefficient g.radial k Φ j ((a i).coeff j) x + m x 1 / ↑(g.radius x) * (↑(j * kp) * Complex.I * (a i).coeff j x + HarmonicCalculus.angularGenerator (fun (l : Fin 3) => (a l).coeff j x) i) + m x 2 * HarmonicFields.derivativeCoefficient g.axial k Φ j ((a i).coeff j) x

theorem NavierStokes.HarmonicMeanInteraction.transport_constant_right {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (a : HarmonicResidual.VectorCoefficients D) (m : D → HarmonicCalculus.ComplexVector) (j : ℤ) (x : D) (i : Fin 3) : (HarmonicResidual.transport g k Φ kp a (HarmonicResidual.constantVector m) i).coeff j x = (a 0).coeff j x * HarmonicCalculus.along g.radial (fun (y : D) => m y i) x + (a 1).coeff j x / ↑(g.radius x) * HarmonicCalculus.angularGenerator (m x) i + (a 2).coeff j x * HarmonicCalculus.along g.axial (fun (y : D) => m y i) x

noncomputable def NavierStokes.HarmonicMeanInteraction.crossCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (m : D → HarmonicCalculus.ComplexVector) (a : HarmonicResidual.VectorCoefficients D) : HarmonicResidual.VectorCoefficients D

The two actual cross-advections at coefficient level, before any zero-mode deletion.

Equations

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

theorem NavierStokes.HarmonicMeanInteraction.nonlinear_mean_difference {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (B m : D → HarmonicCalculus.ComplexVector) (a : HarmonicResidual.VectorCoefficients D) (p : HarmonicFields.Coefficients D) {x : D} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => B y i) x) (hm : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => m y i) x) (j : ℤ) (i : Fin 3) : (HarmonicResidual.nonlinearResidual g k Φ kp (HarmonicResidual.constantVector (B + m)) a p i).coeff j x - (HarmonicResidual.nonlinearResidual g k Φ kp (HarmonicResidual.constantVector B) a p i).coeff j x = (crossCoefficients g k Φ kp m a i).coeff j x

theorem NavierStokes.HarmonicMeanInteraction.realCoefficients_sub {D : Type} (a b : HarmonicFields.Coefficients D) : HarmonicResidual.realCoefficients (a - b) = HarmonicResidual.realCoefficients a - HarmonicResidual.realCoefficients b

theorem NavierStokes.HarmonicMeanInteraction.realCoefficients_add {D : Type} (a b : HarmonicFields.Coefficients D) : HarmonicResidual.realCoefficients (a + b) = HarmonicResidual.realCoefficients a + HarmonicResidual.realCoefficients b

theorem NavierStokes.HarmonicMeanInteraction.realCoefficients_local_congr {D : Type} {U : Set D} {a b : HarmonicFields.Coefficients D} (hab : ∀ (j : ℤ), ∀ x ∈ U, a.coeff j x = b.coeff j x) (j : ℤ) {x : D} (hx : x ∈ U) : (HarmonicResidual.realCoefficients a).coeff j x = (HarmonicResidual.realCoefficients b).coeff j x

noncomputable def NavierStokes.HarmonicMeanInteraction.tripleField {D : Type} (h : MeanIncrementBounds.Triple D) (n : ℕ) (x : D) : HarmonicCalculus.ComplexVector

Triple field, given by ![(h.radial n x : ℂ), (h.angular n x : ℂ), (h.axial n x : ℂ)].

Equations

• NavierStokes.HarmonicMeanInteraction.tripleField h n x = ![↑(h.radial n x), ↑(h.angular n x), ↑(h.axial n x)]

theorem NavierStokes.HarmonicMeanInteraction.stateMean_updated {D : Type} (s₀ s₁ : CorrectionState.State D) (h : MeanIncrementBounds.Triple D) (he : s₁.mean = MeanIncrementBounds.updated s₀.mean h) (n : ℕ) : HarmonicResidual.stateMean s₁ n = HarmonicResidual.stateMean s₀ n + tripleField h n

noncomputable def NavierStokes.HarmonicMeanInteraction.blockAmplitude {D : Type} (b : CorrectionState.HarmonicBlock D) (n : ℕ) : HarmonicResidual.VectorCoefficients D

Block amplitude, defined pointwise by HarmonicResidual.realCoefficients (b.velocity n i).

Equations

• NavierStokes.HarmonicMeanInteraction.blockAmplitude b n i = NavierStokes.HarmonicResidual.realCoefficients (b.velocity n i)

noncomputable def NavierStokes.HarmonicMeanInteraction.meanCross {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (h : MeanIncrementBounds.Triple D) (b : CorrectionState.HarmonicBlock D) (n : ℕ) : HarmonicResidual.VectorCoefficients D

Mean cross, constructed using crossCoefficients.

Equations

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

theorem NavierStokes.HarmonicMeanInteraction.residualCoefficients_mean_update {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s₀ s₁ : CorrectionState.State D) (h : MeanIncrementBounds.Triple D) (he : s₁.mean = MeanIncrementBounds.updated s₀.mean h) (b : CorrectionState.HarmonicBlock D) (G₀ G₁ A₀ A₁ : HarmonicResidual.BlockCoefficients D) (n : ℕ) {x : D} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => HarmonicResidual.contextBase c n y i) x) (hM : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => HarmonicResidual.stateMean s₀ n y i) x) (hh : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => tripleField h n y i) x) (j : ℤ) (i : Fin 3) : ((HarmonicResidual.ofBlock b G₁ A₁ n).residualCoefficients (HarmonicResidual.contextFrame c n) (HarmonicResidual.contextBase c n) (HarmonicResidual.stateMean s₁ n) i).coeff j x - ((HarmonicResidual.ofBlock b G₀ A₀ n).residualCoefficients (HarmonicResidual.contextFrame c n) (HarmonicResidual.contextBase c n) (HarmonicResidual.stateMean s₀ n) i).coeff j x = (HarmonicResidual.realCoefficients (meanCross c h b n i - (G₁ n i - G₀ n i) - (A₁ n i - A₀ n i))).coeff j x

General additive error differences are retained, including their zero modes.

Bounds on the original coefficient domain

noncomputable def NavierStokes.HarmonicMeanInteraction.slowGeometry {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) : WaveInteractionBounds.Geometry s κ

The slow coefficient geometry has no artificial angular coordinate. The actual separate angular carrier is accounted for explicitly below.

Equations

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

noncomputable def NavierStokes.HarmonicMeanInteraction.slowNormal {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) (Φ : ℕ → D → ℝ) (n : ℕ) (x : D) : EuclideanSpace ℝ (Fin 3)

Slow normal, constructed using phaseNormal.

Equations

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

theorem NavierStokes.HarmonicMeanInteraction.tripleField_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {H : ℝ} {h : MeanIncrementBounds.Triple D} (hh : MeanIncrementBounds.IncrementBounds s H h) : WaveInteractionBounds.MeanVector s H (tripleField h)

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

theorem NavierStokes.HarmonicMeanInteraction.blockAmplitude_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} {b : CorrectionState.HarmonicBlock D} (hb : CorrectionState.HarmonicBlock.WaveBounds s P α b) {j : ℤ} (hj : j ≠ 0) : WaveInteractionBounds.WaveVector s P α fun (n : ℕ) (x : D) (i : Fin 3) => (blockAmplitude b n i).coeff j x

noncomputable def NavierStokes.HarmonicMeanInteraction.angularCarrierTerm {D : Type} (c : CorrectionState.Context D) (b : CorrectionState.HarmonicBlock D) (h : MeanIncrementBounds.Triple D) (j : ℤ) (n : ℕ) (x : D) (i : Fin 3) : ℂ

The separate angular phase term has the same carrier loss as the slow phase term.

Equations

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

theorem NavierStokes.HarmonicMeanInteraction.meanCross_eq {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) (h : MeanIncrementBounds.Triple D) (b : CorrectionState.HarmonicBlock D) (j : ℤ) (n : ℕ) (x : D) (i : Fin 3) : (meanCross c h b n i).coeff j x = WaveInteractionBounds.waveMeanCoefficient (slowGeometry c ho hR) b.phase (fun (n : ℕ) => b.frequency n * ↑j) (tripleField h) (fun (n : ℕ) (x : D) (i : Fin 3) => (blockAmplitude b n i).coeff j x) n x i + angularCarrierTerm c b h j n x i

theorem NavierStokes.HarmonicMeanInteraction.angularCarrierTerm_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α H : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {h : MeanIncrementBounds.Triple D} (hh : MeanIncrementBounds.IncrementBounds s H h) {b : CorrectionState.HarmonicBlock D} (hb : CorrectionState.HarmonicBlock.WaveBounds s P α b) (hkp : WeightedClasses.BandBound s (-(1 / 2)) fun (n : ℕ) => ↑(b.angularFrequency n)) {j : ℤ} (hj : j ≠ 0) (i : Fin 3) : WeightedClasses.WaveClass s P (α + H - 1 / 2) fun (n : ℕ) (x : D) => angularCarrierTerm c b h j n x i

theorem NavierStokes.HarmonicMeanInteraction.meanCross_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α H : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hκ : κ ≤ 1 / 2) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {h : MeanIncrementBounds.Triple D} (hh : MeanIncrementBounds.IncrementBounds s H h) {b : CorrectionState.HarmonicBlock D} (hb : CorrectionState.HarmonicBlock.WaveBounds s P α b) (hN : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (slowNormal c ho hR b.phase n x).ofLp i) (hk : WeightedClasses.BandBound s (-(1 / 2)) b.frequency) (hkp : WeightedClasses.BandBound s (-(1 / 2)) fun (n : ℕ) => ↑(b.angularFrequency n)) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) {j : ℤ} (hj : j ≠ 0) (i : Fin 3) : WeightedClasses.WaveClass s P (α + H - 1 / 2) fun (n : ℕ) (x : D) => (meanCross c h b n i).coeff j x

theorem NavierStokes.HarmonicMeanInteraction.realMeanCross_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α H : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hκ : κ ≤ 1 / 2) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {h : MeanIncrementBounds.Triple D} (hh : MeanIncrementBounds.IncrementBounds s H h) {b : CorrectionState.HarmonicBlock D} (hb : CorrectionState.HarmonicBlock.WaveBounds s P α b) (hN : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (slowNormal c ho hR b.phase n x).ofLp i) (hk : WeightedClasses.BandBound s (-(1 / 2)) b.frequency) (hkp : WeightedClasses.BandBound s (-(1 / 2)) fun (n : ℕ) => ↑(b.angularFrequency n)) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) {j : ℤ} (hj : j ≠ 0) (i : Fin 3) : WeightedClasses.WaveClass s P (α + H - 1 / 2) fun (n : ℕ) (x : D) => (HarmonicResidual.realCoefficients (meanCross c h b n i)).coeff j x

The actual output residual blocks

theorem NavierStokes.HarmonicMeanInteraction.nonconstant_apply_of_ne {D : Type} (a : HarmonicFields.Coefficients D) {j : ℤ} (hj : j ≠ 0) (x : D) : (HarmonicResidual.nonconstant a).coeff j x = a.coeff j x

theorem NavierStokes.HarmonicMeanInteraction.residualBlock_mean_update {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s₀ s₁ : CorrectionState.State D) (h : MeanIncrementBounds.Triple D) (he : s₁.mean = MeanIncrementBounds.updated s₀.mean h) (b : CorrectionState.HarmonicBlock D) (G₀ G₁ A₀ A₁ : HarmonicResidual.BlockCoefficients D) (n : ℕ) {x : D} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => HarmonicResidual.contextBase c n y i) x) (hM : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => HarmonicResidual.stateMean s₀ n y i) x) (hh : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => tripleField h n y i) x) (j : ℤ) (i : Fin 3) : ((HarmonicResidual.residualBlock c s₁ b G₁ A₁).velocity n i).coeff j x - ((HarmonicResidual.residualBlock c s₀ b G₀ A₀).velocity n i).coeff j x = (HarmonicResidual.nonconstant (HarmonicResidual.realCoefficients (meanCross c h b n i - (G₁ n i - G₀ n i) - (A₁ n i - A₀ n i)))).coeff j x

theorem NavierStokes.HarmonicMeanInteraction.band_zero_coefficient {D : Type} {a : HarmonicFields.Coefficients D} (ha : HarmonicFields.BandLimited a 0) {j : ℤ} (hj : j ≠ 0) : a.coeff j = 0

theorem NavierStokes.HarmonicMeanInteraction.residualBlock_axisymmetric_alias_update {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s₀ s₁ : CorrectionState.State D) (h : MeanIncrementBounds.Triple D) (he : s₁.mean = MeanIncrementBounds.updated s₀.mean h) (b : CorrectionState.HarmonicBlock D) (G A₀ A₁ : HarmonicResidual.BlockCoefficients D) (hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A₁ n i - A₀ n i) 0) (n : ℕ) {x : D} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => HarmonicResidual.contextBase c n y i) x) (hM : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => HarmonicResidual.stateMean s₀ n y i) x) (hh : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => tripleField h n y i) x) {j : ℤ} (hj : j ≠ 0) (i : Fin 3) : ((HarmonicResidual.residualBlock c s₁ b G A₁).velocity n i).coeff j x - ((HarmonicResidual.residualBlock c s₀ b G A₀).velocity n i).coeff j x = (HarmonicResidual.realCoefficients (meanCross c h b n i)).coeff j x

An axisymmetric alias change has no effect on nonzero harmonics. The Gaussian field is unchanged, so it cancels without a size assumption.

theorem NavierStokes.HarmonicMeanInteraction.tripleField_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {h : MeanIncrementBounds.Triple D} (hh : MeanIncrementBounds.SmoothTriple U h) (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : D) => tripleField h n x i) U

theorem NavierStokes.HarmonicMeanInteraction.residualBlock_mean_update_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α H : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hκ : κ ≤ 1 / 2) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) (s₀ s₁ : CorrectionState.State D) (h : MeanIncrementBounds.Triple D) (he : s₁.mean = MeanIncrementBounds.updated s₀.mean h) (hbase : MeanIncrementBounds.SmoothTriple s.domain c.base) (hmean : MeanIncrementBounds.SmoothTriple s.domain s₀.mean) (hh : MeanIncrementBounds.IncrementBounds s H h) (b : CorrectionState.HarmonicBlock D) (hb : CorrectionState.HarmonicBlock.WaveBounds s P α b) (hN : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (slowNormal c ho hR b.phase n x).ofLp i) (hk : WeightedClasses.BandBound s (-(1 / 2)) b.frequency) (hkp : WeightedClasses.BandBound s (-(1 / 2)) fun (n : ℕ) => ↑(b.angularFrequency n)) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (G A₀ A₁ : HarmonicResidual.BlockCoefficients D) (hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A₁ n i - A₀ n i) 0) {j : ℤ} (hj : j ≠ 0) (i : Fin 3) : WeightedClasses.WaveClass s P (α + H - 1 / 2) fun (n : ℕ) (x : D) => ((HarmonicResidual.residualBlock c s₁ b G A₁).velocity n i).coeff j x - ((HarmonicResidual.residualBlock c s₀ b G A₀).velocity n i).coeff j x

The resulting all-order class is derived for the actual residual-block coefficient difference, with no estimate assumed for that difference.

noncomputable def NavierStokes.HarmonicMeanInteraction.residualDifferenceBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s₀ s₁ : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A₀ A₁ : HarmonicResidual.BlockCoefficients D) : CorrectionState.HarmonicBlock D

Residual difference block, bundling velocity, pressure, frequency, phase and the required compatibility proofs.

Equations

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

theorem NavierStokes.HarmonicMeanInteraction.residualDifferenceBlock_field {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s₀ s₁ : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A₀ A₁ : HarmonicResidual.BlockCoefficients D) (n : ℕ) (x : D × ℝ) (i : Fin 3) : (residualDifferenceBlock c s₀ s₁ b G A₀ A₁).oscillation n x i = (HarmonicResidual.residualBlock c s₁ b G A₁).oscillation n x i - (HarmonicResidual.residualBlock c s₀ b G A₀).oscillation n x i

theorem NavierStokes.HarmonicMeanInteraction.residualDifferenceBlock_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α H : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hκ : κ ≤ 1 / 2) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) (s₀ s₁ : CorrectionState.State D) (h : MeanIncrementBounds.Triple D) (he : s₁.mean = MeanIncrementBounds.updated s₀.mean h) (hbase : MeanIncrementBounds.SmoothTriple s.domain c.base) (hmean : MeanIncrementBounds.SmoothTriple s.domain s₀.mean) (hh : MeanIncrementBounds.IncrementBounds s H h) (b : CorrectionState.HarmonicBlock D) (hb : CorrectionState.HarmonicBlock.WaveBounds s P α b) (hN : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (slowNormal c ho hR b.phase n x).ofLp i) (hk : WeightedClasses.BandBound s (-(1 / 2)) b.frequency) (hkp : WeightedClasses.BandBound s (-(1 / 2)) fun (n : ℕ) => ↑(b.angularFrequency n)) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (G A₀ A₁ : HarmonicResidual.BlockCoefficients D) (hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A₁ n i - A₀ n i) 0) : CorrectionState.HarmonicBlock.WaveBounds s P (α + H - 1 / 2) (residualDifferenceBlock c s₀ s₁ b G A₀ A₁)

Frequency support and physical cross-advection

theorem NavierStokes.HarmonicMeanInteraction.nonconstant_sub {D : Type} (a b : HarmonicFields.Coefficients D) : HarmonicResidual.nonconstant (a - b) = HarmonicResidual.nonconstant a - HarmonicResidual.nonconstant b

noncomputable def NavierStokes.HarmonicMeanInteraction.transportDifference {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (B₀ B₁ : D → HarmonicCalculus.ComplexVector) (a : HarmonicResidual.VectorCoefficients D) (i : Fin 3) : HarmonicFields.Coefficients D

Transport difference as an element of Coefficients D.

Equations

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

theorem NavierStokes.HarmonicMeanInteraction.nonlinear_difference_algebra {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (B₀ B₁ : D → HarmonicCalculus.ComplexVector) (a : HarmonicResidual.VectorCoefficients D) (p : HarmonicFields.Coefficients D) (i : Fin 3) : HarmonicResidual.nonlinearResidual g k Φ kp (HarmonicResidual.constantVector B₁) a p i - HarmonicResidual.nonlinearResidual g k Φ kp (HarmonicResidual.constantVector B₀) a p i = transportDifference g k Φ kp B₀ B₁ a i

theorem NavierStokes.HarmonicMeanInteraction.transportDifference_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (B₀ B₁ : D → HarmonicCalculus.ComplexVector) {a : HarmonicResidual.VectorCoefficients D} {N : ℕ} (ha : ∀ (i : Fin 3), HarmonicFields.BandLimited (a i) N) (i : Fin 3) : HarmonicFields.BandLimited (transportDifference g k Φ kp B₀ B₁ a i) N

theorem NavierStokes.HarmonicMeanInteraction.residualDifferenceBlock_algebra {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s₀ s₁ : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A₀ A₁ : HarmonicResidual.BlockCoefficients D) (n : ℕ) (i : Fin 3) : (residualDifferenceBlock c s₀ s₁ b G A₀ A₁).velocity n i = HarmonicResidual.nonconstant (HarmonicResidual.realCoefficients (transportDifference (HarmonicResidual.contextFrame c n) (b.frequency n) (b.phase n) (b.angularFrequency n) (HarmonicResidual.contextBase c n + HarmonicResidual.stateMean s₀ n) (HarmonicResidual.contextBase c n + HarmonicResidual.stateMean s₁ n) (blockAmplitude b n) i - (A₁ n i - A₀ n i)))

theorem NavierStokes.HarmonicMeanInteraction.residualDifferenceBlock_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s₀ s₁ : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A₀ A₁ : HarmonicResidual.BlockCoefficients D) {N : ℕ} (hb : b.BandLimited N) (hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A₁ n i - A₀ n i) 0) : (residualDifferenceBlock c s₀ s₁ b G A₀ A₁).BandLimited N

A mean-only update preserves the existing harmonic-value bound.

theorem NavierStokes.HarmonicMeanInteraction.residualDifferenceBlock_conjugate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s₀ s₁ : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A₀ A₁ : HarmonicResidual.BlockCoefficients D) (n : ℕ) (i : Fin 3) : HarmonicFields.ConjugateSymmetric ((residualDifferenceBlock c s₀ s₁ b G A₀ A₁).velocity n i)

theorem NavierStokes.HarmonicMeanInteraction.residualDifferenceBlock_zero_mode {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s₀ s₁ : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A₀ A₁ : HarmonicResidual.BlockCoefficients D) (n : ℕ) (i : Fin 3) : ((residualDifferenceBlock c s₀ s₁ b G A₀ A₁).velocity n i).coeff 0 = 0

theorem NavierStokes.HarmonicMeanInteraction.crossCoefficients_field {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : HarmonicResidual.Frame D) (k : ℝ) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (kp : ℤ) (m : D → HarmonicCalculus.ComplexVector) (hm : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : D) => m x i) U) (a : HarmonicResidual.VectorCoefficients D) (ha : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (a i)) {x : D × ℝ} (hx : x ∈ HarmonicResidual.liftDomain U) : HarmonicResidual.vectorField (crossCoefficients g k Φ kp m a) k Φ kp x = LinearWaveResidual.transport (fun (y : D × ℝ) => g.radius y.1) (HarmonicResidual.liftDirection g.radial) HarmonicResidual.angularDirection (HarmonicResidual.liftDirection g.axial) (fun (y : D × ℝ) => m y.1) (HarmonicResidual.vectorField a k Φ kp) x + LinearWaveResidual.transport (fun (y : D × ℝ) => g.radius y.1) (HarmonicResidual.liftDirection g.radial) HarmonicResidual.angularDirection (HarmonicResidual.liftDirection g.axial) (HarmonicResidual.vectorField a k Φ kp) (fun (y : D × ℝ) => m y.1) x

The same finite coefficients evaluate to the two actual cross-advection fields.

theorem NavierStokes.HarmonicMeanInteraction.grouped_wave_change {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {U : Set D} (hU : IsOpen U) {c : CorrectionState.Context D} {s₀ s₁ : CorrectionState.State D} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {G A₀ A₁ : ι → HarmonicResidual.BlockCoefficients D} (hrep₀ : HarmonicResidual.BlockRepresentation labels blocks G A₀ s₀) (hrep₁ : HarmonicResidual.BlockRepresentation labels blocks G A₁ s₁) {n : ℕ} (h₀ : HarmonicResidual.ExtractionRegular U c s₀ labels blocks G A₀ n) (h₁ : HarmonicResidual.ExtractionRegular U c s₁ labels blocks G A₁ n) {x : D × ℝ} (hx : x ∈ HarmonicResidual.liftDomain U) (i : Fin 3) : HarmonicResidual.stateGoodWaveResidual c s₁ n x i - HarmonicResidual.stateGoodWaveResidual c s₀ n x i = ∑ l ∈ labels n, (residualDifferenceBlock c s₀ s₁ (blocks l) (G l) (A₀ l) (A₁ l)).oscillation n x i

The computed block differences reconstruct the actual change in the good nonconstant residual. This is an identity, with no uniform sum estimate assumed.

theorem NavierStokes.HarmonicMeanInteraction.stateMean_addIncrement {D : Type} (s₀ : CorrectionState.State D) (h : MeanIncrementBounds.Triple D) (δp : CorrectionState.ScalarField D) (δe : CorrectionState.ExcludedErrors D) : (s₀.addIncrement h δp 0 0 δe).mean = MeanIncrementBounds.updated s₀.mean h

A recomputed mean pressure is unrestricted in this application; its contribution is in the mean residual, not in the fixed label's wave block.

noncomputable def NavierStokes.HarmonicWaveInteraction.pullbackStrip {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData D) (L : E →L[ℝ] D) : WeightedClasses.StripData E

Pullback strip, bundling domain, isOpen_domain, epsilon, epsilon_pos and the required compatibility proofs.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.norm_jet_comp_linear {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : D → F} {U : Set D} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (L : E →L[ℝ] D) {x : E} (hx : L x ∈ U) (m : ℕ) : ‖iteratedFDeriv ℝ m (f ∘ ⇑L) x‖ ≤ ‖iteratedFDeriv ℝ m f (L x)‖ * ‖L‖ ^ m

theorem NavierStokes.HarmonicWaveInteraction.class_pullback {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → F} (hf : WeightedClasses.MemClass s w α f) (L : E →L[ℝ] D) (hL : ‖L‖ ≤ 1) : WeightedClasses.MemClass (pullbackStrip s L) (fun (n : ℕ) (x : E) => w n (L x)) α fun (n : ℕ) (x : E) => f n (L x)

noncomputable def NavierStokes.HarmonicWaveInteraction.projection {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] : D × ℝ →L[ℝ] D

Projection, given by ContinuousLinearMap.fst ℝ D ℝ.

Equations

• NavierStokes.HarmonicWaveInteraction.projection = ContinuousLinearMap.fst ℝ D ℝ

noncomputable def NavierStokes.HarmonicWaveInteraction.inclusion {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] : D →L[ℝ] D × ℝ

Inclusion, given by (ContinuousLinearMap.id ℝ D).prod (0 : D →L[ℝ] ℝ).

Equations

• NavierStokes.HarmonicWaveInteraction.inclusion = (ContinuousLinearMap.id ℝ D).prod 0

theorem NavierStokes.HarmonicWaveInteraction.projection_norm {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] : ‖projection‖ ≤ 1

theorem NavierStokes.HarmonicWaveInteraction.inclusion_norm {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] : ‖inclusion‖ ≤ 1

noncomputable def NavierStokes.HarmonicWaveInteraction.productStrip {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) : WeightedClasses.StripData (D × ℝ)

Product strip, given by pullbackStrip s projection.

Equations

• NavierStokes.HarmonicWaveInteraction.productStrip s = NavierStokes.HarmonicWaveInteraction.pullbackStrip s NavierStokes.HarmonicWaveInteraction.projection

theorem NavierStokes.HarmonicWaveInteraction.class_lift {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → F} (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass (productStrip s) (fun (n : ℕ) (p : D × ℝ) => w n p.1) α fun (n : ℕ) (p : D × ℝ) => f n p.1

theorem NavierStokes.HarmonicWaveInteraction.class_slice {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D × ℝ → F} (hf : WeightedClasses.MemClass (productStrip s) (fun (n : ℕ) (p : D × ℝ) => w n p.1) α f) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => f n (x, 0)

noncomputable def NavierStokes.HarmonicWaveInteraction.liftedGeometry {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (G : WaveInteractionBounds.Geometry s κ) : WaveInteractionBounds.Geometry (productStrip s) κ

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

Equations

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

noncomputable def NavierStokes.HarmonicWaveInteraction.fullPhase {D : Type} (b : CorrectionState.HarmonicBlock D) (n : ℕ) (p : D × ℝ) : ℝ

Full phase, given by b.phase n p.1 + ((b.angularFrequency n : ℝ) / b.frequency n) * p.2.

Equations

• NavierStokes.HarmonicWaveInteraction.fullPhase b n p = b.phase n p.1 + ↑(b.angularFrequency n) / b.frequency n * p.2

theorem NavierStokes.HarmonicWaveInteraction.fullPhase_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (b : CorrectionState.HarmonicBlock D) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (b.phase n) s.domain) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fullPhase b n) (productStrip s).domain

noncomputable def NavierStokes.HarmonicWaveInteraction.amplitude {D : Type} (b : CorrectionState.HarmonicBlock D) (j : ℤ) (n : ℕ) (x : D) : HarmonicCalculus.ComplexVector

Amplitude, defined pointwise by blockAmplitude b n i j x.

Equations

• NavierStokes.HarmonicWaveInteraction.amplitude b j n x i = (NavierStokes.HarmonicMeanInteraction.blockAmplitude b n i).coeff j x

noncomputable def NavierStokes.HarmonicWaveInteraction.singleMode {D : Type} (b : CorrectionState.HarmonicBlock D) (j : ℤ) (n : ℕ) (p : D × ℝ) : HarmonicCalculus.ComplexVector

Single mode, constructed using HarmonicResidual.vectorField.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.singleMode_eq {D : Type} (b : CorrectionState.HarmonicBlock D) (j : ℤ) (n : ℕ) (hk : b.frequency n ≠ 0) : singleMode b j n = HarmonicCalculus.vectorMode (b.frequency n * ↑j) (fullPhase b n) fun (p : D × ℝ) => amplitude b j n p.1

def NavierStokes.HarmonicWaveInteraction.ModeSolenoidal {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (c : CorrectionState.Context D) (b : CorrectionState.HarmonicBlock D) : Prop

The primitive divergence condition is imposed on each actual harmonic field.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.lifted_amplitude_angularIndependent {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α : ℝ} {P : ℕ → D → ℝ} (G : WaveInteractionBounds.Geometry s κ) {b : CorrectionState.HarmonicBlock D} (hb : CorrectionState.HarmonicBlock.WaveBounds s P α b) {j : ℤ} (hj : j ≠ 0) : WaveInteractionBounds.AngularIndependent (liftedGeometry G) fun (n : ℕ) (p : D × ℝ) => amplitude b j n p.1

theorem NavierStokes.HarmonicWaveInteraction.along_fst {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (V : D → D) {f : D → F} {p : D × ℝ} (hf : DifferentiableAt ℝ f p.1) : HarmonicCalculus.along (HarmonicResidual.liftDirection V) (fun (q : D × ℝ) => f q.1) p = HarmonicCalculus.along V f p.1

theorem NavierStokes.HarmonicWaveInteraction.fullPhase_hasFDerivAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (b : CorrectionState.HarmonicBlock D) (n : ℕ) {p : D × ℝ} (hΦ : DifferentiableAt ℝ (b.phase n) p.1) : HasFDerivAt (fullPhase b n) (fderiv ℝ (b.phase n) p.1 ∘SL projection + (↑(b.angularFrequency n) / b.frequency n) • ContinuousLinearMap.snd ℝ D ℝ) p

theorem NavierStokes.HarmonicWaveInteraction.along_fullPhase_lift {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (b : CorrectionState.HarmonicBlock D) (n : ℕ) (V : D → D) {p : D × ℝ} (hΦ : DifferentiableAt ℝ (b.phase n) p.1) : HarmonicCalculus.along (HarmonicResidual.liftDirection V) (fullPhase b n) p = HarmonicCalculus.along V (b.phase n) p.1

theorem NavierStokes.HarmonicWaveInteraction.along_fullPhase_angular {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (b : CorrectionState.HarmonicBlock D) (n : ℕ) {p : D × ℝ} (hΦ : DifferentiableAt ℝ (b.phase n) p.1) : HarmonicCalculus.along HarmonicResidual.angularDirection (fullPhase b n) p = ↑(b.angularFrequency n) / b.frequency n

noncomputable def NavierStokes.HarmonicWaveInteraction.orderedKernel {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp l : ℤ) (a b : D → HarmonicCalculus.ComplexVector) (x : D) (i : Fin 3) : ℂ

The exact ordered coefficient from harmonic j advecting harmonic l. The first index is carried by the first input function; l enters the derivatives.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.orderedKernel_eq_fullCoefficient {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) (carrierData : CorrectionState.HarmonicBlock D) (a b : WaveInteractionBounds.Family D) (l : ℤ) (n : ℕ) {x : D} (hx : x ∈ s.domain) (hk : carrierData.frequency n ≠ 0) (hΦ : DifferentiableAt ℝ (carrierData.phase n) x) (hb : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => b n y i) x) (i : Fin 3) : orderedKernel (HarmonicResidual.contextFrame c n) (carrierData.frequency n) (carrierData.phase n) (carrierData.angularFrequency n) l (a n) (b n) x i = WaveInteractionBounds.sameCoefficient (liftedGeometry (HarmonicMeanInteraction.slowGeometry c ho hR)) (fullPhase carrierData) (fun (n : ℕ) => carrierData.frequency n * ↑l) (fun (n : ℕ) (p : D × ℝ) => a n p.1) (fun (n : ℕ) (p : D × ℝ) => b n p.1) n (x, 0) i

theorem NavierStokes.HarmonicWaveInteraction.orderedKernel_raw_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : CorrectionState.HarmonicBlock D} (ha : CorrectionState.HarmonicBlock.WaveBounds s P α a) (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hdiv : ModeSolenoidal s c a) {j l : ℤ} (hj : j ≠ 0) (hl : l ≠ 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) => orderedKernel (HarmonicResidual.contextFrame c n) (a.frequency n) (a.phase n) (a.angularFrequency n) l (amplitude a j n) (amplitude b l n) x i

The first harmonic is used only through its genuine divergence equation. Its carrier cancels against the second harmonic with a bounded integer ratio.

def NavierStokes.HarmonicWaveInteraction.ZeroMode {D : Type} (b : CorrectionState.HarmonicBlock D) : Prop

Oscillatory input blocks have no stored velocity at harmonic zero.

Equations

• NavierStokes.HarmonicWaveInteraction.ZeroMode b = ∀ (n : ℕ) (i : Fin 3), (b.velocity n i).coeff 0 = 0

theorem NavierStokes.HarmonicWaveInteraction.amplitude_zero {D : Type} {b : CorrectionState.HarmonicBlock D} (hb : ZeroMode b) (n : ℕ) : amplitude b 0 n = 0

theorem NavierStokes.HarmonicWaveInteraction.orderedKernel_zero_left {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp l : ℤ) (b : D → HarmonicCalculus.ComplexVector) (x : D) (i : Fin 3) : orderedKernel g k Φ kp l 0 b x i = 0

theorem NavierStokes.HarmonicWaveInteraction.orderedKernel_zero_right {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp l : ℤ) (a : D → HarmonicCalculus.ComplexVector) (x : D) (i : Fin 3) : orderedKernel g k Φ kp l a 0 x i = 0

theorem NavierStokes.HarmonicWaveInteraction.orderedKernel_raw_class_all {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : CorrectionState.HarmonicBlock D} (ha : CorrectionState.HarmonicBlock.WaveBounds s P α a) (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (ha0 : ZeroMode a) (hb0 : ZeroMode b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hdiv : ModeSolenoidal s c a) (j l : ℤ) (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) => orderedKernel (HarmonicResidual.contextFrame c n) (a.frequency n) (a.phase n) (a.angularFrequency n) l (amplitude a j n) (amplitude b l n) x i

noncomputable def NavierStokes.HarmonicWaveInteraction.harmonicRange (N : ℕ) : Finset ℤ

A common finite range is fixed for the whole family, not chosen anew on each band. This is the finiteness needed by the uniform class estimates.

Equations

• NavierStokes.HarmonicWaveInteraction.harmonicRange N = Finset.Icc (-↑N) ↑N

theorem NavierStokes.HarmonicWaveInteraction.band_support_range {D : Type} {a : HarmonicFields.Coefficients D} {N : ℕ} (ha : HarmonicFields.BandLimited a N) : a.support ⊆ harmonicRange N

theorem NavierStokes.HarmonicWaveInteraction.convolution_apply_finset {D : Type} (a b : HarmonicFields.Coefficients D) (K : Finset ℤ) (ha : a.support ⊆ K) (m : ℤ) (x : D) : (a * b).coeff m x = ∑ j ∈ K, a.coeff j x * b.coeff (m - j) x

theorem NavierStokes.HarmonicWaveInteraction.transport_convolution {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (a b : HarmonicResidual.VectorCoefficients D) (K : Finset ℤ) (ha : ∀ (i : Fin 3), HarmonicFields.Coefficients.support (a i) ⊆ K) (m : ℤ) (x : D) (i : Fin 3) : (HarmonicResidual.transport g k Φ kp a b i).coeff m x = ∑ j ∈ K, orderedKernel g k Φ kp (m - j) (fun (y : D) (r : Fin 3) => (a r).coeff j y) (fun (y : D) (r : Fin 3) => (b r).coeff (m - j) y) x i

theorem NavierStokes.HarmonicWaveInteraction.transport_raw_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : CorrectionState.HarmonicBlock D} {N : ℕ} (ha : CorrectionState.HarmonicBlock.WaveBounds s P α a) (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (ha0 : ZeroMode a) (hb0 : ZeroMode b) (hN : a.BandLimited N) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hdiv : ModeSolenoidal s c a) (m : ℤ) (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) => (HarmonicResidual.transport (HarmonicResidual.contextFrame c n) (a.frequency n) (a.phase n) (a.angularFrequency n) (HarmonicMeanInteraction.blockAmplitude a n) (HarmonicMeanInteraction.blockAmplitude b n) i).coeff m x

theorem NavierStokes.HarmonicWaveInteraction.transport_wave_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : CorrectionState.HarmonicBlock D} {N : ℕ} (ha : CorrectionState.HarmonicBlock.WaveBounds s P α a) (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (ha0 : ZeroMode a) (hb0 : ZeroMode b) (hN : a.BandLimited N) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hdiv : ModeSolenoidal s c a) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (m : ℤ) (i : Fin 3) : WeightedClasses.WaveClass s P (α + β - κ) fun (n : ℕ) (x : D) => (HarmonicResidual.transport (HarmonicResidual.contextFrame c n) (a.frequency n) (a.phase n) (a.angularFrequency n) (HarmonicMeanInteraction.blockAmplitude a n) (HarmonicMeanInteraction.blockAmplitude b n) i).coeff m x

theorem NavierStokes.HarmonicWaveInteraction.transport_mean_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : CorrectionState.HarmonicBlock D} {N : ℕ} (ha : CorrectionState.HarmonicBlock.WaveBounds s P α a) (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (ha0 : ZeroMode a) (hb0 : ZeroMode b) (hN : a.BandLimited N) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hdiv : ModeSolenoidal s c a) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (m : ℤ) (i : Fin 3) : WeightedClasses.MeanClass s (α + β - κ) fun (n : ℕ) (x : D) => (HarmonicResidual.transport (HarmonicResidual.contextFrame c n) (a.frequency n) (a.phase n) (a.angularFrequency n) (HarmonicMeanInteraction.blockAmplitude a n) (HarmonicMeanInteraction.blockAmplitude b n) i).coeff m x

noncomputable def NavierStokes.HarmonicWaveInteraction.withCarrier {D : Type} (carrierData b : CorrectionState.HarmonicBlock D) : CorrectionState.HarmonicBlock D

Coefficients evaluated using the original label's carrier.

Equations

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

noncomputable def NavierStokes.HarmonicWaveInteraction.addBlock {D : Type} (a b : CorrectionState.HarmonicBlock D) : CorrectionState.HarmonicBlock D

The updated label retains its carrier, including its angular frequency.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.addBlock_oscillation {D : Type} (a b : CorrectionState.HarmonicBlock D) (n : ℕ) (p : D × ℝ) (i : Fin 3) : (addBlock a b).oscillation n p i = a.oscillation n p i + (withCarrier a b).oscillation n p i

theorem NavierStokes.HarmonicWaveInteraction.addBlock_pressure {D : Type} (a b : CorrectionState.HarmonicBlock D) (n : ℕ) (p : D × ℝ) : (addBlock a b).oscillatoryPressure n p = a.oscillatoryPressure n p + (withCarrier a b).oscillatoryPressure n p

theorem NavierStokes.HarmonicWaveInteraction.blockAmplitude_addBlock {D : Type} (a b : CorrectionState.HarmonicBlock D) (n : ℕ) : HarmonicMeanInteraction.blockAmplitude (addBlock a b) n = HarmonicMeanInteraction.blockAmplitude a n + HarmonicMeanInteraction.blockAmplitude b n

noncomputable def NavierStokes.HarmonicWaveInteraction.blockTransport {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (carrierData a b : CorrectionState.HarmonicBlock D) : HarmonicResidual.BlockCoefficients D

Block transport as an element of HarmonicResidual.BlockCoefficients D.

Equations

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

noncomputable def NavierStokes.HarmonicWaveInteraction.nonlinearCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (a b : CorrectionState.HarmonicBlock D) : HarmonicResidual.BlockCoefficients D

All three actual quadratic terms introduced by adding one wave block.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.mixed_wave_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : CorrectionState.HarmonicBlock D} {M N : ℕ} (ha : CorrectionState.HarmonicBlock.WaveBounds s P α a) (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (ha0 : ZeroMode a) (hb0 : ZeroMode b) (hM : a.BandLimited M) (hN : b.BandLimited N) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hda : ModeSolenoidal s c a) (hdb : ModeSolenoidal s c (withCarrier a b)) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (j : ℤ) (i : Fin 3) : WeightedClasses.WaveClass s P (α + β - κ) fun (n : ℕ) (x : D) => (blockTransport c a a b n i).coeff j x + (blockTransport c a b a n i).coeff j x

theorem NavierStokes.HarmonicWaveInteraction.square_wave_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ β : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) (a : CorrectionState.HarmonicBlock D) {b : CorrectionState.HarmonicBlock D} {N : ℕ} (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (hb0 : ZeroMode b) (hN : b.BandLimited N) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hdb : ModeSolenoidal s c (withCarrier a b)) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (j : ℤ) (i : Fin 3) : WeightedClasses.WaveClass s P (β + β - κ) fun (n : ℕ) (x : D) => (blockTransport c a b b n i).coeff j x

theorem NavierStokes.HarmonicWaveInteraction.nonlinearCoefficients_wave_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : CorrectionState.HarmonicBlock D} {M N : ℕ} (ha : CorrectionState.HarmonicBlock.WaveBounds s P α a) (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (ha0 : ZeroMode a) (hb0 : ZeroMode b) (hM : a.BandLimited M) (hN : b.BandLimited N) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hda : ModeSolenoidal s c a) (hdb : ModeSolenoidal s c (withCarrier a b)) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (j : ℤ) (i : Fin 3) : WeightedClasses.WaveClass s P (min (α + β - κ) (β + β - κ)) fun (n : ℕ) (x : D) => (nonlinearCoefficients c a b n i).coeff j x

noncomputable def NavierStokes.HarmonicWaveInteraction.nonlinearErrorBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (a b : CorrectionState.HarmonicBlock D) : CorrectionState.HarmonicBlock D

Nonlinear error block, bundling velocity, pressure, frequency, phase and the required compatibility proofs.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.nonlinearErrorBlock_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : CorrectionState.HarmonicBlock D} {M N : ℕ} (ha : CorrectionState.HarmonicBlock.WaveBounds s P α a) (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (ha0 : ZeroMode a) (hb0 : ZeroMode b) (hM : a.BandLimited M) (hN : b.BandLimited N) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hda : ModeSolenoidal s c a) (hdb : ModeSolenoidal s c (withCarrier a b)) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : CorrectionState.HarmonicBlock.WaveBounds s P (min (α + β - κ) (β + β - κ)) (nonlinearErrorBlock c a b)

theorem NavierStokes.HarmonicWaveInteraction.nonlinearErrorBlock_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) {a b : CorrectionState.HarmonicBlock D} {M N : ℕ} (ha : a.BandLimited M) (hb : b.BandLimited N) : (nonlinearErrorBlock c a b).BandLimited (max (M + N) (N + N))

theorem NavierStokes.HarmonicWaveInteraction.nonlinearErrorBlock_conjugate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (a b : CorrectionState.HarmonicBlock D) (n : ℕ) (i : Fin 3) : HarmonicFields.ConjugateSymmetric ((nonlinearErrorBlock c a b).velocity n i)

theorem NavierStokes.HarmonicWaveInteraction.nonlinearErrorBlock_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (a b : CorrectionState.HarmonicBlock D) : ZeroMode (nonlinearErrorBlock c a b)

Identification with the actual differentiated residual

theorem NavierStokes.HarmonicWaveInteraction.coefficient_eq_of_field_eq_at {D : Type} (a b : HarmonicFields.Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (j : ℤ) (x : D) (he : ∀ (θ : ℝ), HarmonicFields.field a k Φ kp (x, θ) = HarmonicFields.field b k Φ kp (x, θ)) : a.coeff j x = b.coeff j x

theorem NavierStokes.HarmonicWaveInteraction.vectorField_add {D : Type} (a b : HarmonicResidual.VectorCoefficients D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) : HarmonicResidual.vectorField (a + b) k Φ kp = HarmonicResidual.vectorField a k Φ kp + HarmonicResidual.vectorField b k Φ kp

theorem NavierStokes.HarmonicWaveInteraction.scalarField_add {D : Type} (a b : HarmonicFields.Coefficients D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) : HarmonicFields.field (a + b) k Φ kp = HarmonicFields.field a k Φ kp + HarmonicFields.field b k Φ kp

theorem NavierStokes.HarmonicWaveInteraction.nonlinear_update_coefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : HarmonicResidual.Frame D) (hr : ContDiffOn ℝ (↑⊤) g.radial U) (hz : ContDiffOn ℝ (↑⊤) g.axial U) (k : ℝ) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) {kp : ℤ} (hkp : kp ≠ 0) (B a b : HarmonicResidual.VectorCoefficients D) (p q : HarmonicFields.Coefficients D) (hB : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (B i)) (ha : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (a i)) (hb : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (b i)) (hp : HarmonicResidual.SmoothCoefficients U p) (hq : HarmonicResidual.SmoothCoefficients U q) {x : D} (hx : x ∈ U) (j : ℤ) (i : Fin 3) : (HarmonicResidual.nonlinearResidual g k Φ kp B (a + b) (p + q) i).coeff j x - (HarmonicResidual.nonlinearResidual g k Φ kp B a p i).coeff j x = (HarmonicResidual.linearResidual g k Φ kp B b q i).coeff j x + (HarmonicResidual.transport g k Φ kp a b i).coeff j x + (HarmonicResidual.transport g k Φ kp b a i).coeff j x + (HarmonicResidual.transport g k Φ kp b b i).coeff j x

The coefficient identity is extracted from the proved product rules for the actual cylindrical differential operators.

theorem NavierStokes.HarmonicWaveInteraction.linear_mean_difference {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (B m : D → HarmonicCalculus.ComplexVector) (a : HarmonicResidual.VectorCoefficients D) (p : HarmonicFields.Coefficients D) {x : D} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => B y i) x) (hm : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => m y i) x) (j : ℤ) (i : Fin 3) : (HarmonicResidual.linearResidual g k Φ kp (HarmonicResidual.constantVector (B + m)) a p i).coeff j x - (HarmonicResidual.linearResidual g k Φ kp (HarmonicResidual.constantVector B) a p i).coeff j x = (HarmonicMeanInteraction.crossCoefficients g k Φ kp m a i).coeff j x

theorem NavierStokes.HarmonicWaveInteraction.nonlinear_update_with_mean {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : HarmonicResidual.Frame D) (hr : ContDiffOn ℝ (↑⊤) g.radial U) (hz : ContDiffOn ℝ (↑⊤) g.axial U) (k : ℝ) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) {kp : ℤ} (hkp : kp ≠ 0) (B M : D → HarmonicCalculus.ComplexVector) (a b : HarmonicResidual.VectorCoefficients D) (p q : HarmonicFields.Coefficients D) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U) (ha : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (a i)) (hb : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (b i)) (hp : HarmonicResidual.SmoothCoefficients U p) (hq : HarmonicResidual.SmoothCoefficients U q) {x : D} (hx : x ∈ U) (j : ℤ) (i : Fin 3) : (HarmonicResidual.nonlinearResidual g k Φ kp (HarmonicResidual.constantVector (B + M)) (a + b) (p + q) i).coeff j x - (HarmonicResidual.nonlinearResidual g k Φ kp (HarmonicResidual.constantVector (B + M)) a p i).coeff j x = (HarmonicResidual.linearResidual g k Φ kp (HarmonicResidual.constantVector B) b q i).coeff j x + (HarmonicMeanInteraction.crossCoefficients g k Φ kp M b i).coeff j x + (HarmonicResidual.transport g k Φ kp a b i).coeff j x + (HarmonicResidual.transport g k Φ kp b a i).coeff j x + (HarmonicResidual.transport g k Φ kp b b i).coeff j x

noncomputable def NavierStokes.HarmonicWaveInteraction.linearCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (carrierData b : CorrectionState.HarmonicBlock D) : HarmonicResidual.BlockCoefficients D

Linear coefficients as an element of HarmonicResidual.BlockCoefficients D.

Equations

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

noncomputable def NavierStokes.HarmonicWaveInteraction.waveChangeCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (a b : CorrectionState.HarmonicBlock D) (g A₀ A₁ : HarmonicResidual.BlockCoefficients D) : HarmonicResidual.BlockCoefficients D

The complete wave change before removing its zero mode. The Gaussian increment and the alias difference remain literal coefficient fields.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.residualCoefficients_wave_update {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (c : CorrectionState.Context D) (u₀ u₁ : CorrectionState.State D) (he : u₁.mean = u₀.mean) (a b : CorrectionState.HarmonicBlock D) (G g A₀ A₁ : HarmonicResidual.BlockCoefficients D) (n : ℕ) (hr : ContDiffOn ℝ (↑⊤) (HarmonicResidual.contextFrame c n).radial U) (hz : ContDiffOn ℝ (↑⊤) (HarmonicResidual.contextFrame c n).axial U) (hΦ : ContDiffOn ℝ (↑⊤) (a.phase n) U) (hkp : a.angularFrequency n ≠ 0) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => HarmonicResidual.contextBase c n y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => HarmonicResidual.stateMean u₀ n y i) U) (ha : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (a.velocity n i)) (hb : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (b.velocity n i)) (hp : HarmonicResidual.SmoothCoefficients U (a.pressure n)) (hq : HarmonicResidual.SmoothCoefficients U (b.pressure n)) {x : D} (hx : x ∈ U) (j : ℤ) (i : Fin 3) : ((HarmonicResidual.ofBlock (addBlock a b) (G + g) A₁ n).residualCoefficients (HarmonicResidual.contextFrame c n) (HarmonicResidual.contextBase c n) (HarmonicResidual.stateMean u₁ n) i).coeff j x - ((HarmonicResidual.ofBlock a G A₀ n).residualCoefficients (HarmonicResidual.contextFrame c n) (HarmonicResidual.contextBase c n) (HarmonicResidual.stateMean u₀ n) i).coeff j x = (HarmonicResidual.realCoefficients (waveChangeCoefficients c u₀ a b g A₀ A₁ n i)).coeff j x

theorem NavierStokes.HarmonicWaveInteraction.residualBlock_wave_update {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (c : CorrectionState.Context D) (u₀ u₁ : CorrectionState.State D) (he : u₁.mean = u₀.mean) (a b : CorrectionState.HarmonicBlock D) (G g A₀ A₁ : HarmonicResidual.BlockCoefficients D) (n : ℕ) (hr : ContDiffOn ℝ (↑⊤) (HarmonicResidual.contextFrame c n).radial U) (hz : ContDiffOn ℝ (↑⊤) (HarmonicResidual.contextFrame c n).axial U) (hΦ : ContDiffOn ℝ (↑⊤) (a.phase n) U) (hkp : a.angularFrequency n ≠ 0) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => HarmonicResidual.contextBase c n y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => HarmonicResidual.stateMean u₀ n y i) U) (ha : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (a.velocity n i)) (hb : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (b.velocity n i)) (hp : HarmonicResidual.SmoothCoefficients U (a.pressure n)) (hq : HarmonicResidual.SmoothCoefficients U (b.pressure n)) {x : D} (hx : x ∈ U) (j : ℤ) (i : Fin 3) : ((HarmonicResidual.residualBlock c u₁ (addBlock a b) (G + g) A₁).velocity n i).coeff j x - ((HarmonicResidual.residualBlock c u₀ a G A₀).velocity n i).coeff j x = (HarmonicResidual.nonconstant (HarmonicResidual.realCoefficients (waveChangeCoefficients c u₀ a b g A₀ A₁ n i))).coeff j x

noncomputable def NavierStokes.HarmonicWaveInteraction.interactionCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (a b : CorrectionState.HarmonicBlock D) : HarmonicResidual.BlockCoefficients D

Interaction coefficients, given by meanCross c u.mean (withCarrier a b) + nonlinearCoefficients c a b.

Equations

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

noncomputable def NavierStokes.HarmonicWaveInteraction.interactionBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (a b : CorrectionState.HarmonicBlock D) : CorrectionState.HarmonicBlock D

Interaction block, bundling velocity, pressure, frequency, phase and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.HarmonicWaveInteraction.linearGoodBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (a b : CorrectionState.HarmonicBlock D) (g : HarmonicResidual.BlockCoefficients D) : CorrectionState.HarmonicBlock D

Linear good block, bundling velocity, pressure, frequency, phase and the required compatibility proofs.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.nonconstant_add {D : Type} (a b : HarmonicFields.Coefficients D) : HarmonicResidual.nonconstant (a + b) = HarmonicResidual.nonconstant a + HarmonicResidual.nonconstant b

theorem NavierStokes.HarmonicWaveInteraction.nonconstant_real_sub_axisymmetric {D : Type} (a b : HarmonicFields.Coefficients D) (hb : HarmonicFields.BandLimited b 0) : HarmonicResidual.nonconstant (HarmonicResidual.realCoefficients (a - b)) = HarmonicResidual.nonconstant (HarmonicResidual.realCoefficients a)

The zero-mode alias remains in the complete residual but vanishes under the actual nonconstant projection.

theorem NavierStokes.HarmonicWaveInteraction.waveChange_projection_split {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (a b : CorrectionState.HarmonicBlock D) (g A₀ A₁ : HarmonicResidual.BlockCoefficients D) (hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A₁ n i - A₀ n i) 0) (n : ℕ) (i : Fin 3) : HarmonicResidual.nonconstant (HarmonicResidual.realCoefficients (waveChangeCoefficients c u a b g A₀ A₁ n i)) = (linearGoodBlock c a b g).velocity n i + (interactionBlock c u a b).velocity n i

theorem NavierStokes.HarmonicWaveInteraction.residualBlock_wave_update_split {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (c : CorrectionState.Context D) (u₀ u₁ : CorrectionState.State D) (he : u₁.mean = u₀.mean) (a b : CorrectionState.HarmonicBlock D) (G g A₀ A₁ : HarmonicResidual.BlockCoefficients D) (hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A₁ n i - A₀ n i) 0) (n : ℕ) (hr : ContDiffOn ℝ (↑⊤) (HarmonicResidual.contextFrame c n).radial U) (hz : ContDiffOn ℝ (↑⊤) (HarmonicResidual.contextFrame c n).axial U) (hΦ : ContDiffOn ℝ (↑⊤) (a.phase n) U) (hkp : a.angularFrequency n ≠ 0) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => HarmonicResidual.contextBase c n y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => HarmonicResidual.stateMean u₀ n y i) U) (ha : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (a.velocity n i)) (hb : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (b.velocity n i)) (hp : HarmonicResidual.SmoothCoefficients U (a.pressure n)) (hq : HarmonicResidual.SmoothCoefficients U (b.pressure n)) {x : D} (hx : x ∈ U) (j : ℤ) (i : Fin 3) : ((HarmonicResidual.residualBlock c u₁ (addBlock a b) (G + g) A₁).velocity n i).coeff j x - ((HarmonicResidual.residualBlock c u₀ a G A₀).velocity n i).coeff j x = ((linearGoodBlock c a b g).velocity n i).coeff j x + ((interactionBlock c u₀ a b).velocity n i).coeff j x

theorem NavierStokes.HarmonicWaveInteraction.interactionBlock_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β H : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hκ : κ ≤ 1 / 2) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {u : CorrectionState.State D} (hm : MeanIncrementBounds.IncrementBounds s H u.mean) {a b : CorrectionState.HarmonicBlock D} {M N : ℕ} (ha : CorrectionState.HarmonicBlock.WaveBounds s P α a) (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (ha0 : ZeroMode a) (hb0 : ZeroMode b) (hM : a.BandLimited M) (hN : b.BandLimited N) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hda : ModeSolenoidal s c a) (hdb : ModeSolenoidal s c (withCarrier a b)) (hNormal : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (HarmonicMeanInteraction.slowNormal c ho hR a.phase n x).ofLp i) (hFreq : WeightedClasses.BandBound s (-(1 / 2)) a.frequency) (hAng : WeightedClasses.BandBound s (-(1 / 2)) fun (n : ℕ) => ↑(a.angularFrequency n)) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : CorrectionState.HarmonicBlock.WaveBounds s P (min (β + H - 1 / 2) (min (α + β - κ) (β + β - κ))) (interactionBlock c u a b)

Mean-wave and wave-wave terms retain their separate gains until the final minimum. No class hypothesis is imposed on their output.

Extracting the actual divergence condition

noncomputable def NavierStokes.HarmonicWaveInteraction.divergenceCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (a : HarmonicResidual.VectorCoefficients D) : HarmonicFields.Coefficients D

Divergence coefficients, constructed using differentiate.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.field_divergenceCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : HarmonicResidual.Frame D) (k : ℝ) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (kp : ℤ) (a : HarmonicResidual.VectorCoefficients D) (ha : ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (a i)) {p : D × ℝ} (hp : p ∈ HarmonicResidual.liftDomain U) : HarmonicFields.field (divergenceCoefficients g k Φ kp a) k Φ kp p = HarmonicCalculus.cylindricalDivergence (fun (y : D × ℝ) => g.radius y.1) (HarmonicResidual.liftDirection g.radial) HarmonicResidual.angularDirection (HarmonicResidual.liftDirection g.axial) (HarmonicResidual.vectorField a k Φ kp) p

theorem NavierStokes.HarmonicWaveInteraction.divergenceCoefficients_single {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (a : HarmonicResidual.VectorCoefficients D) (j : ℤ) : (divergenceCoefficients g k Φ kp fun (i : Fin 3) => AddMonoidAlgebra.single j ((a i).coeff j)) = AddMonoidAlgebra.single j ((divergenceCoefficients g k Φ kp a).coeff j)

theorem NavierStokes.HarmonicWaveInteraction.smoothCoefficients_single {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : D → ℂ} (hf : ContDiffOn ℝ (↑⊤) f U) (j : ℤ) : HarmonicResidual.SmoothCoefficients U (AddMonoidAlgebra.single j f)

theorem NavierStokes.HarmonicWaveInteraction.modeSolenoidal_of_full {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (c : CorrectionState.Context D) (b : CorrectionState.HarmonicBlock D) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (b.phase n) s.domain) (hkp : ∀ (n : ℕ), b.angularFrequency n ≠ 0) (hb : ∀ (n : ℕ) (i : Fin 3), HarmonicResidual.SmoothCoefficients s.domain (b.velocity n i)) (hdiv : ∀ (n : ℕ) (p : D × ℝ), p.1 ∈ s.domain → HarmonicCalculus.cylindricalDivergence (fun (q : D × ℝ) => c.operators.radius q.1) (HarmonicResidual.liftDirection (HarmonicResidual.contextFrame c n).radial) HarmonicResidual.angularDirection (HarmonicResidual.liftDirection (HarmonicResidual.contextFrame c n).axial) (fun (q : D × ℝ) (i : Fin 3) => ↑(b.oscillation n q i)) p = 0) : ModeSolenoidal s c b

theorem NavierStokes.HarmonicWaveInteraction.waveBounds_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} {b : CorrectionState.HarmonicBlock D} (hb : CorrectionState.HarmonicBlock.WaveBounds s P α b) (h0 : ZeroMode b) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients s.domain (b.velocity n i)

Finite harmonic values, realness, and actual label reconstruction

theorem NavierStokes.HarmonicWaveInteraction.nonlinearCoefficients_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) {a b : CorrectionState.HarmonicBlock D} {M N : ℕ} (ha : a.BandLimited M) (hb : b.BandLimited N) (n : ℕ) (i : Fin 3) : HarmonicFields.BandLimited (nonlinearCoefficients c a b n i) (max (M + N) (N + N))

theorem NavierStokes.HarmonicWaveInteraction.crossCoefficients_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (m : D → HarmonicCalculus.ComplexVector) {a : HarmonicResidual.VectorCoefficients D} {N : ℕ} (ha : ∀ (i : Fin 3), HarmonicFields.BandLimited (a i) N) (i : Fin 3) : HarmonicFields.BandLimited (HarmonicMeanInteraction.crossCoefficients g k Φ kp m a i) N

theorem NavierStokes.HarmonicWaveInteraction.interactionBlock_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) {a b : CorrectionState.HarmonicBlock D} {M N : ℕ} (ha : a.BandLimited M) (hb : b.BandLimited N) : (interactionBlock c u a b).BandLimited (max (M + N) (N + N))

theorem NavierStokes.HarmonicWaveInteraction.interactionBlock_conjugate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (a b : CorrectionState.HarmonicBlock D) (n : ℕ) (i : Fin 3) : HarmonicFields.ConjugateSymmetric ((interactionBlock c u a b).velocity n i)

theorem NavierStokes.HarmonicWaveInteraction.interactionBlock_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (a b : CorrectionState.HarmonicBlock D) : ZeroMode (interactionBlock c u a b)

theorem NavierStokes.HarmonicWaveInteraction.linearGoodBlock_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (a : CorrectionState.HarmonicBlock D) {b : CorrectionState.HarmonicBlock D} {g : HarmonicResidual.BlockCoefficients D} {N E : ℕ} (hb : b.BandLimited N) (hg : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (g n i) E) : (linearGoodBlock c a b g).BandLimited (max N E)

theorem NavierStokes.HarmonicWaveInteraction.linearGoodBlock_conjugate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (a b : CorrectionState.HarmonicBlock D) (g : HarmonicResidual.BlockCoefficients D) (n : ℕ) (i : Fin 3) : HarmonicFields.ConjugateSymmetric ((linearGoodBlock c a b g).velocity n i)

theorem NavierStokes.HarmonicWaveInteraction.linearGoodBlock_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (a b : CorrectionState.HarmonicBlock D) (g : HarmonicResidual.BlockCoefficients D) : ZeroMode (linearGoodBlock c a b g)

noncomputable def NavierStokes.HarmonicWaveInteraction.waveResidualDifferenceBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u₀ u₁ : CorrectionState.State D) (a b : CorrectionState.HarmonicBlock D) (G g A₀ A₁ : HarmonicResidual.BlockCoefficients D) : CorrectionState.HarmonicBlock D

Wave residual difference block, bundling velocity, pressure, frequency, phase and the required compatibility proofs.

Equations

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

theorem NavierStokes.HarmonicWaveInteraction.waveResidualDifferenceBlock_field {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u₀ u₁ : CorrectionState.State D) (a b : CorrectionState.HarmonicBlock D) (G g A₀ A₁ : HarmonicResidual.BlockCoefficients D) (n : ℕ) (x : D × ℝ) (i : Fin 3) : (waveResidualDifferenceBlock c u₀ u₁ a b G g A₀ A₁).oscillation n x i = (HarmonicResidual.residualBlock c u₁ (addBlock a b) (G + g) A₁).oscillation n x i - (HarmonicResidual.residualBlock c u₀ a G A₀).oscillation n x i

theorem NavierStokes.HarmonicWaveInteraction.grouped_wave_change {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_3} {U : Set D} (hU : IsOpen U) {c : CorrectionState.Context D} {u₀ u₁ : CorrectionState.State D} {labels : ℕ → Finset ι} {a b : ι → CorrectionState.HarmonicBlock D} {G g A₀ A₁ : ι → HarmonicResidual.BlockCoefficients D} (hrep₀ : HarmonicResidual.BlockRepresentation labels a G A₀ u₀) (hrep₁ : HarmonicResidual.BlockRepresentation labels (fun (l : ι) => addBlock (a l) (b l)) (fun (l : ι) => G l + g l) A₁ u₁) {n : ℕ} (h₀ : HarmonicResidual.ExtractionRegular U c u₀ labels a G A₀ n) (h₁ : HarmonicResidual.ExtractionRegular U c u₁ labels (fun (l : ι) => addBlock (a l) (b l)) (fun (l : ι) => G l + g l) A₁ n) {x : D × ℝ} (hx : x ∈ HarmonicResidual.liftDomain U) (i : Fin 3) : HarmonicResidual.stateGoodWaveResidual c u₁ n x i - HarmonicResidual.stateGoodWaveResidual c u₀ n x i = ∑ l ∈ labels n, (waveResidualDifferenceBlock c u₀ u₁ (a l) (b l) (G l) (g l) (A₀ l) (A₁ l)).oscillation n x i

The grouped difference is the change in the actual good nonconstant PDE residual. Cross-label products vanish by the disjoint supports contained in ExtractionRegular; finite sums alone are not used as uniform estimates.