Uniform native-cell bounds for actual signed coefficients

The constants in every LocalJets conclusion precede both band and copy. The input functions need smoothness and jets only on their own native cells. The matrix inverse, signed square-root quotient and projected pressure are computed from the primitive input functions.

theorem NavierStokes.SignedCopyBounds.comp_jet_bound_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : D → ℝ} {g : ℝ → ℝ} {x : D} (hf : ContDiffAt ℝ (↑⊤) f x) (hg : ContDiffAt ℝ (↑⊤) g (f x)) (n : ℕ) {C B : ℝ} (hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C) (hB : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ B ^ i) : ‖iteratedFDeriv ℝ n (g ∘ f) x‖ ≤ ↑n.factorial * C * B ^ n

The quantitative chain rule needs only the actual finite jet at the point. No common smooth extension of the native copies is required.

theorem NavierStokes.SignedCopyBounds.local_congr {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → I → D → E} (hf : PeriodizedWaveBounds.LocalJets s w α K f) (he : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → f n i =ᶠ[nhds x] g n i) : PeriodizedWaveBounds.LocalJets s w α K g

theorem NavierStokes.SignedCopyBounds.local_of_eq {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → I → D → E} (hf : PeriodizedWaveBounds.LocalJets s w α K f) (he : ∀ (n : ℕ) (i : I) (x : D), f n i x = g n i x) : PeriodizedWaveBounds.LocalJets s w α K g

theorem NavierStokes.SignedCopyBounds.local_neg {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → I → D → E} (hf : PeriodizedWaveBounds.LocalJets s w α K f) : PeriodizedWaveBounds.LocalJets s w α K fun (n : ℕ) (i : I) (x : D) => -f n i x

theorem NavierStokes.SignedCopyBounds.local_sub {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → I → D → E} (hf : PeriodizedWaveBounds.LocalJets s w α K f) (hg : PeriodizedWaveBounds.LocalJets s w α K g) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) : PeriodizedWaveBounds.LocalJets s w α K fun (n : ℕ) (i : I) (x : D) => f n i x - g n i x

theorem NavierStokes.SignedCopyBounds.local_mul {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w v : ℕ → D → ℝ} {α β : ℝ} {f g : ℕ → I → D → ℝ} (hf : PeriodizedWaveBounds.LocalJets s w α K f) (hg : PeriodizedWaveBounds.LocalJets s v β K g) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hv : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ v n x) : PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => w n x * v n x) (α + β) K fun (n : ℕ) (i : I) (x : D) => f n i x * g n i x

theorem NavierStokes.SignedCopyBounds.local_coeff_mul {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → I → D → ℝ} (hf : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K f) (hg : PeriodizedWaveBounds.LocalJets s w α K g) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) : PeriodizedWaveBounds.LocalJets s w α K fun (n : ℕ) (i : I) (x : D) => f n i x * g n i x

theorem NavierStokes.SignedCopyBounds.local_band_smul {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α β : ℝ} {r : ℕ → ℝ} {f : ℕ → I → D → E} (hf : PeriodizedWaveBounds.LocalJets s w α K f) (hr : WeightedClasses.BandBound s β r) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) : PeriodizedWaveBounds.LocalJets s w (α + β) K fun (n : ℕ) (i : I) (x : D) => r n • f n i x

theorem NavierStokes.SignedCopyBounds.local_indexed_band_smul {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α β : ℝ} {r : I → ℕ → ℝ} {f : ℕ → I → D → E} (hf : PeriodizedWaveBounds.LocalJets s w α K f) (hr : UniformPrimaryWeights.UniformBandBound s β r) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) : PeriodizedWaveBounds.LocalJets s w (α + β) K fun (n : ℕ) (i : I) (x : D) => r i n • f n i x

A band coefficient may itself depend on the copy. Its bound is still chosen before that index, so this also permits a joint label/copy index.

