Weighted native estimates for the constructed primary copies

The local domains retain the actual label-dependent slow cells. Every constant is chosen before that label, its band, and the lattice copy. The square-root estimates retain the vanishing flat weight.

structure NavierStokes.PrimaryCopyBounds.JetDomain (ι : Type u_5) (D : Type u_6) [NormedAddCommGroup D] extends NavierStokes.PhaseJetBounds.Domain ι D : Type (max u_5 u_6)

A local chart domain with the actual slow/inverse-edge growth.

• scale : ι → ℝ
• carrier : ι → Set D
• isOpen (i : ι) : IsOpen (self.carrier i)
• one_le_scale (i : ι) : 1 ≤ self.scale i
• growth : ι → D → ℝ

  Growth of JetDomain, of type ι → D → ℝ.

• scale_le_growth (i : ι) (x : D) : x ∈ self.carrier i → self.scale i ≤ self.growth i x

theorem NavierStokes.PrimaryCopyBounds.JetDomain.one_le_growth {ι : Type u_1} {D : Type} [NormedAddCommGroup D] (V : JetDomain ι D) (i : ι) {x : D} (hx : x ∈ V.carrier i) : 1 ≤ V.growth i x

structure NavierStokes.PrimaryCopyBounds.NativeJets {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (V : JetDomain ι D) (w : ι → D → ℝ) (f : ι → D → E) : Prop

Actual full jets on varying native cells, retaining their full weight.

• nonneg (i : ι) (x : D) : x ∈ V.carrier i → 0 ≤ w i x
• smooth (i : ι) : ContDiffOn ℝ (↑⊤) (f i) (V.carrier i)
• bound (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (i : ι), ∀ x ∈ V.carrier i, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f i) x‖ ≤ C * V.growth i x ^ p * w i x

theorem NavierStokes.PrimaryCopyBounds.NativeJets.of_envelope {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} (hf : PrimaryPulseBounds.EnvelopeJets V.toDomain w f) : NativeJets V w f

theorem NavierStokes.PrimaryCopyBounds.NativeJets.of_polynomial {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {f : ι → D → E} (hf : PhaseJetBounds.PolynomialJets V.toDomain f) : NativeJets V (fun (x : ι) (x_1 : D) => 1) f

theorem NavierStokes.PrimaryCopyBounds.NativeJets.congr {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w : ι → D → ℝ} {f g : ι → D → E} (hf : NativeJets V w f) (he : ∀ (i : ι), Set.EqOn (f i) (g i) (V.carrier i)) : NativeJets V w g

theorem NavierStokes.PrimaryCopyBounds.NativeJets.map {ι : Type u_1} {D : Type} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} (hf : NativeJets V w f) (L : E →L[ℝ] F) : NativeJets V w fun (i : ι) (x : D) => L (f i x)

theorem NavierStokes.PrimaryCopyBounds.NativeJets.add {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w : ι → D → ℝ} {f g : ι → D → E} (hf : NativeJets V w f) (hg : NativeJets V w g) : NativeJets V w fun (i : ι) (x : D) => f i x + g i x

theorem NavierStokes.PrimaryCopyBounds.NativeJets.neg {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} (hf : NativeJets V w f) : NativeJets V w fun (i : ι) (x : D) => -f i x

theorem NavierStokes.PrimaryCopyBounds.NativeJets.sub {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w : ι → D → ℝ} {f g : ι → D → E} (hf : NativeJets V w f) (hg : NativeJets V w g) : NativeJets V w fun (i : ι) (x : D) => f i x - g i x

theorem NavierStokes.PrimaryCopyBounds.NativeJets.bilinear {ι : Type u_1} {D : Type} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {V : JetDomain ι D} {w v : ι → D → ℝ} {f : ι → D → E} {g : ι → D → F} (hf : NativeJets V w f) (hg : NativeJets V v g) (L : E →L[ℝ] F →L[ℝ] G) : NativeJets V (fun (i : ι) (x : D) => w i x * v i x) fun (i : ι) (x : D) => (L (f i x)) (g i x)

theorem NavierStokes.PrimaryCopyBounds.NativeJets.mul {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {w v f g : ι → D → ℝ} (hf : NativeJets V w f) (hg : NativeJets V v g) : NativeJets V (fun (i : ι) (x : D) => w i x * v i x) fun (i : ι) (x : D) => f i x * g i x

theorem NavierStokes.PrimaryCopyBounds.NativeJets.smul {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w v f : ι → D → ℝ} {g : ι → D → E} (hf : NativeJets V w f) (hg : NativeJets V v g) : NativeJets V (fun (i : ι) (x : D) => w i x * v i x) fun (i : ι) (x : D) => f i x • g i x

theorem NavierStokes.PrimaryCopyBounds.NativeJets.polynomial_smul {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} {a : ι → D → ℝ} (hf : NativeJets V w f) (ha : PhaseJetBounds.PolynomialJets V.toDomain a) : NativeJets V w fun (i : ι) (x : D) => a i x • f i x

theorem NavierStokes.PrimaryCopyBounds.NativeJets.polynomial_mul {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {w f a : ι → D → ℝ} (hf : NativeJets V w f) (ha : PhaseJetBounds.PolynomialJets V.toDomain a) : NativeJets V w fun (i : ι) (x : D) => a i x * f i x

theorem NavierStokes.PrimaryCopyBounds.NativeJets.band_smul {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} (hf : NativeJets V w f) (a : ι → ℝ) (ha : ∀ (i : ι), 0 ≤ a i) : NativeJets V (fun (i : ι) (x : D) => a i * w i x) fun (i : ι) (x : D) => a i • f i x

theorem NavierStokes.PrimaryCopyBounds.NativeJets.sqrt {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {w g : ι → D → ℝ} (hg : NativeJets V w g) (hw : ∀ (i : ι), ∀ x ∈ V.carrier i, 0 < w i x) {c : ℝ} (hc : 0 < c) (hlower : ∀ (i : ι), ∀ x ∈ V.carrier i, c * w i x ≤ g i x) : NativeJets V (fun (i : ι) (x : D) => √(w i x)) fun (i : ι) (x : D) => √(g i x)

The exact square root of a vanishing weight is retained. The lower bound is proportional to that weight; no positive minimum is introduced.

theorem NavierStokes.PrimaryCopyBounds.covariance_weights_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {w : ι → D → ℝ} {r : ι → ℝ} {H : ι → D → SmoothCovariance.Mat2} {T : ι → D → SmoothCovariance.Vec2} (hr : PhaseJetBounds.PolynomialJets V.toDomain fun (i : ι) (x : D) => r i) (hrne : ∀ (i : ι), r i ≠ 0) (hH : ∀ (k l : Fin 2), PhaseJetBounds.PolynomialJets V.toDomain fun (i : ι) (x : D) => H i x k l) (hT : ∀ (k : Fin 2), NativeJets V w fun (i : ι) (x : D) => T i x k) {b M : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hdet : ∀ (i : ι), ∀ x ∈ V.carrier i, b ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (r i) (H i x))|) (hentry : ∀ (i : ι), ∀ x ∈ V.carrier i, ∀ (k l : Fin 2), |r i * H i x k l| ≤ M) (j : Fin 2) : NativeJets V w fun (i : ι) (x : D) => SmoothCovariance.weights (H i x) (T i x) j

Cramer's actual formula on the varying native cells. Only the normalized matrix has a positive lower bound; the target keeps its weight.

theorem NavierStokes.PrimaryCopyBounds.covariance_amplitudes_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {w : ι → D → ℝ} {r : ι → ℝ} {H : ι → D → SmoothCovariance.Mat2} {T : ι → D → SmoothCovariance.Vec2} (hr : PhaseJetBounds.PolynomialJets V.toDomain fun (i : ι) (x : D) => r i) (hrne : ∀ (i : ι), r i ≠ 0) (hH : ∀ (k l : Fin 2), PhaseJetBounds.PolynomialJets V.toDomain fun (i : ι) (x : D) => H i x k l) (hT : ∀ (k : Fin 2), NativeJets V w fun (i : ι) (x : D) => T i x k) {b M c : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hc : 0 < c) (hdet : ∀ (i : ι), ∀ x ∈ V.carrier i, b ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (r i) (H i x))|) (hentry : ∀ (i : ι), ∀ x ∈ V.carrier i, ∀ (k l : Fin 2), |r i * H i x k l| ≤ M) (hw : ∀ (i : ι), ∀ x ∈ V.carrier i, 0 < w i x) (hlower : ∀ (i : ι), ∀ x ∈ V.carrier i, ∀ (k : Fin 2), c * w i x ≤ SmoothCovariance.weights (H i x) (T i x) k) (j : Fin 2) : NativeJets V (fun (i : ι) (x : D) => √(w i x)) fun (i : ι) (x : D) => SmoothCovariance.amplitudes (H i x) (T i x) j

theorem NavierStokes.PrimaryCopyBounds.pressureCoefficient_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {w : ι → D → ℝ} {N Ndot u : ι → D → ProblemStatement.Space} {A : ι → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space} (hN : PhaseJetBounds.PolynomialJets V.toDomain N) (hNdot : PhaseJetBounds.PolynomialJets V.toDomain Ndot) (hA : PhaseJetBounds.PolynomialJets V.toDomain A) (hu : NativeJets V w u) {b M : ℝ} (hb : 0 < b) (hlo : ∀ (i : ι), ∀ x ∈ V.carrier i, b ≤ ‖N i x‖) (hhi : ∀ (i : ι), ∀ x ∈ V.carrier i, ‖N i x‖ ≤ M) : NativeJets V w fun (i : ι) (x : D) => TangentProjection.pressureCoefficient (N i x) (Ndot i x) (u i x) ((A i x) (u i x)) 0

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

Pulse matrix, defined pointwise by primaryCovariance pref (fun j => (F j).frame) (fun j => (F j).lam) (fun j => (F j).u) (fun j => (F j).L) i (χ i x).1.

Equations

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

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

Pulse vector, defined pointwise by normalizedPulse ((F j).frame i) ((F j).lam i) ((F j).u i) ((F j).L i) (χ i x).

Equations

• NavierStokes.PrimaryCopyBounds.pulseVector F χ j i x = NavierStokes.PrimaryPulseBounds.normalizedPulse ((F j).frame i) ((F j).lam i) ((F j).u i) ((F j).L i) (χ i x)

noncomputable def NavierStokes.PrimaryCopyBounds.pulseEnvelope {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) (j : Fin 2) : ι → D → ℝ

Pulse envelope, defined pointwise by referenceP ((F j).lam i) ((F j).u i) ((F j).L i) ((F j).L i * (χ i x).2).

Equations

• NavierStokes.PrimaryCopyBounds.pulseEnvelope F χ j i x = NavierStokes.PrimaryPulseBounds.referenceP ((F j).lam i) ((F j).u i) ((F j).L i) ((F j).L i * (χ i x).2)

noncomputable def NavierStokes.PrimaryCopyBounds.primaryVelocity {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ι → ℝ) (χ : ι → D → PhaseCalculus.Slow × ℝ) (ε : ι → ℝ) (T : ι → D → SmoothCovariance.Vec2) (mask : ι → D → ℝ) (j : Fin 2) : ι → D → ProblemStatement.Space

Primary velocity, defined pointwise by PartitionedCovariance.amplitude (ε i) (mask i x) (pulseMatrix F pref χ i x) (T i x) j • pulseVector F χ j i x.

Equations

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

theorem NavierStokes.PrimaryCopyBounds.primaryVelocity_mask_mul {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ι → ℝ) (χ : ι → D → PhaseCalculus.Slow × ℝ) (ε : ι → ℝ) (T : ι → D → SmoothCovariance.Vec2) (mask κ : ι → D → ℝ) (j : Fin 2) (i : ι) (x : D) : primaryVelocity F pref χ ε T (fun (i : ι) (x : D) => κ i x * mask i x) j i x = κ i x • primaryVelocity F pref χ ε T mask j i x

theorem NavierStokes.PrimaryCopyBounds.primaryVelocity_complexify {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (s : WeightedClasses.StripData D) (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (χ : ℕ → D → PhaseCalculus.Slow × ℝ) (T : ℕ → D → SmoothCovariance.Vec2) (mask : ℕ → D → ℝ) (j : Fin 2) (n : ℕ) (x : D) : CurlClassBounds.complexify (primaryVelocity F pref χ s.epsilon T mask j n x) = PrimaryPulseBounds.uncutPrimaryWave s pref (fun (j : Fin 2) => (F j).frame) (fun (j : Fin 2) => (F j).lam) (fun (j : Fin 2) => (F j).u) (fun (j : Fin 2) => (F j).L) χ T mask j n x

theorem NavierStokes.PrimaryCopyBounds.pulseMatrix_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ι → ℝ) (χ : ι → D → PhaseCalculus.Slow × ℝ) (hscale : ∀ (i : ι), U.scale i = V.scale i) (hχ : PhaseJetBounds.PolynomialJets V.toDomain χ) (hmap : ∀ (i : ι), ∀ x ∈ V.carrier i, (χ i x).1 ∈ U.carrier i) (hpref : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets U fun (i : ι) (x : PhaseCalculus.Slow) => pref j i) (j k : Fin 2) : PhaseJetBounds.PolynomialJets V.toDomain fun (i : ι) (x : D) => pulseMatrix F pref χ i x j k

theorem NavierStokes.PrimaryCopyBounds.pulseVector_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) (hscale : ∀ (i : ι), U.scale i = V.scale i) (hχ : PhaseJetBounds.PolynomialJets V.toDomain χ) (hmap : ∀ (i : ι), ∀ x ∈ V.carrier i, χ i x ∈ U.carrier i ×ˢ Set.Ioo 0 1) (j : Fin 2) : NativeJets V (pulseEnvelope F χ j) (pulseVector F χ j)

theorem NavierStokes.PrimaryCopyBounds.sqrt_scale_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (V : JetDomain ι D) : PhaseJetBounds.PolynomialJets V.toDomain fun (i : ι) (x : D) => √(V.scale i)

theorem NavierStokes.PrimaryCopyBounds.primaryVelocity_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ι → ℝ) (χ : ι → D → PhaseCalculus.Slow × ℝ) (ε : ι → ℝ) (T : ι → D → SmoothCovariance.Vec2) (mask ζ : ι → D → ℝ) (hscale : ∀ (i : ι), U.scale i = V.scale i) (hχ : PhaseJetBounds.PolynomialJets V.toDomain χ) (hmap : ∀ (i : ι), ∀ x ∈ V.carrier i, χ i x ∈ U.carrier i ×ˢ Set.Ioo 0 1) (hpref : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets U fun (i : ι) (x : PhaseCalculus.Slow) => pref j i) (hT : ∀ (k : Fin 2), NativeJets V ζ fun (i : ι) (x : D) => T i x k) (hm : PhaseJetBounds.PolynomialJets V.toDomain mask) (hζ : ∀ (i : ι), ∀ x ∈ V.carrier i, 0 < ζ i x) {b M c : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hc : 0 < c) (hzero : ∀ (i : ι), ∀ x ∈ V.carrier i, PrimaryCovarianceBounds.ZeroOrderBounds (√(V.scale i)) b M c (ζ i x) (pulseMatrix F pref χ i x) (T i x)) (j : Fin 2) : NativeJets V (fun (i : ι) (x : D) => √(ε i) * (√(ζ i x) * pulseEnvelope F χ j i x)) (primaryVelocity F pref χ ε T mask j)

The native primary is the actual homogeneous Volterra pulse, scaled by the actual Cramer square root and physical square-root epsilon factor.

theorem NavierStokes.PrimaryCopyBounds.NativeJets.constant_weight {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} (a : ι → E) (v : ι → ℝ) (hv : ∀ (i : ι), 0 ≤ v i) {C : ℝ} (hC : 1 ≤ C) (p : ℕ) (ha : ∀ (i : ι), ‖a i‖ ≤ C * V.scale i ^ p * v i) : NativeJets V (fun (i : ι) (x : D) => v i) fun (i : ι) (x : D) => a i

theorem NavierStokes.PrimaryCopyBounds.NativeJets.localize {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} {V' : JetDomain ι D} {a : ι → D → ℝ} (hf : NativeJets V w f) (ha : PhaseJetBounds.PolynomialJets V'.toDomain a) (hscale : ∀ (i : ι), V'.scale i = V.scale i) (hsub : ∀ (i : ι), V.carrier i ⊆ V'.carrier i) (hgrowth : ∀ (i : ι), ∀ x ∈ V.carrier i, V.growth i x = V'.growth i x) (hw : ∀ (i : ι), ∀ x ∈ V'.carrier i, 0 ≤ w i x) (hsupport : ∀ (i : ι), tsupport (a i) ∩ V'.carrier i ⊆ V.carrier i) : NativeJets V' w fun (i : ι) (x : D) => a i x • f i x

A compactly contained outer cutoff extends the true native function. Every cutoff derivative is included in the product estimate.

theorem NavierStokes.PrimaryCopyBounds.projectedPressure_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {w : ι → D → ℝ} {N Ndot u : ι → D → ProblemStatement.Space} {A : ι → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space} (hN : PhaseJetBounds.PolynomialJets V.toDomain N) (hNdot : PhaseJetBounds.PolynomialJets V.toDomain Ndot) (hA : PhaseJetBounds.PolynomialJets V.toDomain A) (hu : NativeJets V w u) {b M : ℝ} (hb : 0 < b) (hlo : ∀ (i : ι), ∀ x ∈ V.carrier i, b ≤ ‖N i x‖) (hhi : ∀ (i : ι), ∀ x ∈ V.carrier i, ‖N i x‖ ≤ M) (ε frequency : ι → ℝ) (hε : ∀ (i : ι), 0 < ε i) {C : ℝ} (hC : 1 ≤ C) (p : ℕ) (hfrequency : ∀ (i : ι), |1 / frequency i| ≤ C * V.scale i ^ p * √(ε i)) : NativeJets V (fun (i : ι) (x : D) => √(ε i) * w i x) fun (i : ι) => ParticularWaveBounds.projectedPressure (frequency i) (N i) (Ndot i) (u i) (fun (x : D) => (A i x) (u i x)) fun (x : D) => 0

The literal projected pressure gains the inverse-carrier half power. The source is homogeneous, so its pressure source term is exactly zero.

noncomputable def NavierStokes.PrimaryCopyBounds.phasePoint {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (p : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) : ι → D → PhaseCalculus.Slow × ℝ

The actual phase is evaluated at the physical native time L*tau.

Equations

• NavierStokes.PrimaryCopyBounds.phasePoint p χ i x = ((χ i x).1, p.L i * (χ i x).2)

noncomputable def NavierStokes.PrimaryCopyBounds.phasePressure {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (p : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) (frequency : ι → ℝ) (u : ι → D → ProblemStatement.Space) : ι → D → ℂ

Phase pressure as an element of ι → D → ℂ.

Equations

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

theorem NavierStokes.PrimaryCopyBounds.phasePoint_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (p : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) (hscale : ∀ (i : ι), U.scale i = V.scale i) (hχ : PhaseJetBounds.PolynomialJets V.toDomain χ) : PhaseJetBounds.PolynomialJets V.toDomain (phasePoint p χ)

theorem NavierStokes.PrimaryCopyBounds.phasePoint_maps {ι : Type u_1} {D : Type} [NormedAddCommGroup D] {V : JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (p : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) (hmap : ∀ (i : ι), ∀ x ∈ V.carrier i, χ i x ∈ U.carrier i ×ˢ Set.Ioo 0 1) (i : ι) (x : D) : x ∈ V.carrier i → phasePoint p χ i x ∈ (U.slot p.V ⋯).carrier i

theorem NavierStokes.PrimaryCopyBounds.phasePressure_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (p : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) (hscale : ∀ (i : ι), U.scale i = V.scale i) (hχ : PhaseJetBounds.PolynomialJets V.toDomain χ) (hmap : ∀ (i : ι), ∀ x ∈ V.carrier i, χ i x ∈ U.carrier i ×ˢ Set.Ioo 0 1) {w : ι → D → ℝ} {u : ι → D → ProblemStatement.Space} (hu : NativeJets V w u) (ε frequency : ι → ℝ) (hε : ∀ (i : ι), 0 < ε i) {C : ℝ} (hC : 1 ≤ C) (q : ℕ) (hfrequency : ∀ (i : ι), |1 / frequency i| ≤ C * V.scale i ^ q * √(ε i)) : NativeJets V (fun (i : ι) (x : D) => √(ε i) * w i x) (phasePressure p χ frequency u)

Phase-normal, normal-motion and shear estimates all come from the same base and phase construction as the true homogeneous pulse.

theorem NavierStokes.PrimaryCopyBounds.phasePressure_carrier_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (p : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) (hscale : ∀ (i : ι), U.scale i = V.scale i) (hχ : PhaseJetBounds.PolynomialJets V.toDomain χ) (hmap : ∀ (i : ι), ∀ x ∈ V.carrier i, χ i x ∈ U.carrier i ×ˢ Set.Ioo 0 1) {w : ι → D → ℝ} {u : ι → D → ProblemStatement.Space} (hu : NativeJets V w u) (h : ℝ) (hh : 0 ≤ h) (band : ι → ℕ) : NativeJets V (fun (i : ι) (x : D) => √(ChartScales.epsilon h (band i)) * w i x) (phasePressure p χ (fun (i : ι) => ↑(ChartScales.carrier h (band i))) u)

The rounded carrier gives the claimed half-power without a frequency bound supplied by the caller.

theorem NavierStokes.PrimaryCopyBounds.phasePressure_smul {ι : Type u_1} {D : Type} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (p : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) (frequency : ι → ℝ) (a : ι → D → ℝ) (u : ι → D → ProblemStatement.Space) (i : ι) (x : D) : phasePressure p χ frequency (fun (i : ι) (x : D) => a i x • u i x) i x = a i x • phasePressure p χ frequency u i x

The actual outer slot cutoff

noncomputable def NavierStokes.PrimaryCopyBounds.outerBump : ContDiffBump (1 / 2)

Outer bump, bundling rIn, rOut, rIn_pos, rIn_lt_rOut.

Equations

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

noncomputable def NavierStokes.PrimaryCopyBounds.outerCutoff : ℝ → ℝ

Outer cutoff, given by outerBump.

Equations

• NavierStokes.PrimaryCopyBounds.outerCutoff = ↑NavierStokes.PrimaryCopyBounds.outerBump

theorem NavierStokes.PrimaryCopyBounds.outerCutoff_smooth : ContDiff ℝ (↑⊤) outerCutoff

theorem NavierStokes.PrimaryCopyBounds.outerCutoff_support : tsupport outerCutoff ⊆ Set.Icc (1 / 12) (11 / 12)

theorem NavierStokes.PrimaryCopyBounds.outerCutoff_one {t : ℝ} (ht : |t - 1 / 2| ≤ 1 / 3) : outerCutoff t = 1

theorem NavierStokes.PrimaryCopyBounds.profile_mul_outerCutoff (t : ℝ) : GaussianTailFlat.profile t * outerCutoff t = GaussianTailFlat.profile t

theorem NavierStokes.PrimaryCopyBounds.outerCutoff_jet_bounded (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ), ‖iteratedFDeriv ℝ m outerCutoff t‖ ≤ C

theorem NavierStokes.PrimaryCopyBounds.affine_profile_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : PhaseJetBounds.Domain ι D) (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hjets : ∀ (m : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ), ‖iteratedFDeriv ℝ m f t‖ ≤ C) (L : ι → D →L[ℝ] ℝ) (c : ι → ℝ) {K : ℝ} (hK : 1 ≤ K) (q : ℕ) (hL : ∀ (i : ι), ‖L i‖ ≤ K * U.scale i ^ q) : PhaseJetBounds.PolynomialJets U fun (i : ι) (x : D) => f ((L i) x + c i)

theorem NavierStokes.PrimaryCopyBounds.outerCutoff_affine_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : PhaseJetBounds.Domain ι D) (L : ι → D →L[ℝ] ℝ) (c : ι → ℝ) {K : ℝ} (hK : 1 ≤ K) (q : ℕ) (hL : ∀ (i : ι), ‖L i‖ ≤ K * U.scale i ^ q) : PhaseJetBounds.PolynomialJets U fun (i : ι) (x : D) => outerCutoff ((L i) x + c i)

theorem NavierStokes.PrimaryCopyBounds.gaussianCutoff_affine_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : PhaseJetBounds.Domain ι D) (L : ι → D →L[ℝ] ℝ) (c : ι → ℝ) {K : ℝ} (hK : 1 ≤ K) (q : ℕ) (hL : ∀ (i : ι), ‖L i‖ ≤ K * U.scale i ^ q) : PhaseJetBounds.PolynomialJets U fun (i : ι) (x : D) => GaussianTailFlat.profile ((L i) x + c i)

theorem NavierStokes.PrimaryCopyBounds.gaussian_outer_primary {D : Type} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (u : D → E) (τ : D → ℝ) : (fun (x : D) => GaussianTailFlat.profile (τ x) • outerCutoff (τ x) • u x) = fun (x : D) => GaussianTailFlat.profile (τ x) • u x

The outer extension never inserts a second Gaussian cutoff.

theorem NavierStokes.PrimaryCopyBounds.outerCutoff_affine_support {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (L : D →L[ℝ] ℝ) (c : ℝ) : (tsupport fun (x : D) => outerCutoff (L x + c)) ⊆ {x : D | L x + c ∈ Set.Ioo 0 1}

theorem NavierStokes.PrimaryCopyBounds.outer_localized_jets {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V V' : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} (hf : NativeJets V w f) (L : ι → D →L[ℝ] ℝ) (c : ι → ℝ) {K : ℝ} (hK : 1 ≤ K) (q : ℕ) (hL : ∀ (i : ι), ‖L i‖ ≤ K * V'.scale i ^ q) (hscale : ∀ (i : ι), V'.scale i = V.scale i) (hsub : ∀ (i : ι), V.carrier i ⊆ V'.carrier i) (hgrowth : ∀ (i : ι), ∀ x ∈ V.carrier i, V.growth i x = V'.growth i x) (hinside : ∀ (i : ι), ∀ x ∈ V'.carrier i, (L i) x + c i ∈ Set.Ioo 0 1 → x ∈ V.carrier i) (hw : ∀ (i : ι), ∀ x ∈ V'.carrier i, 0 ≤ w i x) : NativeJets V' w fun (i : ι) (x : D) => outerCutoff ((L i) x + c i) • f i x

The actual outer cutoff permits a larger native domain while retaining the uncut fundamental's Gaussian envelope and flat weight.

Transfer to the actual copy coordinates

noncomputable def NavierStokes.PrimaryCopyBounds.affineCopy {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {Λ : Type u_5} {I : Type u_6} (f : ι → D → E) (index : Λ → ℕ → ι) (L : Λ → ℕ → I → X →L[ℝ] D) (c : Λ → ℕ → I → D) : Λ → ℕ → I → X → E

Affine copy, defined pointwise by f (index l n) (L l n i x + c l n i).

Equations

• NavierStokes.PrimaryCopyBounds.affineCopy f index L c l n i x = f (index l n) ((L l n i) x + c l n i)

theorem NavierStokes.PrimaryCopyBounds.NativeJets.copy_localJets {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {Λ : Type u_5} {I : Type u_6} {V : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} (hf : NativeJets V w f) (s : WeightedClasses.StripData X) (W : Λ → ℕ → X → ℝ) (α : ℝ) (index : Λ → ℕ → ι) (L : Λ → ℕ → I → X →L[ℝ] D) (c : Λ → ℕ → I → D) (K : Λ → ℕ → I → Set X) (hW : ∀ (l : Λ) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hmap : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → (L l n i) x + c l n i ∈ V.carrier (index l n)) {A B : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (a b : ℕ) (hgrowth : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → V.growth (index l n) ((L l n i) x + c l n i) ≤ A * s.growth n x ^ a) (hlinear : ∀ (l : Λ) (n : ℕ) (i : I), ‖L l n i‖ ≤ B * s.slow n ^ b) (hweight : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → w (index l n) ((L l n i) x + c l n i) ≤ s.epsilon n ^ α * W l n x) : PeriodizedWaveBounds.UniformLocalJets s W α K (affineCopy f index L c)

The copy translation is arbitrary. Only the linear part's uniform polynomial size matters, so the constants precede the lattice index.

theorem NavierStokes.PrimaryCopyBounds.NativeJets.localized_copy_sum_uniformClass {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {Λ : Type u_5} {I : Type u_6} {V : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} (hf : NativeJets V w f) (s : WeightedClasses.StripData X) (W : Λ → ℕ → X → ℝ) (α : ℝ) (κ : ι → D → ℝ) (hκ : PhaseJetBounds.PolynomialJets V.toDomain κ) (index : Λ → ℕ → ι) (L : Λ → ℕ → I → X →L[ℝ] D) (c : Λ → ℕ → I → D) (K : Λ → PeriodizedWaveBounds.Cells X I) (hW : ∀ (l : Λ) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hcut : ∀ (l : Λ) (n : ℕ) (i : I) (x : X), κ (index l n) ((L l n i) x + c l n i) ≠ 0 → x ∈ (K l).carrier n i) (hmap : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → (L l n i) x + c l n i ∈ V.carrier (index l n)) {A B : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (a b : ℕ) (hgrowth : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → V.growth (index l n) ((L l n i) x + c l n i) ≤ A * s.growth n x ^ a) (hlinear : ∀ (l : Λ) (n : ℕ) (i : I), ‖L l n i‖ ≤ B * s.slow n ^ b) (hweight : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → w (index l n) ((L l n i) x + c l n i) ≤ s.epsilon n ^ α * W l n x) : LabelSumBounds.UniformClass s W α fun (l : Λ) (n : ℕ) => PeriodizedWaveBounds.copySum (affineCopy (fun (i : ι) (x : D) => κ i x • f i x) index L c l n)

A literal cutoff times the native function gives its own support proof. Local finiteness and uniqueness then retain the very same uniform constants in the actual infinite copy sum.

theorem NavierStokes.PrimaryCopyBounds.NativeJets.outer_copy_sum_uniformClass {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {Λ : Type u_5} {I : Type u_6} {V : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} (hf : NativeJets V w f) (s : WeightedClasses.StripData X) (W : Λ → ℕ → X → ℝ) (α : ℝ) (κ : ι → D → ℝ) (hκ : PhaseJetBounds.PolynomialJets V.toDomain κ) (τ : ι → D →L[ℝ] ℝ) (t0 : ι → ℝ) {H : ℝ} (hH : 1 ≤ H) (q : ℕ) (hτ : ∀ (i : ι), ‖τ i‖ ≤ H * V.scale i ^ q) (index : Λ → ℕ → ι) (L : Λ → ℕ → I → X →L[ℝ] D) (c : Λ → ℕ → I → D) (K : Λ → PeriodizedWaveBounds.Cells X I) (hW : ∀ (l : Λ) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hcut : ∀ (l : Λ) (n : ℕ) (i : I) (x : X), κ (index l n) ((L l n i) x + c l n i) ≠ 0 → outerCutoff ((τ (index l n)) ((L l n i) x + c l n i) + t0 (index l n)) ≠ 0 → x ∈ (K l).carrier n i) (hmap : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → (L l n i) x + c l n i ∈ V.carrier (index l n)) {A B : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (a b : ℕ) (hgrowth : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → V.growth (index l n) ((L l n i) x + c l n i) ≤ A * s.growth n x ^ a) (hlinear : ∀ (l : Λ) (n : ℕ) (i : I), ‖L l n i‖ ≤ B * s.slow n ^ b) (hweight : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → w (index l n) ((L l n i) x + c l n i) ≤ s.epsilon n ^ α * W l n x) : LabelSumBounds.UniformClass s W α fun (l : Λ) (n : ℕ) => PeriodizedWaveBounds.copySum (affineCopy (fun (i : ι) (x : D) => (κ i x * outerCutoff ((τ i) x + t0 i)) • f i x) index L c l n)

The explicit outer slot bump is included in the differentiated cutoff. This endpoint assumes support only of the scalar cutoffs.

theorem NavierStokes.PrimaryCopyBounds.NativeJets.of_order {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} (hw : ∀ (i : ι), ∀ x ∈ V.carrier i, 0 ≤ w i x) (hs : ∀ (i : ι), ContDiffOn ℝ (↑⊤) (f i) (V.carrier i)) (hb : ∀ (m : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (i : ι), ∀ x ∈ V.carrier i, ‖iteratedFDeriv ℝ m (f i) x‖ ≤ C * V.growth i x ^ p * w i x) : NativeJets V w f

Order-by-order bounds give one bound for each finite jet, with the constant still preceding the native label.

theorem NavierStokes.PrimaryCopyBounds.NativeJets.comp {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : JetDomain ι X} {v : ι → X → ℝ} {g : ι → X → E} (hg : NativeJets U v g) {χ : ι → D → X} (hχ : PhaseJetBounds.PolynomialJets V.toDomain χ) (hmap : ∀ (i : ι), Set.MapsTo (χ i) (V.carrier i) (U.carrier i)) (hG : ∀ (i : ι), ∀ x ∈ V.carrier i, U.growth i (χ i x) ≤ V.growth i x) : NativeJets V (fun (i : ι) (x : D) => v i (χ i x)) fun (i : ι) (x : D) => g i (χ i x)

Genuine chain-rule estimates with point-dependent edge growth.

The same-profile prepared construction

noncomputable def NavierStokes.PrimaryCopyBounds.leadingDomain {F₀ : OutgoingProfile.Profile} (W : NominalProfile.Witness F₀) (ι : Type u_5) : JetDomain ι SlowBorelBase.Inner

The full open active annulus, retaining the inverse edge distance.

Equations

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

theorem NavierStokes.PrimaryCopyBounds.leadingDomain_mem_annulus {ι : Type u_1} {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} (i : ι) {x : SlowBorelBase.Inner} (hx : x ∈ (leadingDomain W₀ ι).carrier i) : x ∈ FinalSlowBase.annulus W₀

theorem NavierStokes.PrimaryCopyBounds.leadingStress_nativeJets {ι : Type u_1} {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {ld : ModulatedProfileAssembly.LoopData W₀} (v₀ : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v₀) : NativeJets (leadingDomain W₀ ι) (fun (x : ι) => FinalSlowBase.weight W₀) fun (x : ι) => FinalSlowBase.leadingStress v₀

The native target estimate is derived from the actual constructed profile. The flat weight can approach zero at either edge.

theorem NavierStokes.PrimaryCopyBounds.actualTarget_jets {ι : Type u_1} {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {ld : ModulatedProfileAssembly.LoopData W₀} (v₀ : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v₀) (V : JetDomain ι PhaseCalculus.Slow) {r M qlo qhi : ℝ} (hr : 0 < r) (hqlo : 0 < qlo) (hgeom : BaseChartJets.GeometryBounds V.toDomain F₀.data.h r M qlo qhi (NominalConeAssembly.activeLeft W₀) (NominalConeAssembly.activeRight W₀)) (hedge : ∀ (i : ι), ∀ p ∈ V.carrier i, (FinalSlowBase.edgeDistance W₀ (BaseChartJets.normalizedCoordinates F₀.data.h p).2)⁻¹ ≤ V.growth i p) : NativeJets V (fun (x : ι) => PrimaryTargetBounds.movingWeight W₀) fun (x : ι) => PrimaryTargetBounds.actualTarget v₀

Actual normalized leading stress on a native slow domain, from only pointwise chart geometry and the inverse-edge growth comparison.

noncomputable def NavierStokes.PrimaryCopyBounds.preparedPrefactor {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} (r0 : ℝ) (vr vt : TorusInverse.Plane) {N : ℕ} (_j : Fin 2) (L : PrimaryGeometryAssembly.Index W₀ N) : ℝ

Prepared prefactor, constructed using PartitionedCovariance.nativePrefactor.

Equations

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

theorem NavierStokes.PrimaryCopyBounds.preparedPrefactor_eq {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} (r0 : ℝ) (vr vt : TorusInverse.Plane) {N : ℕ} (j : Fin 2) (L : PrimaryGeometryAssembly.Index W₀ N) : preparedPrefactor r0 vr vt j L = PartitionedCovariance.nativePrefactor vr vt r0 * (2 * r0)

theorem NavierStokes.PrimaryCopyBounds.preparedPrefactor_jets {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} (r0 : ℝ) (vr vt : TorusInverse.Plane) (N : ℕ) (j : Fin 2) : PhaseJetBounds.PolynomialJets (PrimaryGeometryAssembly.domain W₀ N) fun (L : PrimaryGeometryAssembly.Index W₀ N) (x : PrimaryGeometryAssembly.Slow) => preparedPrefactor r0 vr vt j L

theorem NavierStokes.PrimaryCopyBounds.exists_prepared_primary_jets {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} (H₀ : NominalConeAssembly.Certificate W₀) {ld : ModulatedProfileAssembly.LoopData W₀} (v₀ : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v₀) (upper : ℝ) (B : ℕ) (r0 : ℝ) (hr0 : 0 < r0) (hbox : 2 * NominalConeAssembly.activeRight W₀ ≤ FinalSlowBase.boxRadius W₀ upper) (N0 : ℕ) (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) : ∃ (a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0), ∀ (V : JetDomain (PrimaryGeometryAssembly.Index W₀ a.N) D) (χ : PrimaryGeometryAssembly.Index W₀ a.N → D → PhaseCalculus.Slow × ℝ) (mask : PrimaryGeometryAssembly.Index W₀ a.N → D → ℝ), (∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), (PrimaryGeometryAssembly.domain W₀ a.N).scale L = V.scale L) → PhaseJetBounds.PolynomialJets V.toDomain χ → (∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), ∀ x ∈ V.carrier L, χ L x ∈ (PrimaryGeometryAssembly.domain W₀ a.N).carrier L ×ˢ Set.Ioo 0 1) → (∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), ∀ x ∈ V.carrier L, (χ L x).1 ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W₀)) → (∀ (k : Fin 2), NativeJets V (fun (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) => PrimaryTargetBounds.movingWeight W₀ (χ L x).1) fun (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) => (PrimaryTargetBounds.actualTarget v₀ (χ L x).1).ofLp k) → PhaseJetBounds.PolynomialJets V.toDomain mask → (∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), ∀ x ∈ V.carrier L, 0 < PrimaryTargetBounds.movingWeight W₀ (χ L x).1) → ∀ (j : Fin 2), NativeJets V (fun (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) => √(ChartScales.epsilon F₀.data.h (BaseChartJets.cellBand L)) * (√(PrimaryTargetBounds.movingWeight W₀ (χ L x).1) * pulseEnvelope (PrimaryGeometryAssembly.construction H₀ v₀ a hr0) χ j L x)) (primaryVelocity (PrimaryGeometryAssembly.construction H₀ v₀ a hr0) (preparedPrefactor r0 vr vt) χ (fun (L : PrimaryGeometryAssembly.Index W₀ a.N) => ChartScales.epsilon F₀.data.h (BaseChartJets.cellBand L)) (fun (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) (k : Fin 2) => (PrimaryTargetBounds.actualTarget v₀ (χ L x).1).ofLp k) mask j)

The determinant, entry and inverse-weight constants are produced by the actual same-profile construction before the label and copy chart are chosen. The target is the literal leading stress of that same profile.

theorem NavierStokes.PrimaryCopyBounds.exists_prepared_pair_jets {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} (H₀ : NominalConeAssembly.Certificate W₀) {ld : ModulatedProfileAssembly.LoopData W₀} (v₀ : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v₀) (upper : ℝ) (B : ℕ) (r0 : ℝ) (hr0 : 0 < r0) (hbox : 2 * NominalConeAssembly.activeRight W₀ ≤ FinalSlowBase.boxRadius W₀ upper) (N0 : ℕ) (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) : ∃ (a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0), ∀ (V : JetDomain (PrimaryGeometryAssembly.Index W₀ a.N) D) (S : JetDomain (PrimaryGeometryAssembly.Index W₀ a.N) PhaseCalculus.Slow) (χ : PrimaryGeometryAssembly.Index W₀ a.N → D → PhaseCalculus.Slow × ℝ) (mask : PrimaryGeometryAssembly.Index W₀ a.N → D → ℝ) (r M qlo qhi : ℝ), (∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), (PrimaryGeometryAssembly.domain W₀ a.N).scale L = V.scale L) → PhaseJetBounds.PolynomialJets V.toDomain χ → (∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), ∀ x ∈ V.carrier L, χ L x ∈ (PrimaryGeometryAssembly.domain W₀ a.N).carrier L ×ˢ Set.Ioo 0 1) → (∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), ∀ x ∈ V.carrier L, (χ L x).1 ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W₀)) → (∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), ∀ x ∈ V.carrier L, (χ L x).1 ∈ S.carrier L) → (∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), ∀ x ∈ V.carrier L, S.growth L (χ L x).1 ≤ V.growth L x) → 0 < r → 0 < qlo → BaseChartJets.GeometryBounds S.toDomain F₀.data.h r M qlo qhi (NominalConeAssembly.activeLeft W₀) (NominalConeAssembly.activeRight W₀) → (∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), ∀ p ∈ S.carrier L, (FinalSlowBase.edgeDistance W₀ (BaseChartJets.normalizedCoordinates F₀.data.h p).2)⁻¹ ≤ S.growth L p) → PhaseJetBounds.PolynomialJets V.toDomain mask → ∀ (j : Fin 2), have ε := fun (L : PrimaryGeometryAssembly.Index W₀ a.N) => ChartScales.epsilon F₀.data.h (BaseChartJets.cellBand L); have F := PrimaryGeometryAssembly.construction H₀ v₀ a hr0; have u := primaryVelocity F (preparedPrefactor r0 vr vt) χ ε (fun (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) (k : Fin 2) => (PrimaryTargetBounds.actualTarget v₀ (χ L x).1).ofLp k) mask j; have w := fun (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) => √(PrimaryTargetBounds.movingWeight W₀ (χ L x).1) * pulseEnvelope F χ j L x; NativeJets V (fun (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) => √(ε L) * w L x) u ∧ NativeJets V (fun (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) => ε L * w L x) (phasePressure (F j) χ (fun (L : PrimaryGeometryAssembly.Index W₀ a.N) => ↑(ChartScales.carrier F₀.data.h (BaseChartJets.cellBand L))) u)

The final native primary estimate has no target-jet premise: the actual leading target is pulled back from its proved profile estimates. The remaining chart hypotheses are pointwise geometry and polynomial jets of the primitive coordinate map and scalar mask.

Actual slow-mask jets and zero germs

noncomputable def NavierStokes.PrimaryCopyBounds.positionCLM : PhaseCalculus.Slow →L[ℝ] SlotColoring.Position

Position continuous linear map, constructed using LinearMap.toContinuousLinearMap.

Equations

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

theorem NavierStokes.PrimaryCopyBounds.norm_positionCLM_le : ‖positionCLM‖ ≤ 1

theorem NavierStokes.PrimaryCopyBounds.nativeMask_jets {ι : Type u_1} (U : PhaseJetBounds.Domain ι PhaseCalculus.Slow) (band : ι → ℕ) (grid : ι → SlotColoring.Grid) (hband : ∀ (i : ι), 1 ≤ band i) (hscale : ∀ (i : ι), U.scale i = ChartScales.S (band i)) : PhaseJetBounds.PolynomialJets U fun (i : ι) => PrimaryRepresentatives.nativeMask (band i) (grid i)

All derivatives of the actual squared-partition mask have uniform polynomial bounds, including every grid node.

theorem NavierStokes.PrimaryCopyBounds.nativeMask_comp_jets {ι : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : PhaseJetBounds.Domain ι D) (χ : ι → D → PhaseCalculus.Slow) (hχ : PhaseJetBounds.PolynomialJets U χ) (band : ι → ℕ) (grid : ι → SlotColoring.Grid) (hband : ∀ (i : ι), 1 ≤ band i) (hscale : ∀ (i : ι), U.scale i = ChartScales.S (band i)) : PhaseJetBounds.PolynomialJets U fun (i : ι) (x : D) => PrimaryRepresentatives.nativeMask (band i) (grid i) (χ i x)

theorem NavierStokes.PrimaryCopyBounds.preparedMask_zero_germ {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {N : ℕ} (L : PrimaryGeometryAssembly.Index W₀ N) {p : PhaseCalculus.Slow} (hT : 0 < p.2.2) (hout : p ∉ (PrimaryGeometryAssembly.domain W₀ N).carrier L) : PrimaryRepresentatives.nativeMask (PrimaryGeometryAssembly.label W₀ L).1 (PrimaryGeometryAssembly.label W₀ L).2 =ᶠ[nhds p] fun (x : PhaseCalculus.Slow) => 0

Off the actual label's enlarged slow cell, its mask has a zero germ. This is the extension fact needed before applying whole-torus copy bounds.

theorem NavierStokes.PrimaryCopyBounds.NativeJets.prepared_mask_outer_localize {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {N : ℕ} {V V' : JetDomain (PrimaryGeometryAssembly.Index W₀ N) D} {w : PrimaryGeometryAssembly.Index W₀ N → D → ℝ} {f : PrimaryGeometryAssembly.Index W₀ N → D → E} (hf : NativeJets V w f) (χ : PrimaryGeometryAssembly.Index W₀ N → D → PhaseCalculus.Slow) (hχ : PhaseJetBounds.PolynomialJets V'.toDomain χ) (hscaleBand : ∀ (L : PrimaryGeometryAssembly.Index W₀ N), V'.scale L = ChartScales.S (PrimaryGeometryAssembly.label W₀ L).1) (hT : ∀ (L : PrimaryGeometryAssembly.Index W₀ N), ∀ x ∈ V'.carrier L, 0 < (χ L x).2.2) (τ : PrimaryGeometryAssembly.Index W₀ N → D →L[ℝ] ℝ) (t0 : PrimaryGeometryAssembly.Index W₀ N → ℝ) {K : ℝ} (hK : 1 ≤ K) (q : ℕ) (hτ : ∀ (L : PrimaryGeometryAssembly.Index W₀ N), ‖τ L‖ ≤ K * V'.scale L ^ q) (hscale : ∀ (L : PrimaryGeometryAssembly.Index W₀ N), V'.scale L = V.scale L) (hsub : ∀ (L : PrimaryGeometryAssembly.Index W₀ N), V.carrier L ⊆ V'.carrier L) (hgrowth : ∀ (L : PrimaryGeometryAssembly.Index W₀ N), ∀ x ∈ V.carrier L, V.growth L x = V'.growth L x) (hinside : ∀ (L : PrimaryGeometryAssembly.Index W₀ N), ∀ x ∈ V'.carrier L, χ L x ∈ (PrimaryGeometryAssembly.domain W₀ N).carrier L → (τ L) x + t0 L ∈ Set.Ioo 0 1 → x ∈ V.carrier L) (hw : ∀ (L : PrimaryGeometryAssembly.Index W₀ N), ∀ x ∈ V'.carrier L, 0 ≤ w L x) : NativeJets V' w fun (L : PrimaryGeometryAssembly.Index W₀ N) (x : D) => (PrimaryRepresentatives.nativeMask (PrimaryGeometryAssembly.label W₀ L).1 (PrimaryGeometryAssembly.label W₀ L).2 (χ L x) * outerCutoff ((τ L) x + t0 L)) • f L x

The actual slow mask and actual outer bump extend a native field to the whole larger chart. Off its own cell it is locally zero, including all slow-mask and slot-cutoff derivatives.

The two orientations share one family of constants

noncomputable def NavierStokes.PrimaryCopyBounds.signDomain {ι : Type u_1} {D : Type} [NormedAddCommGroup D] (V : JetDomain ι D) : JetDomain (Fin 2 × ι) D

Sign domain, bundling carrier, isOpen, scale, one_le_scale and the required compatibility proofs.

Equations

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

theorem NavierStokes.PrimaryCopyBounds.NativeJets.both_signs {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : JetDomain ι D} {w : Fin 2 → ι → D → ℝ} {f : Fin 2 → ι → D → E} (hf : ∀ (j : Fin 2), NativeJets V (w j) (f j)) : NativeJets (signDomain V) (fun (i : Fin 2 × ι) => w i.1 i.2) fun (i : Fin 2 × ι) => f i.1 i.2

The actual common-cover copy map

noncomputable def NavierStokes.PrimaryCopyBounds.nativePointLinear {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) : P × TorusInverse.Plane →L[ℝ] P × TorusInverse.Plane

Native point linear, given by (ContinuousLinearMap.fst ℝ P TorusInverse.Plane).prod (g.coordinateLinear.comp (ContinuousLinearMap.snd ℝ P TorusInverse.Plane)).

Equations

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

theorem NavierStokes.PrimaryCopyBounds.nativePoint_affine {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : ParticularWaveBounds.nativePoint g k x = (nativePointLinear g) x + ParticularWaveBounds.nativePoint g k 0

theorem NavierStokes.PrimaryCopyBounds.norm_nativePointLinear_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) : ‖nativePointLinear g‖ ≤ CommonCoverClass.argumentCost g

theorem NavierStokes.PrimaryCopyBounds.nativePointLinear_band_bound {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) {n gap Δ : ℕ} (hn : 4 ≤ n) (hgap : gap ≤ Δ) (center : TorusInverse.Plane) : ‖nativePointLinear (CommonCoverClass.bandGeometry B h n gap center)‖ ≤ CommonCoverClass.bandArgumentCost B Δ * ChartScales.S n

For the actual band basis, the affine derivative cost is uniform in the center and lattice translation.

theorem NavierStokes.PrimaryCopyBounds.NativeJets.native_copy_localJets {ι : Type u_1} {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [NormedSpace ℝ H] {Λ : Type u_5} {V : JetDomain ι (P × TorusInverse.Plane)} {w : ι → P × TorusInverse.Plane → ℝ} {f : ι → P × TorusInverse.Plane → H} (hf : NativeJets V w f) (s : WeightedClasses.StripData (P × TorusInverse.Plane)) (W : Λ → ℕ → P × TorusInverse.Plane → ℝ) (α : ℝ) (index : Λ → ℕ → ι) (g : Λ → ℕ → CommonCoverSolve.Geometry) (Ω : Λ → ℕ → Set TorusInverse.Plane) (hW : ∀ (l : Λ) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hmap : ∀ (l : Λ) (n : ℕ) (k : TorusInverse.Frequency), ∀ x ∈ s.domain, (g l n).coordinates k x.2 ∈ Ω l n → ParticularWaveBounds.nativePoint (g l n) k x ∈ V.carrier (index l n)) {A B : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (a b : ℕ) (hgrowth : ∀ (l : Λ) (n : ℕ) (k : TorusInverse.Frequency), ∀ x ∈ s.domain, (g l n).coordinates k x.2 ∈ Ω l n → V.growth (index l n) (ParticularWaveBounds.nativePoint (g l n) k x) ≤ A * s.growth n x ^ a) (hgeometry : ∀ (l : Λ) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ B * s.slow n ^ b) (hweight : ∀ (l : Λ) (n : ℕ) (k : TorusInverse.Frequency), ∀ x ∈ s.domain, (g l n).coordinates k x.2 ∈ Ω l n → w (index l n) (ParticularWaveBounds.nativePoint (g l n) k x) ≤ s.epsilon n ^ α * W l n x) : PeriodizedWaveBounds.UniformLocalJets s W α (fun (l : Λ) (n : ℕ) => PeriodizedWaveBounds.nativeCell (g l n) (Ω l n)) fun (l : Λ) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) => f (index l n) (ParticularWaveBounds.nativePoint (g l n) k x)

theorem NavierStokes.PrimaryCopyBounds.NativeJets.native_copy_sum_uniformClass {ι : Type u_1} {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [NormedSpace ℝ H] {Λ : Type u_5} {V : JetDomain ι (P × TorusInverse.Plane)} {w : ι → P × TorusInverse.Plane → ℝ} {f : ι → P × TorusInverse.Plane → H} (hf : NativeJets V w f) (s : WeightedClasses.StripData (P × TorusInverse.Plane)) (W : Λ → ℕ → P × TorusInverse.Plane → ℝ) (α : ℝ) (index : Λ → ℕ → ι) (g : Λ → ℕ → CommonCoverSolve.Geometry) (Ω : Λ → ℕ → Set TorusInverse.Plane) (hcompact : ∀ (l : Λ) (n : ℕ), IsCompact (Ω l n)) (hinj : ∀ (l : Λ) (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (g l n).center + (g l n).basis z) '' Ω l n)) (κ : ι → TorusInverse.Plane → ℝ) (hκ : PhaseJetBounds.PolynomialJets V.toDomain fun (i : ι) (x : P × TorusInverse.Plane) => κ i x.2) (hcut : ∀ (l : Λ) (n : ℕ), Function.support (κ (index l n)) ⊆ Ω l n) (hW : ∀ (l : Λ) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hmap : ∀ (l : Λ) (n : ℕ) (k : TorusInverse.Frequency), ∀ x ∈ s.domain, (g l n).coordinates k x.2 ∈ Ω l n → ParticularWaveBounds.nativePoint (g l n) k x ∈ V.carrier (index l n)) {A B : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (a b : ℕ) (hgrowth : ∀ (l : Λ) (n : ℕ) (k : TorusInverse.Frequency), ∀ x ∈ s.domain, (g l n).coordinates k x.2 ∈ Ω l n → V.growth (index l n) (ParticularWaveBounds.nativePoint (g l n) k x) ≤ A * s.growth n x ^ a) (hgeometry : ∀ (l : Λ) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ B * s.slow n ^ b) (hweight : ∀ (l : Λ) (n : ℕ) (k : TorusInverse.Frequency), ∀ x ∈ s.domain, (g l n).coordinates k x.2 ∈ Ω l n → w (index l n) (ParticularWaveBounds.nativePoint (g l n) k x) ≤ s.epsilon n ^ α * W l n x) : LabelSumBounds.UniformClass s W α fun (l : Λ) (n : ℕ) => ParticularWaveBounds.periodizedCopies (g l n) (κ (index l n)) fun (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) => f (index l n) (ParticularWaveBounds.nativePoint (g l n) k x)

The constructed native field is periodized over the genuine covering lattice. Support is proved from the scalar cutoff, and the native cells are constructed from compactness and injectivity of that patch.