Uniform coefficient bounds for the literal harmonic blocks

Restriction to angle zero, isometric coordinate changes, conjugate pairs, and finite signed harmonic sums preserve constants chosen before labels. The endpoints use the actual signed and particular block constructors.

theorem NavierStokes.UniformBlockBounds.uniform_reindex {D E : Type} {F : Type u_1} {ι : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] D) {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {f : ι → ℕ → D → F} (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass (ParticularWaveBounds.reindexStrip e s) (fun (l : ι) (n : ℕ) (x : E) => w l n (e x)) α fun (l : ι) (n : ℕ) (x : E) => f l n (e x)

An isometry preserves the constants and polynomial degrees of every actual finite-jet bound, uniformly over the extra index.

theorem NavierStokes.UniformBlockBounds.uniform_zeroSection {D : Type} {F : Type u_1} {ι : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData (D × ℝ)} {w : ι → ℕ → D × ℝ → ℝ} {α : ℝ} {f : ι → ℕ → D × ℝ → F} (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass (SignedWaveUpdate.sectionStrip s) (fun (l : ι) (n : ℕ) (x : D) => w l n (x, 0)) α fun (l : ι) (n : ℕ) (x : D) => f l n (x, 0)

Restriction to angle zero does not enlarge a single jet constant.

theorem NavierStokes.UniformBlockBounds.sectionStrip_productStrip {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) : SignedWaveUpdate.sectionStrip (HarmonicWaveInteraction.productStrip s) = s

theorem NavierStokes.UniformBlockBounds.uniform_slice {D : Type} {F : Type u_1} {ι : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {f : ι → ℕ → D × ℝ → F} (hf : LabelSumBounds.UniformClass (HarmonicWaveInteraction.productStrip s) (fun (l : ι) (n : ℕ) (x : D × ℝ) => w l n x.1) α f) : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => f l n (x, 0)

theorem NavierStokes.UniformBlockBounds.pair_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {a : ι → ℕ → D → ℂ} (ha : LabelSumBounds.UniformClass s w α a) (j m : ℤ) : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => (ErrorHarmonics.conjugatePair j (a l n)).coeff m x

A conjugate pair retains uniformity, including both negative and positive Fourier modes.

theorem NavierStokes.UniformBlockBounds.pair_sub_apply {D : Type} (j m : ℤ) (a b : D → ℂ) (x : D) : (ErrorHarmonics.conjugatePair j fun (y : D) => a y - b y).coeff m x = (ErrorHarmonics.conjugatePair j a).coeff m x - (ErrorHarmonics.conjugatePair j b).coeff m x

theorem NavierStokes.UniformBlockBounds.coefficientBlock_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α γ : ℝ} (k : ι → ℕ → ℝ) (Φ : ι → ℕ → D → ℝ) (kp : ι → ℕ → ℤ) {v : ι → ℕ → D → HarmonicCalculus.ComplexVector} {p : ι → ℕ → D → ℂ} (hv : LabelSumBounds.UniformClass s w α v) (hp : LabelSumBounds.UniformClass s w γ p) : (∀ (i : Fin 3) (m : ℤ), LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => ((SignedWaveUpdate.coefficientBlock (k l) (Φ l) (kp l) (v l) (p l)).velocity n i).coeff m x) ∧ ∀ (m : ℤ), LabelSumBounds.UniformClass s w γ fun (l : ι) (n : ℕ) (x : D) => ((SignedWaveUpdate.coefficientBlock (k l) (Φ l) (kp l) (v l) (p l)).pressure n).coeff m x

theorem NavierStokes.UniformBlockBounds.blockOfCoefficients_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData (D × ℝ)} {w : ι → ℕ → D × ℝ → ℝ} {α γ : ℝ} (a : ι → LinearWaveBounds.WaveCoefficients (D × ℝ)) (kp : ι → ℕ → ℤ) (ha : LabelSumBounds.UniformClass s w α fun (l : ι) => (a l).amplitude) (hp : LabelSumBounds.UniformClass s w γ fun (l : ι) => (a l).pressure) : (∀ (i : Fin 3) (m : ℤ), LabelSumBounds.UniformClass (SignedWaveUpdate.sectionStrip s) (fun (l : ι) (n : ℕ) (x : D) => w l n (x, 0)) α fun (l : ι) (n : ℕ) (x : D) => ((SignedWaveUpdate.blockOfCoefficients (a l) (kp l)).velocity n i).coeff m x) ∧ ∀ (m : ℤ), LabelSumBounds.UniformClass (SignedWaveUpdate.sectionStrip s) (fun (l : ι) (n : ℕ) (x : D) => w l n (x, 0)) γ fun (l : ι) (n : ℕ) (x : D) => ((SignedWaveUpdate.blockOfCoefficients (a l) (kp l)).pressure n).coeff m x

Uniform full-angle amplitude and pressure bounds give the actual stored coefficients of the angle-zero signed block.

theorem NavierStokes.UniformBlockBounds.blockOfCoefficients_difference_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData (D × ℝ)} {w : ι → ℕ → D × ℝ → ℝ} {α : ℝ} (a b : ι → LinearWaveBounds.WaveCoefficients (D × ℝ)) (kp : ι → ℕ → ℤ) (hab : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D × ℝ) => (a l).amplitude n x - (b l).amplitude n x) (i : Fin 3) (m : ℤ) : LabelSumBounds.UniformClass (SignedWaveUpdate.sectionStrip s) (fun (l : ι) (n : ℕ) (x : D) => w l n (x, 0)) α fun (l : ι) (n : ℕ) (x : D) => ((SignedWaveUpdate.blockOfCoefficients (a l) (kp l)).velocity n i).coeff m x - ((SignedWaveUpdate.blockOfCoefficients (b l) (kp l)).velocity n i).coeff m x