theorem NavierStokes.SignedCopyBounds.local_compact_comp {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {f : ℕ → I → D → ℝ} (hf : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K f) {g : ℝ → ℝ} {U C : Set ℝ} (hU : IsOpen U) (hg : ContDiffOn ℝ (↑⊤) g U) (hC : IsCompact C) (hCU : C ⊆ U) (hmap : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → f n i x ∈ C) : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) (x : D) => g (f n i x)

Compactness controls only the fixed outer scalar function. The native input jets have one bound before every band and copy index.

theorem NavierStokes.SignedCopyBounds.local_inv {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {f : ℕ → I → D → ℝ} (hf : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K f) {b M : ℝ} (hb : 0 < b) (hl : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ |f n i x|) (hu : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → |f n i x| ≤ M) : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) (x : D) => (f n i x)⁻¹

The actual square-root quotient at a native point

theorem NavierStokes.SignedCopyBounds.rpow_comp_jets_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : D → ℝ} {x : D} (hf : ContDiffAt ℝ (↑⊤) f x) (hpos : 0 < f x) (p : ℝ) (m : ℕ) {B : ℝ} (hB : 1 ≤ B) (hpow : f x ^ p ≤ B) (hinv : (f x)⁻¹ ≤ B) (hjet : ∀ i ≤ m, ‖iteratedFDeriv ℝ i f x‖ ≤ B) {j : ℕ} (hj : j ≤ m) : ‖iteratedFDeriv ℝ j (fun (y : D) => f y ^ p) x‖ ≤ WeightedQuotients.orderBound p m * B ^ (2 * m + 1)

theorem NavierStokes.SignedCopyBounds.normalized_jet_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : D → ℝ} {x : D} (hf : ContDiffAt ℝ (↑⊤) f x) {w B : ℝ} (hw : 0 < w) (j : ℕ) (hjet : ‖iteratedFDeriv ℝ j f x‖ ≤ w * B) : ‖iteratedFDeriv ℝ j (WeightedQuotients.normalizeAt w f) x‖ ≤ B

theorem NavierStokes.SignedCopyBounds.mul_jets_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f g : D → ℝ} {x : D} (hf : ContDiffAt ℝ (↑⊤) f x) (hg : ContDiffAt ℝ (↑⊤) g x) (n : ℕ) {A B : ℝ} (hA : 0 ≤ A) (_hB : 0 ≤ B) (hfj : ∀ i ≤ n, ‖iteratedFDeriv ℝ i f x‖ ≤ A) (hgj : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g x‖ ≤ B) : ‖iteratedFDeriv ℝ n (fun (y : D) => f y * g y) x‖ ≤ WeightedQuotients.chooseSum n * A * B

theorem NavierStokes.SignedCopyBounds.signed_jet_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {g r : D → ℝ} {x : D} (hg : ContDiffAt ℝ (↑⊤) g x) (hr : ContDiffAt ℝ (↑⊤) r x) (hpos : 0 < g x) {w B : ℝ} (hw : 0 < w) (hB : 1 ≤ B) (m : ℕ) (hlo : w / B ≤ g x) (hgj : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g x‖ ≤ w * B) (hrj : ∀ i ≤ m, ‖iteratedFDeriv ℝ i r x‖ ≤ w * B) : ‖iteratedFDeriv ℝ m (fun (y : D) => r y / (2 * √(g y))) x‖ ≤ √w * SignedCovariance.signedJetCost m * B ^ (2 * m + 2)