The smallness of a full-angle amplitude difference transfers to the literal difference of the two stored velocity coefficients.

theorem NavierStokes.UniformBlockBounds.commonCorrected_difference_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData (D × ℝ)} {w : ι → ℕ → D × ℝ → ℝ} {α : ℝ} {I : Type} (a : ι → PeriodizedWaveBounds.CopyData (D × ℝ) I) (d : ι → LinearWaveBounds.GraphDirections (D × ℝ)) (kp : ι → ℕ → ℤ) (hc : LabelSumBounds.UniformClass s w α fun (l : ι) => (a l).common.curlCorrection s (d l)) (i : Fin 3) (m : ℤ) : LabelSumBounds.UniformClass (SignedWaveUpdate.sectionStrip s) (fun (l : ι) (n : ℕ) (x : D) => w l n (x, 0)) α fun (l : ι) (n : ℕ) (x : D) => ((SignedWaveUpdate.blockOfCoefficients ((a l).commonCorrected s (d l)) (kp l)).velocity n i).coeff m x - ((SignedWaveUpdate.blockOfCoefficients (a l).common (kp l)).velocity n i).coeff m x

For the actual common corrected wave, the amplitude difference is exactly the common curl correction.

theorem NavierStokes.UniformBlockBounds.blockOfCoefficients_product_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α γ : ℝ} (a : ι → LinearWaveBounds.WaveCoefficients (D × ℝ)) (kp : ι → ℕ → ℤ) (ha : LabelSumBounds.UniformWaveClass (HarmonicWaveInteraction.productStrip s) (fun (l : ι) (n : ℕ) (x : D × ℝ) => P l n x.1) α fun (l : ι) => (a l).amplitude) (hp : LabelSumBounds.UniformWaveClass (HarmonicWaveInteraction.productStrip s) (fun (l : ι) (n : ℕ) (x : D × ℝ) => P l n x.1) γ fun (l : ι) => (a l).pressure) : (∀ (i : Fin 3) (m : ℤ), LabelSumBounds.UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((SignedWaveUpdate.blockOfCoefficients (a l) (kp l)).velocity n i).coeff m x) ∧ ∀ (m : ℤ), LabelSumBounds.UniformWaveClass s P γ fun (l : ι) (n : ℕ) (x : D) => ((SignedWaveUpdate.blockOfCoefficients (a l) (kp l)).pressure n).coeff m x

theorem NavierStokes.UniformBlockBounds.commonCorrected_product_difference_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α : ℝ} {I : Type} (a : ι → PeriodizedWaveBounds.CopyData (D × ℝ) I) (d : ι → LinearWaveBounds.GraphDirections (D × ℝ)) (kp : ι → ℕ → ℤ) (hc : LabelSumBounds.UniformWaveClass (HarmonicWaveInteraction.productStrip s) (fun (l : ι) (n : ℕ) (x : D × ℝ) => P l n x.1) α fun (l : ι) => (a l).common.curlCorrection (HarmonicWaveInteraction.productStrip s) (d l)) (i : Fin 3) (m : ℤ) : LabelSumBounds.UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((SignedWaveUpdate.blockOfCoefficients ((a l).commonCorrected (HarmonicWaveInteraction.productStrip s) (d l)) (kp l)).velocity n i).coeff m x - ((SignedWaveUpdate.blockOfCoefficients (a l).common (kp l)).velocity n i).coeff m x

theorem NavierStokes.UniformBlockBounds.assembledBlock_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α γ : ℝ} (N : ℕ) (k : ι → ℕ → ℝ) (Φ : ι → ℕ → D → ℝ) (kp : ι → ℕ → ℤ) {v : ι → ℤ → ℕ → D → HarmonicCalculus.ComplexVector} {p : ι → ℤ → ℕ → D → ℂ} (hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w l n x) (hv : ∀ j ∈ ParticularWaveAssembly.modes N, LabelSumBounds.UniformClass s w α fun (l : ι) => v l j) (hp : ∀ j ∈ ParticularWaveAssembly.modes N, LabelSumBounds.UniformClass s w γ fun (l : ι) => p l j) : (∀ (i : Fin 3) (m : ℤ), LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => ((ParticularWaveAssembly.assembledBlock N (k l) (Φ l) (kp l) (v l) (p l)).velocity n i).coeff m x) ∧ ∀ (m : ℤ), LabelSumBounds.UniformClass s w γ fun (l : ι) (n : ℕ) (x : D) => ((ParticularWaveAssembly.assembledBlock N (k l) (Φ l) (kp l) (v l) (p l)).pressure n).coeff m x

A fixed finite signed harmonic sum preserves uniformity in the spatial label, independently of the total number of such labels.