theorem NavierStokes.SignedCopyBounds.local_input_envelope {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {g r : ℕ → I → D → ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < w n x) (hg : PeriodizedWaveBounds.LocalJets s w 0 K g) (hr : PeriodizedWaveBounds.LocalJets s w 0 K r) {c : ℝ} (hc : 0 < c) (hl : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → c * w n x ≤ g n i x) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → 1 ≤ C * s.growth n x ^ p ∧ w n x / (C * s.growth n x ^ p) ≤ g n i x ∧ (∀ j ≤ m, ‖iteratedFDeriv ℝ j (g n i) x‖ ≤ w n x * (C * s.growth n x ^ p)) ∧ ∀ j ≤ m, ‖iteratedFDeriv ℝ j (r n i) x‖ ≤ w n x * (C * s.growth n x ^ p)

All finite input jet bounds and the positive weight margin are collected before choosing a band, a copy, or a spatial point.

theorem NavierStokes.SignedCopyBounds.local_signed_quotient_zero {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {g r : ℕ → I → D → ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < w n x) (hg : PeriodizedWaveBounds.LocalJets s w 0 K g) (hr : PeriodizedWaveBounds.LocalJets s w 0 K r) {c : ℝ} (hc : 0 < c) (hl : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → c * w n x ≤ g n i x) : PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(w n x)) 0 K fun (n : ℕ) (i : I) (x : D) => r n i x / (2 * √(g n i x))

theorem NavierStokes.SignedCopyBounds.local_signed_quotient {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {g r : ℕ → I → D → ℝ} {β : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < w n x) (hg : PeriodizedWaveBounds.LocalJets s w 0 K g) (hr : PeriodizedWaveBounds.LocalJets s w β K r) {c : ℝ} (hc : 0 < c) (hl : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → c * w n x ≤ g n i x) : PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(w n x)) β K fun (n : ℕ) (i : I) (x : D) => r n i x / (2 * √(g n i x))

Cramer's actual solve, uniformly on the native cells

@[reducible, inline]

abbrev NavierStokes.SignedCopyBounds.Mat2 : Type

Mat2: an abbreviation for SignedWaveUpdate.Mat2.

Equations

• NavierStokes.SignedCopyBounds.Mat2 = NavierStokes.SignedWaveUpdate.Mat2

@[reducible, inline]

abbrev NavierStokes.SignedCopyBounds.Vec2 : Type

Vec2: an abbreviation for SignedWaveUpdate.Vec2.

Equations

• NavierStokes.SignedCopyBounds.Vec2 = NavierStokes.SignedWaveUpdate.Vec2

@[reducible, inline]

abbrev NavierStokes.SignedCopyBounds.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.SignedCopyBounds.Space = NavierStokes.ProblemStatement.Space

structure NavierStokes.SignedCopyBounds.NativeCovariance {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (K : ℕ → I → Set D) (H : I → ℕ → D → Mat2) (T : I → ℕ → D → Vec2) : Type

Only primitive matrix/target jets and zeroth-order margins occur here. There is no inverse-jet or signed-output estimate in this record.

• matrix_jets (a b : Fin 2) : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) (x : D) => H i n x a b
• target_jets (a : Fin 2) : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => s.zeta x_1) 0 K fun (n : ℕ) (i : I) (x : D) => T i n x a
• zeta_pos (x : D) : x ∈ s.domain → 0 < s.zeta x
• determinantGap : ℝ

  Determinant gap of NativeCovariance, of type ℝ.

• entryBound : ℝ

  Entry bound of NativeCovariance, of type ℝ.

• primaryLower : ℝ

  Primary lower of NativeCovariance, of type ℝ.

• gap_pos : 0 < self.determinantGap
• entry_one : 1 ≤ self.entryBound
• lower_pos : 0 < self.primaryLower
• determinant (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K n i → self.determinantGap ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (√(s.slow n)) (H i n x))|
• entries (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K n i → ∀ (a b : Fin 2), |√(s.slow n) * H i n x a b| ≤ self.entryBound
• lower (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K n i → ∀ (j : Fin 2), self.primaryLower * s.zeta x ≤ SmoothCovariance.weights (H i n x) (T i n x) j

theorem NavierStokes.SignedCopyBounds.NativeCovariance.det_nonzero {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {H : I → ℕ → D → Mat2} {T : I → ℕ → D → Vec2} (h : NativeCovariance s K H T) (n : ℕ) (i : I) {x : D} (hx : x ∈ s.domain) (hi : x ∈ K n i) : Matrix.det (H i n x) ≠ 0

theorem NavierStokes.SignedCopyBounds.NativeCovariance.det_eventually {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {H : I → ℕ → D → Mat2} {T : I → ℕ → D → Vec2} (h : NativeCovariance s K H T) (n : ℕ) (i : I) {x : D} (hx : x ∈ s.domain) (hi : x ∈ K n i) : ∀ᶠ (y : D) in nhds x, Matrix.det (H i n y) ≠ 0

theorem NavierStokes.SignedCopyBounds.NativeCovariance.weights_jets {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {H : I → ℕ → D → Mat2} {T : I → ℕ → D → Vec2} (h : NativeCovariance s K H T) {R : I → ℕ → D → Vec2} {w : ℕ → D → ℝ} {β : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hR : ∀ (a : Fin 2), PeriodizedWaveBounds.LocalJets s w β K fun (n : ℕ) (i : I) (x : D) => R i n x a) (j : Fin 2) : PeriodizedWaveBounds.LocalJets s w β K fun (n : ℕ) (i : I) (x : D) => SmoothCovariance.weights (H i n x) (R i n x) j

theorem NavierStokes.SignedCopyBounds.NativeCovariance.increment_jets {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {H : I → ℕ → D → Mat2} {T : I → ℕ → D → Vec2} (h : NativeCovariance s K H T) {R : I → ℕ → D → Vec2} {β : ℝ} (hR : ∀ (a : Fin 2), PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => s.zeta x_1) β K fun (n : ℕ) (i : I) (x : D) => R i n x a) (j : Fin 2) : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => √(s.zeta x_1)) β K fun (n : ℕ) (i : I) (x : D) => SignedCovariance.increment (H i n x) (T i n x) (R i n x) j

The literal signed amplitude and homogeneous pressure

theorem NavierStokes.SignedCopyBounds.signedScalar_jets {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {H : I → ℕ → D → Mat2} {T R : I → ℕ → D → Vec2} {mask : I → ℕ → D → ℝ} {β : ℝ} (h : NativeCovariance s K H T) (hR : ∀ (a : Fin 2), PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => s.zeta x_1) β K fun (n : ℕ) (i : I) (x : D) => R i n x a) (hm : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => mask i n) (j : Fin 2) : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => √(s.zeta x_1)) (β + 1 / 2) K fun (n : ℕ) (i : I) => SignedWaveUpdate.signedScalar s (H i) (T i) (R i) (mask i) j n

theorem NavierStokes.SignedCopyBounds.signedVector_jets {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {H : I → ℕ → D → Mat2} {T R : I → ℕ → D → Vec2} {mask : I → ℕ → D → ℝ} {v : I → ℕ → D → Space} {W : ℕ → D → ℝ} {β : ℝ} (h : NativeCovariance s K H T) (hR : ∀ (a : Fin 2), PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => s.zeta x_1) β K fun (n : ℕ) (i : I) (x : D) => R i n x a) (hm : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => mask i n) (hv : PeriodizedWaveBounds.LocalJets s W 0 K fun (n : ℕ) (i : I) => v i n) (hW : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x) (j : Fin 2) : PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) (β + 1 / 2) K fun (n : ℕ) (i : I) => SignedWaveUpdate.signedVector s (H i) (T i) (R i) (mask i) (v i) j n

theorem NavierStokes.SignedCopyBounds.local_inner {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α : ℝ} {u v : ℕ → I → D → Space} (hu : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K u) (hv : PeriodizedWaveBounds.LocalJets s w α K v) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) : PeriodizedWaveBounds.LocalJets s w α K fun (n : ℕ) (i : I) (x : D) => inner ℝ (u n i x) (v n i x)

theorem NavierStokes.SignedCopyBounds.local_normalInverse {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {N : ℕ → I → D → Space} (hN : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K N) {b M : ℝ} (hb : 0 < b) (hl : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ ‖N n i x‖) (hu : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ‖N n i x‖ ≤ M) : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) (x : D) => (‖N n i x‖ ^ 2)⁻¹

theorem NavierStokes.SignedCopyBounds.local_pressureCoefficient {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α : ℝ} {N Ndot u : ℕ → I → D → Space} {A : ℕ → I → D → Space →L[ℝ] Space} (hN : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K N) (hNdot : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K Ndot) (hA : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K A) (ha : PeriodizedWaveBounds.LocalJets s w α K u) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) {b M : ℝ} (hb : 0 < b) (hl : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ ‖N n i x‖) (hu : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ‖N n i x‖ ≤ M) : PeriodizedWaveBounds.LocalJets s w α K fun (n : ℕ) (i : I) (x : D) => TangentProjection.pressureCoefficient (N n i x) (Ndot n i x) (u n i x) ((A n i x) (u n i x)) 0