theorem NavierStokes.UniformBlockBounds.nativeSlice_uniform {Q : Type} {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData ((Q × ℝ) × TorusInverse.Plane)} {w : ι → ℕ → (Q × ℝ) × TorusInverse.Plane → ℝ} {α : ℝ} {f : ι → ℕ → (Q × ℝ) × TorusInverse.Plane → F} (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass (ParticularWaveAssembly.sectionStrip s) (fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => w l n (ParticularWaveAssembly.angleShuffle (x, 0))) α fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => f l n (ParticularWaveAssembly.angleShuffle (x, 0))

The actual angle shuffle followed by the actual zero section.

noncomputable def NavierStokes.UniformBlockBounds.nativeStrip {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (s : WeightedClasses.StripData (Q × TorusInverse.Plane)) : WeightedClasses.StripData ((Q × ℝ) × TorusInverse.Plane)

The native whole-angle strip used by the literal particular solver.

Equations

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

theorem NavierStokes.UniformBlockBounds.sectionStrip_nativeStrip {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (s : WeightedClasses.StripData (Q × TorusInverse.Plane)) : ParticularWaveAssembly.sectionStrip (nativeStrip s) = s

theorem NavierStokes.UniformBlockBounds.nativeSlice_original_uniform {Q : Type} {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData (Q × TorusInverse.Plane)} {w : ι → ℕ → (Q × ℝ) × TorusInverse.Plane → ℝ} {α : ℝ} {f : ι → ℕ → (Q × ℝ) × TorusInverse.Plane → F} (hf : LabelSumBounds.UniformClass (nativeStrip s) w α f) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => w l n (ParticularWaveAssembly.angleShuffle (x, 0))) α fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => f l n (ParticularWaveAssembly.angleShuffle (x, 0))

theorem NavierStokes.UniformBlockBounds.native_assembledBlock_uniform {Q : Type} {ι : Type u_1} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {s : WeightedClasses.StripData ((Q × ℝ) × TorusInverse.Plane)} {w : ι → ℕ → (Q × ℝ) × TorusInverse.Plane → ℝ} {α γ : ℝ} (N : ℕ) (k : ι → ℕ → ℝ) (Φ : ι → ℕ → Q × TorusInverse.Plane → ℝ) (kp : ι → ℕ → ℤ) {v : ι → ℤ → ℕ → (Q × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector} {p : ι → ℤ → ℕ → (Q × ℝ) × TorusInverse.Plane → ℂ} (hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w l n x) (hv : ∀ j ∈ ParticularWaveAssembly.modes N, LabelSumBounds.UniformClass s w α fun (l : ι) => v l j) (hp : ∀ j ∈ ParticularWaveAssembly.modes N, LabelSumBounds.UniformClass s w γ fun (l : ι) => p l j) : (∀ (i : Fin 3) (m : ℤ), LabelSumBounds.UniformClass (ParticularWaveAssembly.sectionStrip s) (fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => w l n (ParticularWaveAssembly.angleShuffle (x, 0))) α fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => ((ParticularWaveAssembly.assembledBlock N (k l) (Φ l) (kp l) (fun (j : ℤ) (n : ℕ) (x : Q × TorusInverse.Plane) => v l j n (ParticularWaveAssembly.angleShuffle (x, 0))) fun (j : ℤ) (n : ℕ) (x : Q × TorusInverse.Plane) => p l j n (ParticularWaveAssembly.angleShuffle (x, 0))).velocity n i).coeff m x) ∧ ∀ (m : ℤ), LabelSumBounds.UniformClass (ParticularWaveAssembly.sectionStrip s) (fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => w l n (ParticularWaveAssembly.angleShuffle (x, 0))) γ fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => ((ParticularWaveAssembly.assembledBlock N (k l) (Φ l) (kp l) (fun (j : ℤ) (n : ℕ) (x : Q × TorusInverse.Plane) => v l j n (ParticularWaveAssembly.angleShuffle (x, 0))) fun (j : ℤ) (n : ℕ) (x : Q × TorusInverse.Plane) => p l j n (ParticularWaveAssembly.angleShuffle (x, 0))).pressure n).coeff m x

Full-angle, already periodized mode coefficients produce the actual finite particular block. Every output mode has uniform label bounds.

theorem NavierStokes.UniformBlockBounds.native_assembledBlock_original_uniform {Q : Type} {ι : Type u_1} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {s : WeightedClasses.StripData (Q × TorusInverse.Plane)} {w : ι → ℕ → (Q × ℝ) × TorusInverse.Plane → ℝ} {α γ : ℝ} (N : ℕ) (k : ι → ℕ → ℝ) (Φ : ι → ℕ → Q × TorusInverse.Plane → ℝ) (kp : ι → ℕ → ℤ) {v : ι → ℤ → ℕ → (Q × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector} {p : ι → ℤ → ℕ → (Q × ℝ) × TorusInverse.Plane → ℂ} (hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ (nativeStrip s).domain, 0 ≤ w l n x) (hv : ∀ j ∈ ParticularWaveAssembly.modes N, LabelSumBounds.UniformClass (nativeStrip s) w α fun (l : ι) => v l j) (hp : ∀ j ∈ ParticularWaveAssembly.modes N, LabelSumBounds.UniformClass (nativeStrip s) w γ fun (l : ι) => p l j) : (∀ (i : Fin 3) (m : ℤ), LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => w l n (ParticularWaveAssembly.angleShuffle (x, 0))) α fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => ((ParticularWaveAssembly.assembledBlock N (k l) (Φ l) (kp l) (fun (j : ℤ) (n : ℕ) (x : Q × TorusInverse.Plane) => v l j n (ParticularWaveAssembly.angleShuffle (x, 0))) fun (j : ℤ) (n : ℕ) (x : Q × TorusInverse.Plane) => p l j n (ParticularWaveAssembly.angleShuffle (x, 0))).velocity n i).coeff m x) ∧ ∀ (m : ℤ), LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => w l n (ParticularWaveAssembly.angleShuffle (x, 0))) γ fun (l : ι) (n : ℕ) (x : Q × TorusInverse.Plane) => ((ParticularWaveAssembly.assembledBlock N (k l) (Φ l) (kp l) (fun (j : ℤ) (n : ℕ) (x : Q × TorusInverse.Plane) => v l j n (ParticularWaveAssembly.angleShuffle (x, 0))) fun (j : ℤ) (n : ℕ) (x : Q × TorusInverse.Plane) => p l j n (ParticularWaveAssembly.angleShuffle (x, 0))).pressure n).coeff m x

theorem NavierStokes.UniformBlockBounds.block_velocity_reindex {D E : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) {s : WeightedClasses.StripData E} {w : ι → ℕ → E → ℝ} {α : ℝ} {a : ι → CorrectionState.HarmonicBlock E} (i : Fin 3) (j : ℤ) (ha : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : E) => ((a l).velocity n i).coeff j x) : LabelSumBounds.UniformClass (StateReindex.strip e s) (fun (l : ι) (n : ℕ) (x : D) => w l n (e x)) α fun (l : ι) (n : ℕ) (x : D) => ((StateReindex.block e (a l)).velocity n i).coeff j x

The last coordinate reassociation acts on the actual stored velocity coefficients and preserves the uniform class.

theorem NavierStokes.UniformBlockBounds.block_pressure_reindex {D E : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) {s : WeightedClasses.StripData E} {w : ι → ℕ → E → ℝ} {α : ℝ} {a : ι → CorrectionState.HarmonicBlock E} (j : ℤ) (ha : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : E) => ((a l).pressure n).coeff j x) : LabelSumBounds.UniformClass (StateReindex.strip e s) (fun (l : ι) (n : ℕ) (x : D) => w l n (e x)) α fun (l : ι) (n : ℕ) (x : D) => ((StateReindex.block e (a l)).pressure n).coeff j x