theorem NavierStokes.SignedCopyBounds.local_projectedPressure {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {w : ℕ → D → ℝ} {α : ℝ} {N Ndot u : ℕ → I → D → Space} {A : ℕ → I → D → Space →L[ℝ] Space} {frequency : I → ℕ → ℝ} (hN : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K N) (hNdot : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K Ndot) (hA : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K A) (ha : PeriodizedWaveBounds.LocalJets s w α K u) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) {b M : ℝ} (hb : 0 < b) (hl : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ ‖N n i x‖) (hu : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ‖N n i x‖ ≤ M) (hK : UniformPrimaryWeights.UniformBandBound s (1 / 2) fun (i : I) (n : ℕ) => 1 / frequency i n) : PeriodizedWaveBounds.LocalJets s w (α + 1 / 2) K fun (n : ℕ) (i : I) => ParticularWaveBounds.projectedPressure (frequency i n) (N n i) (Ndot n i) (u n i) (fun (x : D) => (A n i x) (u n i x)) fun (x : D) => 0

theorem NavierStokes.SignedCopyBounds.coefficients_jets {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {a : I → LinearWaveBounds.WaveCoefficients D} {d : I → LinearWaveBounds.GraphDirections D} {H : I → ℕ → D → Mat2} {T R : I → ℕ → D → Vec2} {mask : I → ℕ → D → ℝ} {v Ndot : I → ℕ → D → Space} {A : I → ℕ → D → Space →L[ℝ] Space} {W : ℕ → D → ℝ} {β : ℝ} (h : NativeCovariance s K H T) (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => s.zeta x_1) β K fun (n : ℕ) (i : I) (x : D) => R i n x q) (hm : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => mask i n) (hv : PeriodizedWaveBounds.LocalJets s W 0 K fun (n : ℕ) (i : I) => v i n) (hW : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x) (hN : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => (a i).normal s (d i) n) (hNdot : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => Ndot i n) (hA : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => A i n) {b M : ℝ} (hb : 0 < b) (hl : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ ‖(a i).normal s (d i) n x‖) (hu : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ‖(a i).normal s (d i) n x‖ ≤ M) (hK : UniformPrimaryWeights.UniformBandBound s (1 / 2) fun (i : I) (n : ℕ) => 1 / (a i).frequency n) (j : Fin 2) : (PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) (β + 1 / 2) K fun (n : ℕ) (i : I) => (SignedWaveUpdate.coefficients (a i) s (d i) (H i) (T i) (R i) (mask i) (v i) (Ndot i) (A i) j).amplitude n) ∧ PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) (β + 1) K fun (n : ℕ) (i : I) => (SignedWaveUpdate.coefficients (a i) s (d i) (H i) (T i) (R i) (mask i) (v i) (Ndot i) (A i) j).pressure n

Native bounds for the literal signed quotient and its constructed homogeneous pressure. Even the background and frequency may vary with the copy index, provided their primitive estimates are uniform.

theorem NavierStokes.SignedCopyBounds.coefficients_localized_jets {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {a : I → LinearWaveBounds.WaveCoefficients D} {d : I → LinearWaveBounds.GraphDirections D} {H : I → ℕ → D → Mat2} {T R : I → ℕ → D → Vec2} {mask : I → ℕ → D → ℝ} {v Ndot : I → ℕ → D → Space} {A : I → ℕ → D → Space →L[ℝ] Space} {W : ℕ → D → ℝ} {β : ℝ} (h : NativeCovariance s K H T) (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => s.zeta x_1) β K fun (n : ℕ) (i : I) (x : D) => R i n x q) (hm : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => mask i n) (hv : PeriodizedWaveBounds.LocalJets s W 0 K fun (n : ℕ) (i : I) => v i n) (hW : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x) (hN : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => (a i).normal s (d i) n) (hNdot : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => Ndot i n) (hA : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => A i n) {b M : ℝ} (hb : 0 < b) (hl : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → b ≤ ‖(a i).normal s (d i) n x‖) (hu : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → ‖(a i).normal s (d i) n x‖ ≤ M) (hK : UniformPrimaryWeights.UniformBandBound s (1 / 2) fun (i : I) (n : ℕ) => 1 / (a i).frequency n) {ψ : I → ℕ → D → ℝ} (hψ : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => ψ i n) (j : Fin 2) : (PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) (β + 1 / 2) K fun (n : ℕ) (i : I) => ((SignedWaveUpdate.coefficients (a i) s (d i) (H i) (T i) (R i) (mask i) (v i) (Ndot i) (A i) j).withCutoff (ψ i)).amplitude n) ∧ PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : D) => √(s.zeta x) * W n x) (β + 1) K fun (n : ℕ) (i : I) => ((SignedWaveUpdate.coefficients (a i) s (d i) (H i) (T i) (R i) (mask i) (v i) (Ndot i) (A i) j).withCutoff (ψ i)).pressure n

The cutoff is applied exactly once. These are the coefficients consumed by PeriodizedWaveBounds.CopyData.common_bounds_from_native.

Uniformity in an external label as well as the native copy

theorem NavierStokes.SignedCopyBounds.local_pull {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Type} {s : WeightedClasses.StripData D} {α : ℝ} {w : L → ℕ → D → ℝ} {K : L → ℕ → I → Set D} {f : L → ℕ → I → D → E} (hf : PeriodizedWaveBounds.UniformLocalJets s w α K f) (e : ℕ → ℕ × L) : PeriodizedWaveBounds.LocalJets (UniformPrimaryWeights.reindexedStrip s e) (fun (k : ℕ) => w (e k).2 (e k).1) α (fun (k : ℕ) => K (e k).2 (e k).1) fun (k : ℕ) => f (e k).2 (e k).1

Reindexing the discrete band/label pair preserves the actual spatial derivatives and the full inverse-edge majorant.

theorem NavierStokes.SignedCopyBounds.uniform_local_of_pull {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Type} {s : WeightedClasses.StripData D} {α : ℝ} {w : L → ℕ → D → ℝ} {K : L → ℕ → I → Set D} {f : L → ℕ → I → D → E} {e : ℕ → ℕ × L} (he : Function.Surjective e) (hf : PeriodizedWaveBounds.LocalJets (UniformPrimaryWeights.reindexedStrip s e) (fun (k : ℕ) => w (e k).2 (e k).1) α (fun (k : ℕ) => K (e k).2 (e k).1) fun (k : ℕ) => f (e k).2 (e k).1) : PeriodizedWaveBounds.UniformLocalJets s w α K f

Surjectivity recovers all labels with the same constants. A collection of separately bounded label outputs would not suffice here.

theorem NavierStokes.SignedCopyBounds.uniform_smul {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Type} {s : WeightedClasses.StripData D} {α : ℝ} {w : L → ℕ → D → ℝ} {K : L → ℕ → I → Set D} {f : L → ℕ → I → D → E} [Countable L] [Nonempty L] {r : L → ℕ → I → D → ℝ} (hr : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K r) (hf : PeriodizedWaveBounds.UniformLocalJets s w α K f) (hw : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w l n x) : PeriodizedWaveBounds.UniformLocalJets s w α K fun (l : L) (n : ℕ) (i : I) (x : D) => r l n i x • f l n i x

structure NavierStokes.SignedCopyBounds.UniformNativeCovariance {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {L : Type} (s : WeightedClasses.StripData D) (K : L → ℕ → I → Set D) (H : L → I → ℕ → D → Mat2) (T : L → I → ℕ → D → Vec2) : Type

Primitive covariance data with one determinant gap, entry bound, positive weight margin, and finite-jet constants for all external labels.

• matrix_jets (a b : Fin 2) : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K fun (l : L) (n : ℕ) (i : I) (x : D) => H l i n x a b
• target_jets (a : Fin 2) : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => s.zeta x_2) 0 K fun (l : L) (n : ℕ) (i : I) (x : D) => T l i n x a
• zeta_pos (x : D) : x ∈ s.domain → 0 < s.zeta x
• determinantGap : ℝ

  Determinant gap of UniformNativeCovariance, of type ℝ.

• entryBound : ℝ

  Entry bound of UniformNativeCovariance, of type ℝ.

• primaryLower : ℝ

  Primary lower of UniformNativeCovariance, of type ℝ.

• gap_pos : 0 < self.determinantGap
• entry_one : 1 ≤ self.entryBound
• lower_pos : 0 < self.primaryLower
• determinant (l : L) (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K l n i → self.determinantGap ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (√(s.slow n)) (H l i n x))|
• entries (l : L) (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K l n i → ∀ (a b : Fin 2), |√(s.slow n) * H l i n x a b| ≤ self.entryBound
• lower (l : L) (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ K l n i → ∀ (j : Fin 2), self.primaryLower * s.zeta x ≤ SmoothCovariance.weights (H l i n x) (T l i n x) j

noncomputable def NavierStokes.SignedCopyBounds.UniformNativeCovariance.pull {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {L : Type} {s : WeightedClasses.StripData D} {K : L → ℕ → I → Set D} {H : L → I → ℕ → D → Mat2} {T : L → I → ℕ → D → Vec2} (h : UniformNativeCovariance s K H T) (e : ℕ → ℕ × L) : NativeCovariance (UniformPrimaryWeights.reindexedStrip s e) (fun (k : ℕ) => K (e k).2 (e k).1) (fun (i : I) (k : ℕ) => H (e k).2 i (e k).1) fun (i : I) (k : ℕ) => T (e k).2 i (e k).1

Pull, bundling matrix_jets, target_jets, zeta_pos, determinantGap and the required compatibility proofs.

Equations

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

theorem NavierStokes.SignedCopyBounds.uniform_coefficients_jets {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {L : Type} [Countable L] [Nonempty L] {s : WeightedClasses.StripData D} {K : L → ℕ → I → Set D} {a : L → I → LinearWaveBounds.WaveCoefficients D} {d : L → I → LinearWaveBounds.GraphDirections D} {H : L → I → ℕ → D → Mat2} {T R : L → I → ℕ → D → Vec2} {mask : L → I → ℕ → D → ℝ} {v Ndot : L → I → ℕ → D → Space} {A : L → I → ℕ → D → Space →L[ℝ] Space} {W : L → ℕ → D → ℝ} {β : ℝ} (h : UniformNativeCovariance s K H T) (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => s.zeta x_2) β K fun (l : L) (n : ℕ) (i : I) (x : D) => R l i n x q) (hm : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K fun (l : L) (n : ℕ) (i : I) => mask l i n) (hv : PeriodizedWaveBounds.UniformLocalJets s W 0 K fun (l : L) (n : ℕ) (i : I) => v l i n) (hW : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hN : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K fun (l : L) (n : ℕ) (i : I) => (a l i).normal s (d l i) n) (hNdot : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K fun (l : L) (n : ℕ) (i : I) => Ndot l i n) (hA : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K fun (l : L) (n : ℕ) (i : I) => A l i n) {b M : ℝ} (hb : 0 < b) (hl : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → b ≤ ‖(a l i).normal s (d l i) n x‖) (hu : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → ‖(a l i).normal s (d l i) n x‖ ≤ M) (hK : UniformPrimaryWeights.UniformBandBound s (1 / 2) fun (li : L × I) (n : ℕ) => 1 / (a li.1 li.2).frequency n) (j : Fin 2) : (PeriodizedWaveBounds.UniformLocalJets s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) (β + 1 / 2) K fun (l : L) (n : ℕ) (i : I) => (SignedWaveUpdate.coefficients (a l i) s (d l i) (H l i) (T l i) (R l i) (mask l i) (v l i) (Ndot l i) (A l i) j).amplitude n) ∧ PeriodizedWaveBounds.UniformLocalJets s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) (β + 1) K fun (l : L) (n : ℕ) (i : I) => (SignedWaveUpdate.coefficients (a l i) s (d l i) (H l i) (T l i) (R l i) (mask l i) (v l i) (Ndot l i) (A l i) j).pressure n

The amplitude and projected-pressure estimates are simultaneous in all spatial labels, all bands and all lattice copies. Label-dependent envelopes are retained.

theorem NavierStokes.SignedCopyBounds.uniform_coefficients_localized_jets {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {L : Type} [Countable L] [Nonempty L] {s : WeightedClasses.StripData D} {K : L → ℕ → I → Set D} {a : L → I → LinearWaveBounds.WaveCoefficients D} {d : L → I → LinearWaveBounds.GraphDirections D} {H : L → I → ℕ → D → Mat2} {T R : L → I → ℕ → D → Vec2} {mask : L → I → ℕ → D → ℝ} {v Ndot : L → I → ℕ → D → Space} {A : L → I → ℕ → D → Space →L[ℝ] Space} {W : L → ℕ → D → ℝ} {β : ℝ} (h : UniformNativeCovariance s K H T) (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => s.zeta x_2) β K fun (l : L) (n : ℕ) (i : I) (x : D) => R l i n x q) (hm : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K fun (l : L) (n : ℕ) (i : I) => mask l i n) (hv : PeriodizedWaveBounds.UniformLocalJets s W 0 K fun (l : L) (n : ℕ) (i : I) => v l i n) (hW : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hN : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K fun (l : L) (n : ℕ) (i : I) => (a l i).normal s (d l i) n) (hNdot : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K fun (l : L) (n : ℕ) (i : I) => Ndot l i n) (hA : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K fun (l : L) (n : ℕ) (i : I) => A l i n) {b M : ℝ} (hb : 0 < b) (hl : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → b ≤ ‖(a l i).normal s (d l i) n x‖) (hu : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → ‖(a l i).normal s (d l i) n x‖ ≤ M) (hK : UniformPrimaryWeights.UniformBandBound s (1 / 2) fun (li : L × I) (n : ℕ) => 1 / (a li.1 li.2).frequency n) {ψ : L → I → ℕ → D → ℝ} (hψ : PeriodizedWaveBounds.UniformLocalJets s (fun (x : L) (x_1 : ℕ) (x_2 : D) => 1) 0 K fun (l : L) (n : ℕ) (i : I) => ψ l i n) (j : Fin 2) : (PeriodizedWaveBounds.UniformLocalJets s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) (β + 1 / 2) K fun (l : L) (n : ℕ) (i : I) => ((SignedWaveUpdate.coefficients (a l i) s (d l i) (H l i) (T l i) (R l i) (mask l i) (v l i) (Ndot l i) (A l i) j).withCutoff (ψ l i)).amplitude n) ∧ PeriodizedWaveBounds.UniformLocalJets s (fun (l : L) (n : ℕ) (x : D) => √(s.zeta x) * W l n x) (β + 1) K fun (l : L) (n : ℕ) (i : I) => ((SignedWaveUpdate.coefficients (a l i) s (d l i) (H l i) (T l i) (R l i) (mask l i) (v l i) (Ndot l i) (A l i) j).withCutoff (ψ l i)).pressure n

Uniform native data control the actual once-localized coefficients; the constants can be passed directly to uniform periodization.