Weighted bounds for the actual primary pulses

The homogeneous ODE is reparametrized onto a fixed unit interval. Its current endpoint becomes an additional parameter, so the weighted ODE jet estimate controls actual joint parameter and slot derivatives.

noncomputable def NavierStokes.PrimaryPulseBounds.timeLinear {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (σ : ℝ) : Q × ℝ →L[ℝ] Q × ℝ

Time linear, given by (ContinuousLinearMap.fst ℝ Q ℝ).prod (σ • ContinuousLinearMap.snd ℝ Q ℝ).

Equations

• NavierStokes.PrimaryPulseBounds.timeLinear σ = (ContinuousLinearMap.fst ℝ Q ℝ).prod (σ • ContinuousLinearMap.snd ℝ Q ℝ)

@[simp]

theorem NavierStokes.PrimaryPulseBounds.timeLinear_apply {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (σ : ℝ) (z : Q × ℝ) : (timeLinear σ) z = (z.1, σ * z.2)

theorem NavierStokes.PrimaryPulseBounds.timeLinear_norm_le {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {σ : ℝ} (hσ : |σ| ≤ 1) : ‖timeLinear σ‖ ≤ 1

theorem NavierStokes.PrimaryPulseBounds.norm_jet_slot_coordinate {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (z : Q × ℝ) (j : ℕ) : ‖iteratedFDeriv ℝ j (fun (y : Q × ℝ) => y.2) z‖ ≤ max 1 |z.2|

theorem NavierStokes.PrimaryPulseBounds.norm_lsmul_le_one {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] : ‖ContinuousLinearMap.lsmul ℝ ℝ‖ ≤ 1

theorem NavierStokes.PrimaryPulseBounds.smul_jet_bound {Q E : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup E] [NormedSpace ℝ E] {A : Q → ℝ} {B : Q → E} {U : Set Q} (hU : IsOpen U) (hA : ContDiffOn ℝ (↑⊤) A U) (hB : ContDiffOn ℝ (↑⊤) B U) {x : Q} (hx : x ∈ U) {N j : ℕ} (hj : j ≤ N) {C D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D) (ha : ∀ i ≤ N, ‖iteratedFDeriv ℝ i A x‖ ≤ C) (hb : ∀ i ≤ N, ‖iteratedFDeriv ℝ i B x‖ ≤ D) : ‖iteratedFDeriv ℝ j (fun (y : Q) => A y • B y) x‖ ≤ 2 ^ N * C * D

Pointwise higher Leibniz bound. The right-hand bounds may be frozen weights at this point, so no derivative of a majorant is introduced.

theorem NavierStokes.PrimaryPulseBounds.rescale_jet_bound {Q E : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup E] [NormedSpace ℝ E] {A : Q × ℝ → E} {U : Set (Q × ℝ)} (hU : IsOpen U) (hA : ContDiffOn ℝ (↑⊤) A U) {z : Q × ℝ} {σ C T : ℝ} (hσ : |σ| ≤ 1) (hz : (timeLinear σ) z ∈ U) (hC : 0 ≤ C) (hT : 1 ≤ T) (ht : |z.2| ≤ T) {N j : ℕ} (hj : j ≤ N) (hjet : ∀ i ≤ N, ‖iteratedFDeriv ℝ i A ((timeLinear σ) z)‖ ≤ C) : ‖iteratedFDeriv ℝ j (fun (y : Q × ℝ) => y.2 • A (y.1, σ * y.2)) z‖ ≤ 2 ^ N * T * C

All derivatives of the rescaled coefficient, including derivatives of its endpoint prefactor, follow from the original joint coefficient jets.

noncomputable def NavierStokes.PrimaryPulseBounds.rescaleConstant (N : ℕ) (K : ℝ) : ℝ

Rescale constant, given by 2 ^ N * K ^ 2 + K + 1.

Equations

• NavierStokes.PrimaryPulseBounds.rescaleConstant N K = 2 ^ N * K ^ 2 + K + 1

theorem NavierStokes.PrimaryPulseBounds.le_rescaleConstant (N : ℕ) (K : ℝ) : K ≤ rescaleConstant N K

theorem NavierStokes.PrimaryPulseBounds.homogeneous_joint_jet_bound {Q H : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {L S K μ : ℝ} (_hL : 0 < L) (hS : 1 ≤ S) (hK : 1 ≤ K) (hμ : 0 ≤ μ) (hslot : L ≤ K * S) (hExp : Real.exp (μ * L) ≤ K) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc 0 L ⊆ V) (A : Q × ℝ → H →L[ℝ] H) (hA : ContDiffOn ℝ (↑⊤) A (U ×ˢ V)) (P rate : ℝ → ℝ) (hP : ∀ (t : ℝ), 0 < P t) (hdP : ∀ (t : ℝ), HasDerivAt P (rate t * P t) t) (e : H) (he : ‖e‖ ≤ 1) {p : Q} (hp : p ∈ U) {t : ℝ} (ht : t ∈ Set.Icc 0 L) (henergy : ∀ v ∈ Set.Icc 0 L, ∀ (x : H), inner ℝ x ((A (p, v)) x) ≤ (rate v + μ) * ‖x‖ ^ 2) (m N : ℕ) (hjets : ∀ j ≤ N, ∀ v ∈ Set.Icc 0 L, ‖iteratedFDeriv ℝ j A (p, v)‖ ≤ K * S ^ m) (j : ℕ) (hj : j ≤ N) : ‖iteratedFDeriv ℝ j (JointODE.reparamSolution 0 A (fun (x : Q) => P 0 • e) fun (x : Q × ℝ) => 0) (p, t)‖ ≤ (2 ^ (N + 1) * rescaleConstant N K ^ 3) ^ (j + 1) * S ^ ((m + 2) * (j + 1)) * P t

Actual joint derivatives of a homogeneous fundamental solution retain the reference envelope. The solution is the constructed Volterra solution in JointODE, rather than an assumed smooth solution family.

structure NavierStokes.PrimaryPulseBounds.EnvelopeJets {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (D : PhaseJetBounds.Domain ι E) (w : ι → E → ℝ) (f : ι → E → F) : Prop

Polynomial jets with a retained pointwise envelope. This is only an intermediate family predicate; the constructed solution is proved to satisfy it.

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

noncomputable def NavierStokes.PrimaryPulseBounds.productDomain {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (D : PhaseJetBounds.Domain ι E) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) : PhaseJetBounds.Domain ι (E × ℝ)

Product domain, bundling scale, carrier, isOpen, one_le_scale.

Equations

• NavierStokes.PrimaryPulseBounds.productDomain D V hV = { scale := D.scale, carrier := fun (i : ι) => D.carrier i ×ˢ V i, isOpen := ⋯, one_le_scale := ⋯ }

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.comp {ι : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {D : PhaseJetBounds.Domain ι E} {D' : PhaseJetBounds.Domain ι F} {f : ι → F → G} {w : ι → F → ℝ} (hf : EnvelopeJets D' w f) {g : ι → E → F} (hg : PhaseJetBounds.PolynomialJets D g) (hscale : ∀ (i : ι), D'.scale i = D.scale i) (hmap : ∀ (i : ι), Set.MapsTo (g i) (D.carrier i) (D'.carrier i)) : EnvelopeJets D (fun (i : ι) (x : E) => w i (g i x)) fun (i : ι) (x : E) => f i (g i x)

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.of_polynomial {ι : Type u_1} {E : Type u_2} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {D : PhaseJetBounds.Domain ι E} {f : ι → E → G} (hf : PhaseJetBounds.PolynomialJets D f) : EnvelopeJets D (fun (x : ι) (x_1 : E) => 1) f

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.to_polynomial {ι : Type u_1} {E : Type u_2} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {D : PhaseJetBounds.Domain ι E} {w : ι → E → ℝ} {f : ι → E → G} (hf : EnvelopeJets D w f) (hw : ∀ (i : ι), ∀ x ∈ D.carrier i, w i x ≤ 1) : PhaseJetBounds.PolynomialJets D f

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.precomp_linear {ι : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {D : PhaseJetBounds.Domain ι E} {D' : PhaseJetBounds.Domain ι F} {f : ι → F → G} {w : ι → F → ℝ} (hf : EnvelopeJets D' w f) (L : ι → E →L[ℝ] F) (hscale : ∀ (i : ι), D'.scale i = D.scale i) (hmap : ∀ (i : ι), Set.MapsTo (⇑(L i)) (D.carrier i) (D'.carrier i)) {C : ℝ} {k : ℕ} (hC : 1 ≤ C) (hL : ∀ (i : ι), ‖L i‖ ≤ C * D.scale i ^ k) : EnvelopeJets D (fun (i : ι) (x : E) => w i ((L i) x)) fun (i : ι) (x : E) => f i ((L i) x)

noncomputable def NavierStokes.PrimaryPulseBounds.phaseDomain {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) : PhaseJetBounds.Domain ℕ E

Phase domain, bundling scale, carrier, isOpen, one_le_scale.

Equations

• NavierStokes.PrimaryPulseBounds.phaseDomain s = { scale := s.slow, carrier := fun (x : ℕ) => s.domain, isOpen := ⋯, one_le_scale := ⋯ }

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.memClass {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : PhaseJetBounds.Domain ℕ E} {w : ℕ → E → ℝ} {f : ℕ → E → F} (hf : EnvelopeJets D w f) (s : WeightedClasses.StripData E) (hscale : ∀ (n : ℕ), D.scale n = s.slow n) (hdom : ∀ (n : ℕ), D.carrier n = s.domain) : WeightedClasses.MemClass s w 0 f

theorem NavierStokes.PrimaryPulseBounds.polynomial_memClass {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (s : WeightedClasses.StripData E) {f : ℕ → E → F} (hf : PhaseJetBounds.PolynomialJets (phaseDomain s) f) : WeightedClasses.UnweightedClass s 0 f

theorem NavierStokes.PrimaryPulseBounds.homogeneous_family_envelope_jets {ι : Type u_1} {Q H : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : PhaseJetBounds.Domain ι Q) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) (L μ : ι → ℝ) (hL : ∀ (i : ι), 0 < L i) (hI : ∀ (i : ι), Set.Icc 0 (L i) ⊆ V i) (A : ι → Q × ℝ → H →L[ℝ] H) (hA : PhaseJetBounds.PolynomialJets (productDomain D V hV) A) (P rate : ι → ℝ → ℝ) (hP : ∀ (i : ι) (t : ℝ), 0 < P i t) (hdP : ∀ (i : ι) (t : ℝ), HasDerivAt (P i) (rate i t * P i t) t) (e : H) (he : ‖e‖ ≤ 1) {K₀ : ℝ} (hK₀ : 1 ≤ K₀) (hμ : ∀ (i : ι), 0 ≤ μ i) (hslot : ∀ (i : ι), L i ≤ K₀ * D.scale i) (hExp : ∀ (i : ι), Real.exp (μ i * L i) ≤ K₀) (henergy : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), ∀ (x : H), inner ℝ x ((A i (p, v)) x) ≤ (rate i v + μ i) * ‖x‖ ^ 2) : EnvelopeJets (productDomain D (fun (i : ι) => Set.Ioo 0 (L i)) ⋯) (fun (i : ι) (z : Q × ℝ) => P i z.2) fun (i : ι) => JointODE.reparamSolution 0 (A i) (fun (x : Q) => P i 0 • e) fun (x : Q × ℝ) => 0

Every fixed joint jet of the actual homogeneous family has a single band-uniform polynomial bound times the original reference envelope.

theorem NavierStokes.PrimaryPulseBounds.pathFamily_polynomial {ι : Type u_1} {Q H : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup H] [NormedSpace ℝ H] (D : PhaseJetBounds.Domain ι Q) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) {a b : ℝ} (hI : ∀ (i : ι), Set.Icc a b ⊆ V i) {F : ι → Q × ℝ → H} (hF : PhaseJetBounds.PolynomialJets (productDomain D V hV) F) : PhaseJetBounds.PolynomialJets D fun (i : ι) => SmoothPathFamily.pathFamily (F i)

Joint coefficient jets control the actual continuous-path jets in the supremum norm, uniformly on a fixed compact integration interval.

noncomputable def NavierStokes.PrimaryPulseBounds.intervalIntegralCLM {H : Type} [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] {a b : ℝ} (hab : a ≤ b) : C(↑(Set.Icc a b), H) →L[ℝ] H

Interval integral continuous linear map, given by (ContinuousMap.evalCLM ℝ (⟨b, hab, le_rfl⟩ : Icc a b)).comp (ParametricODE.integrator hab).

Equations

• NavierStokes.PrimaryPulseBounds.intervalIntegralCLM hab = ContinuousMap.evalCLM ℝ ⟨b, ⋯⟩ ∘SL NavierStokes.ParametricODE.integrator hab

theorem NavierStokes.PrimaryPulseBounds.intervalIntegral_polynomial {ι : Type u_1} {Q H : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] (D : PhaseJetBounds.Domain ι Q) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) {a b : ℝ} (hab : a ≤ b) (hI : ∀ (i : ι), Set.Icc a b ⊆ V i) {F : ι → Q × ℝ → H} (hF : PhaseJetBounds.PolynomialJets (productDomain D V hV) F) : PhaseJetBounds.PolynomialJets D fun (i : ι) (p : Q) => ∫ (t : ℝ) in a..b, F i (p, t)

The actual parameter-dependent integral has polynomial jets; no smoothness or derivative estimate for the integral is an input.

@[reducible, inline]

abbrev NavierStokes.PrimaryPulseBounds.State : Type

State: an abbreviation for MovingFrameODE.Plane.

Equations

• NavierStokes.PrimaryPulseBounds.State = NavierStokes.MovingFrameODE.Plane

@[reducible, inline]

abbrev NavierStokes.PrimaryPulseBounds.Space : Type

Space: an abbreviation for MovingFrameODE.Space.

Equations

• NavierStokes.PrimaryPulseBounds.Space = NavierStokes.MovingFrameODE.Space

noncomputable def NavierStokes.PrimaryPulseBounds.positiveSeed : State

Positive seed, given by !₂[1, 0].

Equations

• NavierStokes.PrimaryPulseBounds.positiveSeed = !₂[1, 0]

theorem NavierStokes.PrimaryPulseBounds.positiveSeed_norm : ‖positiveSeed‖ = 1

noncomputable def NavierStokes.PrimaryPulseBounds.referenceP (lam u L t : ℝ) : ℝ

Reference P, given by GaussianEnvelope.envelope (GaussianEnvelope.referenceRate lam u L) (L / 2) t.

Equations

• NavierStokes.PrimaryPulseBounds.referenceP lam u L t = NavierStokes.GaussianEnvelope.envelope (NavierStokes.GaussianEnvelope.referenceRate lam u L) (L / 2) t

theorem NavierStokes.PrimaryPulseBounds.referenceP_pos (lam u L t : ℝ) : 0 < referenceP lam u L t

theorem NavierStokes.PrimaryPulseBounds.referenceP_hasDerivAt (lam u L t : ℝ) : HasDerivAt (referenceP lam u L) (GaussianEnvelope.referenceRate lam u L t * referenceP lam u L t) t

theorem NavierStokes.PrimaryPulseBounds.referenceP_le_one {lam u L t : ℝ} (hlam : 0 < lam) (hu : 0 < u) (hL : 0 < L) (ht : t ∈ Set.Icc 0 L) : referenceP lam u L t ≤ 1

noncomputable def NavierStokes.PrimaryPulseBounds.fundamental {Q : Type} (d : PrimaryODE.FrameData Q) (lam u L : ℝ) : Q × ℝ → State

Fundamental, given by JointODE.reparamSolution 0 (d.coefficient 1) (fun _ => referenceP lam u L 0 • positiveSeed) (fun _ => 0).

Equations

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

theorem NavierStokes.PrimaryPulseBounds.fundamental_envelope_jets {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (D : PhaseJetBounds.Domain ι Q) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) (d : ι → PrimaryODE.FrameData Q) (hd : PhaseJetBounds.FrameJets (productDomain D V hV) d) (lam u L : ι → ℝ) (hlam : ∀ (i : ι), 0 < lam i) (_hu : ∀ (i : ι), 0 < u i) (hL : ∀ (i : ι), 0 < L i) (hI : ∀ (i : ι), Set.Icc 0 (L i) ⊆ V i) {M C B : ℝ} (hM : 1 ≤ M) (hC : 0 ≤ C) (hB : 0 ≤ B) (hslot : ∀ (i : ι), L i ≤ M * D.scale i) (heigen : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), (d i).eigenvalue (p, v) = ViscousPropagator.referenceEigenvalue (lam i) (u i) (L i) v) (hν : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), 0 ≤ (d i).viscosity (p, v)) (hνerr : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), ViscousPropagator.referenceViscosity (lam i) (u i) (L i) v - B / D.scale i ≤ (d i).viscosity (p, v)) (herr : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), |(d i).error11 (p, v)| ≤ C / D.scale i ∧ |(d i).error12 (p, v)| ≤ C / D.scale i ∧ |(d i).error21 (p, v)| ≤ C / D.scale i ∧ |(d i).error22 (p, v)| ≤ C / D.scale i) : EnvelopeJets (productDomain D (fun (i : ι) => Set.Ioo 0 (L i)) ⋯) (fun (i : ι) (z : Q × ℝ) => referenceP (lam i) (u i) (L i) z.2) fun (i : ι) => fundamental (d i) (lam i) (u i) (L i)

The phase-derived coefficient jets are applied to the actual growing fundamental, with its actual viscosity and four moving-basis errors.

theorem NavierStokes.PrimaryPulseBounds.fundamental_eq_primary {Q : Type} [NormedAddCommGroup Q] {d : PrimaryODE.FrameData Q} {lam u L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) {p : Q} (hp : p ∈ U) {t : ℝ} (ht : t ∈ Set.Icc 0 L) : fundamental d lam u L (p, t) = PrimaryODE.primary ⋯ d (fun (z : Q × ℝ) => referenceP lam u L z.2) p t

theorem NavierStokes.PrimaryPulseBounds.timeLinear_norm_le_max {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (t : ℝ) : ‖timeLinear t‖ ≤ max 1 |t|

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.normalize_slot {ι : Type u_1} {Q H : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup H] [NormedSpace ℝ H] (D : PhaseJetBounds.Domain ι Q) (L : ι → ℝ) (hL : ∀ (i : ι), 0 < L i) {w : ι → Q × ℝ → ℝ} {f : ι → Q × ℝ → H} (hf : EnvelopeJets (productDomain D (fun (i : ι) => Set.Ioo 0 (L i)) ⋯) w f) {M : ℝ} (hM : 1 ≤ M) (hslot : ∀ (i : ι), L i ≤ M * D.scale i) : EnvelopeJets (productDomain D (fun (x : ι) => Set.Ioo 0 1) ⋯) (fun (i : ι) (z : Q × ℝ) => w i (z.1, L i * z.2)) fun (i : ι) (z : Q × ℝ) => f i (z.1, L i * z.2)

Changing v to Lθ costs polynomial factors only and preserves the exact Gaussian weight at v=Lθ.

noncomputable def NavierStokes.PrimaryPulseBounds.synthesisColumn {Q : Type} (d : PrimaryODE.FrameData Q) (j : Fin 2) (z : Q × ℝ) : Space

Synthesis column, given by MovingFrameODE.pack 1 ((-d.rho z) • d.frame z 0 + (if j = 0 then d.eigenvector z else -d.eigenvector z) • d.frame z 1).

Equations

• NavierStokes.PrimaryPulseBounds.synthesisColumn d j z = NavierStokes.MovingFrameODE.pack 1 (-d.rho z • (d.frame z) 0 + (if j = 0 then d.eigenvector z else -d.eigenvector z) • (d.frame z) 1)

theorem NavierStokes.PrimaryPulseBounds.ambient_eq_synthesis {Q : Type} (d : PrimaryODE.FrameData Q) (z : Q × ℝ) (w : State) : d.ambient z w = w.ofLp 0 • synthesisColumn d 0 z + w.ofLp 1 • synthesisColumn d 1 z

theorem NavierStokes.PrimaryPulseBounds.synthesisColumn_polynomial {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : PhaseJetBounds.Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (hd : PhaseJetBounds.FrameJets D d) (j : Fin 2) : PhaseJetBounds.PolynomialJets D fun (i : ι) => synthesisColumn (d i) j

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.restrict {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D D' : PhaseJetBounds.Domain ι E} {w : ι → E → ℝ} {f : ι → E → F} (hf : EnvelopeJets D w f) (hscale : ∀ (i : ι), D.scale i = D'.scale i) (hsub : ∀ (i : ι), D'.carrier i ⊆ D.carrier i) : EnvelopeJets D' w f

theorem NavierStokes.PrimaryPulseBounds.polynomial_memClass_of_domain {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : PhaseJetBounds.Domain ℕ E} {f : ℕ → E → F} (hf : PhaseJetBounds.PolynomialJets D f) (s : WeightedClasses.StripData E) (hscale : ∀ (i : ℕ), D.scale i = s.slow i) (hdom : ∀ (i : ℕ), D.carrier i = s.domain) : WeightedClasses.UnweightedClass s 0 f

theorem NavierStokes.PrimaryPulseBounds.synthesis_memClass {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {s : WeightedClasses.StripData (Q × ℝ)} {P : ℕ → Q × ℝ → ℝ} {c : Fin 2 → ℕ → Q × ℝ → Space} {z : ℕ → Q × ℝ → State} (hc : ∀ (j : Fin 2), WeightedClasses.UnweightedClass s 0 (c j)) (hz : WeightedClasses.MemClass s P 0 z) : WeightedClasses.MemClass s P 0 fun (n : ℕ) (x : Q × ℝ) => (z n x).ofLp 0 • c 0 n x + (z n x).ofLp 1 • c 1 n x

noncomputable def NavierStokes.PrimaryPulseBounds.covarianceMatrix {ι : Type u_1} {Q : Type} (a b : ℝ) (pref : Fin 2 → ι → ℝ) (ψ : Fin 2 → ι → Q × ℝ → ℝ) (v : Fin 2 → ι → Q × ℝ → Space) (n : ι) (p : Q) : SmoothCovariance.Mat2

The two actual normalized-slot integrals making up each covariance column. The prefactor includes the native Haar factor and ci times L.

Equations

• NavierStokes.PrimaryPulseBounds.covarianceMatrix a b pref ψ v n p r c = pref c n * ∫ (t : ℝ) in a..b, ψ c n (p, t) ^ 2 * ((v c n (p, t)).ofLp 0 * (v c n (p, t)).ofLp r.succ)

theorem NavierStokes.PrimaryPulseBounds.covarianceMatrix_entry_polynomial {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (D : PhaseJetBounds.Domain ι Q) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) {a b : ℝ} (hab : a ≤ b) (hI : ∀ (i : ι), Set.Icc a b ⊆ V i) {pref : Fin 2 → ι → ℝ} {ψ : Fin 2 → ι → Q × ℝ → ℝ} {v : Fin 2 → ι → Q × ℝ → Space} (hpref : ∀ (c : Fin 2), PhaseJetBounds.PolynomialJets D fun (n : ι) (x : Q) => pref c n) (hψ : ∀ (c : Fin 2), PhaseJetBounds.PolynomialJets (productDomain D V hV) (ψ c)) (hv : ∀ (c : Fin 2), PhaseJetBounds.PolynomialJets (productDomain D V hV) (v c)) (r c : Fin 2) : PhaseJetBounds.PolynomialJets D fun (n : ι) (p : Q) => covarianceMatrix a b pref ψ v n p r c

theorem NavierStokes.PrimaryPulseBounds.slot_profile_polynomial {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (D : PhaseJetBounds.Domain ι Q) (ψ : ℝ → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) : PhaseJetBounds.PolynomialJets (productDomain D (fun (x : ι) => Set.Ioo 0 1) ⋯) fun (x : ι) (z : Q × ℝ) => ψ z.2

A fixed smooth cutoff has the required jets, derived by compactness of the fixed profile rather than supplied as a family of derivative bounds.

noncomputable def NavierStokes.PrimaryPulseBounds.normalizedMatrix (r : ℝ) (H : SmoothCovariance.Mat2) : SmoothCovariance.Mat2

Normalized matrix, defined pointwise by r * H i j.

Equations

• NavierStokes.PrimaryPulseBounds.normalizedMatrix r H i j = r * H i j

theorem NavierStokes.PrimaryPulseBounds.normalizedMatrix_det (r : ℝ) (H : SmoothCovariance.Mat2) : Matrix.det (normalizedMatrix r H) = r ^ 2 * Matrix.det H

theorem NavierStokes.PrimaryPulseBounds.weights_eq_normalized (r : ℝ) (H : SmoothCovariance.Mat2) (T : SmoothCovariance.Vec2) (hr : r ≠ 0) (hH : Matrix.det H ≠ 0) (j : Fin 2) : SmoothCovariance.weights H T j = r ^ 2 * (Matrix.det (normalizedMatrix r H))⁻¹ * SmoothCovariance.cramerNumerator H T j

theorem NavierStokes.PrimaryPulseBounds.covariance_weights_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {r : ℕ → ℝ} {H : ℕ → E → SmoothCovariance.Mat2} {T : ℕ → E → SmoothCovariance.Vec2} {w : ℕ → E → ℝ} (hr : PhaseJetBounds.PolynomialJets (phaseDomain s) fun (n : ℕ) (x : E) => r n) (hrne : ∀ (n : ℕ), r n ≠ 0) (hH : ∀ (i j : Fin 2), PhaseJetBounds.PolynomialJets (phaseDomain s) fun (n : ℕ) (x : E) => H n x i j) (hT : ∀ (i : Fin 2), WeightedClasses.MemClass s w 0 fun (n : ℕ) (x : E) => T n x i) {b M : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hdet : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (normalizedMatrix (r n) (H n x))|) (hentry : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |r n * H n x i j| ≤ M) (j : Fin 2) : WeightedClasses.MemClass s w 0 fun (n : ℕ) (x : E) => SmoothCovariance.weights (H n x) (T n x) j

Only the normalized matrix's zeroth-order range and determinant gap are inputs. All inverse jets follow from the actual integrated matrix entries.

theorem NavierStokes.PrimaryPulseBounds.covariance_amplitudes_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {r : ℕ → ℝ} {H : ℕ → E → SmoothCovariance.Mat2} {T : ℕ → E → SmoothCovariance.Vec2} {w : ℕ → E → ℝ} (hr : PhaseJetBounds.PolynomialJets (phaseDomain s) fun (n : ℕ) (x : E) => r n) (hrne : ∀ (n : ℕ), r n ≠ 0) (hH : ∀ (i j : Fin 2), PhaseJetBounds.PolynomialJets (phaseDomain s) fun (n : ℕ) (x : E) => H n x i j) (hT : ∀ (i : Fin 2), WeightedClasses.MemClass s w 0 fun (n : ℕ) (x : E) => T n x i) {b M c : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hc : 0 < c) (hdet : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (normalizedMatrix (r n) (H n x))|) (hentry : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |r n * H n x i j| ≤ M) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < w n x) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (j : Fin 2), c * w n x ≤ SmoothCovariance.weights (H n x) (T n x) j) (j : Fin 2) : WeightedClasses.MemClass s (fun (n : ℕ) (x : E) => √(w n x)) 0 fun (n : ℕ) (x : E) => SmoothCovariance.amplitudes (H n x) (T n x) j

The primary square root retains the edge factor. Positivity is derived from the positive edge weight and the order-zero lower bound.

theorem NavierStokes.PrimaryPulseBounds.sqrt_slow_polynomial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) : PhaseJetBounds.PolynomialJets (phaseDomain s) fun (n : ℕ) (x : E) => √(s.slow n)

The manuscript's normalization r=√S is a frozen polynomial family.

noncomputable def NavierStokes.PrimaryPulseBounds.primaryCoefficient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) (H : ℕ → E → SmoothCovariance.Mat2) (T : ℕ → E → SmoothCovariance.Vec2) (mask : ℕ → E → ℝ) (v : ℕ → E → Space) (j : Fin 2) : ℕ → E → HarmonicCalculus.ComplexVector

The stripped coefficient uses exactly the positive inverse-weight amplitude of the physical covariance construction.

Equations

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

theorem NavierStokes.PrimaryPulseBounds.primaryCoefficient_waveClass {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {P : ℕ → E → ℝ} {H : ℕ → E → SmoothCovariance.Mat2} {T : ℕ → E → SmoothCovariance.Vec2} {mask : ℕ → E → ℝ} {v : ℕ → E → Space} (hH : ∀ (i j : Fin 2), PhaseJetBounds.PolynomialJets (phaseDomain s) fun (n : ℕ) (x : E) => H n x i j) (hT : ∀ (i : Fin 2), WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : E) => T n x i) (hmask : PhaseJetBounds.PolynomialJets (phaseDomain s) mask) (hv : WeightedClasses.MemClass s P 0 v) {b M c : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hc : 0 < c) (hdet : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (normalizedMatrix (√(s.slow n)) (H n x))|) (hentry : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |√(s.slow n) * H n x i j| ≤ M) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (j : Fin 2), c * s.zeta x ≤ SmoothCovariance.weights (H n x) (T n x) j) (j : Fin 2) : WeightedClasses.WaveClass s P (1 / 2) (primaryCoefficient s H T mask v j)

All stripped jets of the constructed amplitude retain √ζ P. The half-power comes from the actual √ε factor, not a bound assumed on it.

noncomputable def NavierStokes.PrimaryPulseBounds.primaryCurlRemainder {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) (N : ℕ → E → Space) (R : E → ℝ) (Vr Vθ Vz : ℕ → E → E) (harmonic : ℕ → ℤ) (a : ℕ → E → HarmonicCalculus.ComplexVector) : ℕ → E → HarmonicCalculus.ComplexVector

The actual normal-cross-product curl correction with the rounded carrier and any nonzero integer harmonic.

Equations

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

theorem NavierStokes.PrimaryPulseBounds.primaryCurlRemainder_waveClass {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {P : ℕ → E → ℝ} {κ : ℝ} {N : ℕ → E → Space} {R : E → ℝ} {Vr Vθ Vz : ℕ → E → E} {harmonic : ℕ → ℤ} {a : ℕ → E → HarmonicCalculus.ComplexVector} (hN : PhaseJetBounds.PolynomialJets (phaseDomain s) N) (ha : WeightedClasses.WaveClass s P (1 / 2) a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖N n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖N n x‖ ≤ M) (hκ : 0 ≤ κ) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hθ : WeightedClasses.UnweightedClass s 0 Vθ) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hR : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : E) => (R x_1)⁻¹) (hharmonic : ∀ (n : ℕ), harmonic n ≠ 0) : WeightedClasses.WaveClass s P (1 - κ) (primaryCurlRemainder s N R Vr Vθ Vz harmonic a)

theorem NavierStokes.PrimaryPulseBounds.primaryCurlRemainder_budget {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {P : ℕ → E → ℝ} {κ : ℝ} {N : ℕ → E → Space} {R : E → ℝ} {Vr Vθ Vz : ℕ → E → E} {harmonic : ℕ → ℤ} {a : ℕ → E → HarmonicCalculus.ComplexVector} (h : WeightedClasses.WaveClass s P (1 - κ) (primaryCurlRemainder s N R Vr Vθ Vz harmonic a)) (hκ : κ ≤ 8 / 25) : WeightedClasses.WaveClass s P (17 / 25) (primaryCurlRemainder s N R Vr Vθ Vz harmonic a)

In particular the exact-curl change meets the cumulative 0.68 budget.

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.congr {ι : Type u_1} {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : PhaseJetBounds.Domain ι E} {w : ι → E → ℝ} {f g : ι → E → F} (hf : EnvelopeJets D w f) (hfg : ∀ (i : ι), Set.EqOn (f i) (g i) (D.carrier i)) : EnvelopeJets D w g

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.map {ι : Type u_1} {E F G : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {D : PhaseJetBounds.Domain ι E} {w : ι → E → ℝ} {f : ι → E → F} (hf : EnvelopeJets D w f) (L : F →L[ℝ] G) : EnvelopeJets D w fun (i : ι) (x : E) => L (f i x)

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.add {ι : Type u_1} {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : PhaseJetBounds.Domain ι E} {w : ι → E → ℝ} {f g : ι → E → F} (hf : EnvelopeJets D w f) (hg : EnvelopeJets D w g) : EnvelopeJets D w fun (i : ι) (x : E) => f i x + g i x

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.smul_polynomial {ι : Type u_1} {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : PhaseJetBounds.Domain ι E} {w a : ι → E → ℝ} {f : ι → E → F} (ha : EnvelopeJets D w a) (hf : PhaseJetBounds.PolynomialJets D f) : EnvelopeJets D w fun (i : ι) (x : E) => a i x • f i x

Multiplying by an actual polynomial-jet geometric factor preserves the full envelope, including weights which can become arbitrarily small.

theorem NavierStokes.PrimaryPulseBounds.ambient_envelope_jets {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : PhaseJetBounds.Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} {w : ι → Q × ℝ → ℝ} {z : ι → Q × ℝ → State} (hz : EnvelopeJets D w z) (hc : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets D fun (n : ι) => synthesisColumn (d n) j) : EnvelopeJets D w fun (n : ι) (x : Q × ℝ) => (d n).ambient x (z n x)

noncomputable def NavierStokes.PrimaryPulseBounds.normalizedPulse {Q : Type} (d : PrimaryODE.FrameData Q) (lam u L : ℝ) (z : Q × ℝ) : Space

Normalized pulse, given by d.ambient (z.1, L * z.2) (fundamental d lam u L (z.1, L * z.2)).

Equations

• NavierStokes.PrimaryPulseBounds.normalizedPulse d lam u L z = d.ambient (z.1, L * z.2) (NavierStokes.PrimaryPulseBounds.fundamental d lam u L (z.1, L * z.2))

theorem NavierStokes.PrimaryPulseBounds.normalizedPulse_envelope_jets {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (D : PhaseJetBounds.Domain ι Q) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) (d : ι → PrimaryODE.FrameData Q) (hd : PhaseJetBounds.FrameJets (productDomain D V hV) d) (lam u L : ι → ℝ) (hL : ∀ (i : ι), 0 < L i) (hI : ∀ (i : ι), Set.Icc 0 (L i) ⊆ V i) (hf : EnvelopeJets (productDomain D (fun (i : ι) => Set.Ioo 0 (L i)) ⋯) (fun (i : ι) (z : Q × ℝ) => referenceP (lam i) (u i) (L i) z.2) fun (i : ι) => fundamental (d i) (lam i) (u i) (L i)) {M : ℝ} (hM : 1 ≤ M) (hslot : ∀ (i : ι), L i ≤ M * D.scale i) : EnvelopeJets (productDomain D (fun (x : ι) => Set.Ioo 0 1) ⋯) (fun (i : ι) (z : Q × ℝ) => referenceP (lam i) (u i) (L i) (L i * z.2)) fun (i : ι) => normalizedPulse (d i) (lam i) (u i) (L i)

theorem NavierStokes.PrimaryPulseBounds.normalizedPulse_polynomial {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (D : PhaseJetBounds.Domain ι Q) (lam u L : ι → ℝ) (d : ι → PrimaryODE.FrameData Q) (h : EnvelopeJets (productDomain D (fun (x : ι) => Set.Ioo 0 1) ⋯) (fun (i : ι) (z : Q × ℝ) => referenceP (lam i) (u i) (L i) (L i * z.2)) fun (i : ι) => normalizedPulse (d i) (lam i) (u i) (L i)) (hlam : ∀ (i : ι), 0 < lam i) (hu : ∀ (i : ι), 0 < u i) (hL : ∀ (i : ι), 0 < L i) : PhaseJetBounds.PolynomialJets (productDomain D (fun (x : ι) => Set.Ioo 0 1) ⋯) fun (i : ι) => normalizedPulse (d i) (lam i) (u i) (L i)

noncomputable def NavierStokes.PrimaryPulseBounds.primaryCovariance {ι : Type u_1} {Q : Type} (pref : Fin 2 → ι → ℝ) (d : Fin 2 → ι → PrimaryODE.FrameData Q) (lam u L : Fin 2 → ι → ℝ) : ι → Q → SmoothCovariance.Mat2

The covariance matrix is made from the two constructed ambient pulses, with the fixed smooth middle cutoff.

Equations

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

theorem NavierStokes.PrimaryPulseBounds.primaryCovariance_entry_polynomial {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (D : PhaseJetBounds.Domain ι Q) (pref : Fin 2 → ι → ℝ) (d : Fin 2 → ι → PrimaryODE.FrameData Q) (lam u L : Fin 2 → ι → ℝ) (hpref : ∀ (c : Fin 2), PhaseJetBounds.PolynomialJets D fun (n : ι) (x : Q) => pref c n) (hpulse : ∀ (c : Fin 2), EnvelopeJets (productDomain D (fun (x : ι) => Set.Ioo 0 1) ⋯) (fun (i : ι) (z : Q × ℝ) => referenceP (lam c i) (u c i) (L c i) (L c i * z.2)) fun (i : ι) => normalizedPulse (d c i) (lam c i) (u c i) (L c i)) (hlam : ∀ (c : Fin 2) (i : ι), 0 < lam c i) (hu : ∀ (c : Fin 2) (i : ι), 0 < u c i) (hL : ∀ (c : Fin 2) (i : ι), 0 < L c i) (r c : Fin 2) : PhaseJetBounds.PolynomialJets D fun (n : ι) (p : Q) => primaryCovariance pref d lam u L n p r c

theorem NavierStokes.PrimaryPulseBounds.profile_support_covariance_interval : Function.support GaussianTailFlat.profile ⊆ Set.Ioc (1 / 10) (9 / 10)

theorem NavierStokes.PrimaryPulseBounds.actualColumn_normalization {a b L : ℝ} (hL : 0 < L) (ci : ℝ) (ψ x : ℝ → ℝ) (t : ℝ → SmoothCovariance.Vec2) (χ : ℝ → ℝ) (v : ℝ → Space) (hχ : Function.support χ ⊆ Set.Ioc a b) (r : Fin 2) (hmatch : ∀ (s : ℝ), ψ s ^ 2 * x s * t s r = χ (s / L) ^ 2 * ((v (s / L)).ofLp 0 * (v (s / L)).ofLp r.succ)) : PulseCovariance.actualColumn ci ψ x t r = ci * L * ∫ (s : ℝ) in a..b, χ s ^ 2 * ((v s).ofLp 0 * (v s).ofLp r.succ)

Exact change of variables from the physical slot to the fixed middle interval. The integrand identity can be checked only where the cutoff is nonzero; no global equality of clamped ODE extensions is required.

theorem NavierStokes.PrimaryPulseBounds.primaryCovariance_eq_pairMatrix {ι : Type u_1} {Q : Type} (pref : Fin 2 → ι → ℝ) (d : Fin 2 → ι → PrimaryODE.FrameData Q) (lam u L : Fin 2 → ι → ℝ) (n : ι) (p : Q) (vr vt : TorusInverse.Plane) (radius : ℝ) (ci : SmoothCovariance.Vec2) (pulses : Fin 2 → PartitionedCovariance.Pulse) (hL : ∀ (c : Fin 2), 0 < L c n) (hpref : ∀ (c : Fin 2), pref c n = PartitionedCovariance.nativePrefactor vr vt radius * ci c * L c n) (hmatch : ∀ (c r : Fin 2) (s : ℝ), (pulses c).ψ s ^ 2 * (pulses c).x s * (pulses c).t s r = GaussianTailFlat.profile (s / L c n) ^ 2 * ((normalizedPulse (d c n) (lam c n) (u c n) (L c n) (p, s / L c n)).ofLp 0 * (normalizedPulse (d c n) (lam c n) (u c n) (L c n) (p, s / L c n)).ofLp r.succ)) : primaryCovariance pref d lam u L n p = PartitionedCovariance.pairMatrix vr vt radius ci pulses

The matrix estimated above is the literal matrix of native pulse covariances when the two original pulse integrands are identified.

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.polynomial_smul {ι : Type u_1} {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : PhaseJetBounds.Domain ι E} {w a : ι → E → ℝ} {f : ι → E → F} (hf : EnvelopeJets D w f) (ha : PhaseJetBounds.PolynomialJets D a) : EnvelopeJets D w fun (i : ι) (x : E) => a i x • f i x

theorem NavierStokes.PrimaryPulseBounds.EnvelopeJets.mono_weight {ι : Type u_1} {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : PhaseJetBounds.Domain ι E} {w v : ι → E → ℝ} {f : ι → E → F} (hf : EnvelopeJets D w f) (hvw : ∀ (i : ι), ∀ x ∈ D.carrier i, w i x ≤ v i x) : EnvelopeJets D v f

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

A compactly contained cutoff extends the actual slot solution with all jets. No smoothness of the uncut solution outside the slot is used.

theorem NavierStokes.PrimaryPulseBounds.profile_linear_polynomial {ι : Type u_1} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (D : PhaseJetBounds.Domain ι E) (L : E →L[ℝ] ℝ) : PhaseJetBounds.PolynomialJets D fun (x : ι) (x_1 : E) => GaussianTailFlat.profile (L x_1)

All profile jets are obtained from the constructed compact smooth bump.

noncomputable def NavierStokes.PrimaryPulseBounds.cutoffPulse {Q : Type} (d : PrimaryODE.FrameData Q) (lam u L : ℝ) (z : Q × ℝ) : Space

Cutoff pulse, given by GaussianTailFlat.profile z.2 • normalizedPulse d lam u L z.

Equations

• NavierStokes.PrimaryPulseBounds.cutoffPulse d lam u L z = NavierStokes.GaussianTailFlat.profile z.2 • NavierStokes.PrimaryPulseBounds.normalizedPulse d lam u L z

theorem NavierStokes.PrimaryPulseBounds.profile_tsupport_slot {Q : Type} [NormedAddCommGroup Q] : (tsupport fun (z : Q × ℝ) => GaussianTailFlat.profile z.2) ⊆ {z : Q × ℝ | z.2 ∈ Set.Ioo 0 1}

theorem NavierStokes.PrimaryPulseBounds.cutoffPulse_envelope_jets {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (D : PhaseJetBounds.Domain ι Q) (d : ι → PrimaryODE.FrameData Q) (lam u L : ι → ℝ) (hp : EnvelopeJets (productDomain D (fun (x : ι) => Set.Ioo 0 1) ⋯) (fun (i : ι) (z : Q × ℝ) => referenceP (lam i) (u i) (L i) (L i * z.2)) fun (i : ι) => normalizedPulse (d i) (lam i) (u i) (L i)) : EnvelopeJets (productDomain D (fun (x : ι) => Set.univ) ⋯) (fun (i : ι) (z : Q × ℝ) => GaussianTailFlat.referenceSlotEnvelope (lam i) (u i) (L i) z.2) fun (i : ι) => cutoffPulse (d i) (lam i) (u i) (L i)

The actual cutoff pulse has global slot-coordinate jets with the zero-extended Gaussian envelope. This is the form used in physical charts.

theorem NavierStokes.PrimaryPulseBounds.phase_normalizedPulse_envelope_jets {ι : Type u_1} (a : PhaseJetBounds.PhaseFamily ι) (D : PhaseJetBounds.Domain ι PhaseJetBounds.Slow) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) (lam c0 u L ν B : ι → ℝ) (K : ι → PhaseJetBounds.Plane) (s δ : ι → PhaseJetBounds.Slow × ℝ → ℝ) (hF : PhaseJetBounds.PolynomialJets D a.F) (hG : PhaseJetBounds.PolynomialJets D a.G) {r b M : ℝ} (hr : 0 < r) (hb : 0 < b) (hM : 1 ≤ M) (hconstant : ∀ (i : ι), |a.epsilon i| ≤ M ∧ |a.p i| ≤ M ∧ |a.pz i| ≤ M ∧ |a.x0 i| ≤ M) (heps : ∀ (i : ι), a.epsilon i ≠ 0) (hR : ∀ (i : ι), ∀ q ∈ D.carrier i, r ≤ |q.1| ∧ |q.1| ≤ M) (hslot : ∀ (i : ι), ∀ v ∈ V i, |v| ≤ M * D.scale i) (hlam : ∀ (i : ι), |lam i| ≤ M) (hc : ∀ (i : ι), b ≤ |c0 i| ∧ |c0 i| ≤ M) (hu : ∀ (i : ι), |u i| ≤ M) (hrate : ∀ (i : ι), |u i / L i| * D.scale i ≤ M) (hν : ∀ (i : ι), |ν i| ≤ M) (hB : ∀ (i : ι), 2 * b ≤ B i ∧ B i ≤ M) (hK : ∀ (i : ι), ‖K i‖ = 1) (hs : ∀ (i : ι), ∀ z ∈ (D.slot V hV).carrier i, |s i z| ≤ M) (hδ : ∀ (i : ι), ∀ z ∈ (D.slot V hV).carrier i, δ i z ≤ B i / 2) (hclose : ∀ (i : ι), ∀ z ∈ (D.slot V hV).carrier i, ‖a.normal i z - MovingFrameODE.pack (B i * s i z) (B i • K i)‖ ≤ δ i z) (hlampos : ∀ (i : ι), 0 < lam i) (hupos : ∀ (i : ι), 0 < u i) (hL : ∀ (i : ι), 0 < L i) (hI : ∀ (i : ι), Set.Icc 0 (L i) ⊆ V i) (hνpos : ∀ (i : ι), 0 ≤ ν i) {C E : ℝ} (hC : 0 ≤ C) (hE : 0 ≤ E) (hvisc : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), ViscousPropagator.referenceViscosity (lam i) (u i) (L i) v - E / D.scale i ≤ (a.frameData lam c0 u L ν i).viscosity (p, v)) (herr : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), |(a.frameData lam c0 u L ν i).error11 (p, v)| ≤ C / D.scale i ∧ |(a.frameData lam c0 u L ν i).error12 (p, v)| ≤ C / D.scale i ∧ |(a.frameData lam c0 u L ν i).error21 (p, v)| ≤ C / D.scale i ∧ |(a.frameData lam c0 u L ν i).error22 (p, v)| ≤ C / D.scale i) : EnvelopeJets (productDomain D (fun (x : ι) => Set.Ioo 0 1) ⋯) (fun (i : ι) (z : PhaseJetBounds.Slow × ℝ) => referenceP (lam i) (u i) (L i) (L i * z.2)) fun (i : ι) => normalizedPulse (a.frameData lam c0 u L ν i) (lam i) (u i) (L i)

The actual PhaseCalculus normal and reconstructed frame supply the ODE coefficient jets. Only normalized base-field jets and previously quantified zeroth-order geometric/viscous errors are inputs. Rounding and all fixed representative choices stay constant within each label.

noncomputable def NavierStokes.PrimaryPulseBounds.chartCovariance {Q E : Type} (pref : Fin 2 → ℕ → ℝ) (d : Fin 2 → ℕ → PrimaryODE.FrameData Q) (lam u L : Fin 2 → ℕ → ℝ) (χ : ℕ → E → Q × ℝ) : ℕ → E → SmoothCovariance.Mat2

Chart covariance, defined pointwise by primaryCovariance pref d lam u L n (χ n x).1.

Equations

• NavierStokes.PrimaryPulseBounds.chartCovariance pref d lam u L χ n x = NavierStokes.PrimaryPulseBounds.primaryCovariance pref d lam u L n (χ n x).1

noncomputable def NavierStokes.PrimaryPulseBounds.primaryWave {Q E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) (pref : Fin 2 → ℕ → ℝ) (d : Fin 2 → ℕ → PrimaryODE.FrameData Q) (lam u L : Fin 2 → ℕ → ℝ) (χ : ℕ → E → Q × ℝ) (T : ℕ → E → SmoothCovariance.Vec2) (mask : ℕ → E → ℝ) (c : Fin 2) : ℕ → E → HarmonicCalculus.ComplexVector

Primary wave, constructed using primaryCoefficient.

Equations

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

theorem NavierStokes.PrimaryPulseBounds.primaryWave_waveClass {Q E : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) (D : PhaseJetBounds.Domain ℕ Q) (pref : Fin 2 → ℕ → ℝ) (d : Fin 2 → ℕ → PrimaryODE.FrameData Q) (lam u L : Fin 2 → ℕ → ℝ) (χ : ℕ → E → Q × ℝ) (T : ℕ → E → SmoothCovariance.Vec2) (mask : ℕ → E → ℝ) (hscale : ∀ (n : ℕ), D.scale n = s.slow n) (hχ : PhaseJetBounds.PolynomialJets (phaseDomain s) χ) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ D.carrier n) (hpref : ∀ (c : Fin 2), PhaseJetBounds.PolynomialJets D fun (n : ℕ) (x : Q) => pref c n) (hpulse : ∀ (c : Fin 2), EnvelopeJets (productDomain D (fun (x : ℕ) => Set.Ioo 0 1) ⋯) (fun (n : ℕ) (z : Q × ℝ) => referenceP (lam c n) (u c n) (L c n) (L c n * z.2)) fun (n : ℕ) => normalizedPulse (d c n) (lam c n) (u c n) (L c n)) (hlam : ∀ (c : Fin 2) (n : ℕ), 0 < lam c n) (hu : ∀ (c : Fin 2) (n : ℕ), 0 < u c n) (hL : ∀ (c : Fin 2) (n : ℕ), 0 < L c n) (hT : ∀ (i : Fin 2), WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : E) => T n x i) (hmask : PhaseJetBounds.PolynomialJets (phaseDomain s) mask) {b M a : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (ha : 0 < a) (hdet : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (normalizedMatrix (√(s.slow n)) (chartCovariance pref d lam u L χ n x))|) (hentry : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |√(s.slow n) * chartCovariance pref d lam u L χ n x i j| ≤ M) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (j : Fin 2), a * s.zeta x ≤ SmoothCovariance.weights (chartCovariance pref d lam u L χ n x) (T n x) j) (c : Fin 2) : WeightedClasses.WaveClass s (fun (n : ℕ) (x : E) => GaussianTailFlat.referenceSlotEnvelope (lam c n) (u c n) (L c n) (χ n x).2) (1 / 2) (primaryWave s pref d lam u L χ T mask c)

Assembly with the actual phase-frame pulse, the actual integrated covariance matrix, the fixed slot cutoff, and a chart of polynomial scale. The remaining matrix hypotheses are strictly order zero.

structure NavierStokes.PrimaryPulseBounds.PhaseConstruction {ι : Type u_1} (D : PhaseJetBounds.Domain ι PhaseJetBounds.Slow) : Type u_1

Explicit input data for one sign of the phase construction. There are no solution, propagator, covariance, or output-jet assumptions in this record. The error fields are the order-zero moving-frame estimates.

• phase : PhaseJetBounds.PhaseFamily ι

  Phase of PhaseConstruction, of type PhaseFamily ι.

• V : ι → Set ℝ

  V of PhaseConstruction, of type ι → Set ℝ.

• openV (i : ι) : IsOpen (self.V i)
• lam : ι → ℝ

  Lam of PhaseConstruction, of type ι → ℝ.

• c0 : ι → ℝ

  C0 of PhaseConstruction, of type ι → ℝ.

• u : ι → ℝ

  U of PhaseConstruction, of type ι → ℝ.

• L : ι → ℝ

  L of PhaseConstruction, of type ι → ℝ.

• viscosity : ι → ℝ

  Viscosity of PhaseConstruction, of type ι → ℝ.

• B : ι → ℝ

  Bound parameter of PhaseConstruction, of type ι → ℝ.

• K : ι → PhaseJetBounds.Plane

  K of PhaseConstruction, of type ι → Plane.

• slope : ι → PhaseJetBounds.Slow × ℝ → ℝ

  Slope of PhaseConstruction, of type ι → Slow × ℝ → ℝ.

• error : ι → PhaseJetBounds.Slow × ℝ → ℝ

  Error of PhaseConstruction, of type ι → Slow × ℝ → ℝ.

• r : ℝ

  R of PhaseConstruction, of type ℝ.

• b : ℝ

  B of PhaseConstruction, of type ℝ.

• M : ℝ

  M of PhaseConstruction, of type ℝ.

• C : ℝ

  Bound coefficient of PhaseConstruction, of type ℝ.

• E : ℝ

  E of PhaseConstruction, of type ℝ.

• r_pos : 0 < self.r
• b_pos : 0 < self.b
• one_le_M : 1 ≤ self.M
• C_nonneg : 0 ≤ self.C
• E_nonneg : 0 ≤ self.E
• baseF : PhaseJetBounds.PolynomialJets D self.phase.F
• baseG : PhaseJetBounds.PolynomialJets D self.phase.G
• constants (i : ι) : |self.phase.epsilon i| ≤ self.M ∧ |self.phase.p i| ≤ self.M ∧ |self.phase.pz i| ≤ self.M ∧ |self.phase.x0 i| ≤ self.M
• epsilon_ne (i : ι) : self.phase.epsilon i ≠ 0
• radius (i : ι) (q : PhaseJetBounds.Slow) : q ∈ D.carrier i → self.r ≤ |q.1| ∧ |q.1| ≤ self.M
• slot (i : ι) (v : ℝ) : v ∈ self.V i → |v| ≤ self.M * D.scale i
• lam_bound (i : ι) : |self.lam i| ≤ self.M
• c0_bound (i : ι) : self.b ≤ |self.c0 i| ∧ |self.c0 i| ≤ self.M
• u_bound (i : ι) : |self.u i| ≤ self.M
• rate_bound (i : ι) : |self.u i / self.L i| * D.scale i ≤ self.M
• viscosity_bound (i : ι) : |self.viscosity i| ≤ self.M
• B_bound (i : ι) : 2 * self.b ≤ self.B i ∧ self.B i ≤ self.M
• K_unit (i : ι) : ‖self.K i‖ = 1
• slope_bound (i : ι) (z : PhaseJetBounds.Slow × ℝ) : z ∈ (D.slot self.V ⋯).carrier i → |self.slope i z| ≤ self.M
• error_small (i : ι) (z : PhaseJetBounds.Slow × ℝ) : z ∈ (D.slot self.V ⋯).carrier i → self.error i z ≤ self.B i / 2
• normal_close (i : ι) (z : PhaseJetBounds.Slow × ℝ) : z ∈ (D.slot self.V ⋯).carrier i → ‖self.phase.normal i z - MovingFrameODE.pack (self.B i * self.slope i z) (self.B i • self.K i)‖ ≤ self.error i z
• lam_pos (i : ι) : 0 < self.lam i
• u_pos (i : ι) : 0 < self.u i
• L_pos (i : ι) : 0 < self.L i
• interval (i : ι) : Set.Icc 0 (self.L i) ⊆ self.V i
• viscosity_nonneg (i : ι) : 0 ≤ self.viscosity i
• damping_error (i : ι) (p : PhaseJetBounds.Slow) : p ∈ D.carrier i → ∀ v ∈ Set.Icc 0 (self.L i), ViscousPropagator.referenceViscosity (self.lam i) (self.u i) (self.L i) v - self.E / D.scale i ≤ (self.phase.frameData self.lam self.c0 self.u self.L self.viscosity i).viscosity (p, v)
• modal_errors (i : ι) (p : PhaseJetBounds.Slow) : p ∈ D.carrier i → ∀ v ∈ Set.Icc 0 (self.L i), |(self.phase.frameData self.lam self.c0 self.u self.L self.viscosity i).error11 (p, v)| ≤ self.C / D.scale i ∧ |(self.phase.frameData self.lam self.c0 self.u self.L self.viscosity i).error12 (p, v)| ≤ self.C / D.scale i ∧ |(self.phase.frameData self.lam self.c0 self.u self.L self.viscosity i).error21 (p, v)| ≤ self.C / D.scale i ∧ |(self.phase.frameData self.lam self.c0 self.u self.L self.viscosity i).error22 (p, v)| ≤ self.C / D.scale i

noncomputable def NavierStokes.PrimaryPulseBounds.PhaseConstruction.frame {ι : Type u_1} {D : PhaseJetBounds.Domain ι PhaseJetBounds.Slow} (p : PhaseConstruction D) : ι → PrimaryODE.FrameData PhaseJetBounds.Slow

Frame, given by p.phase.frameData p.lam p.c0 p.u p.L p.viscosity.

Equations

• p.frame = p.phase.frameData p.lam p.c0 p.u p.L p.viscosity

theorem NavierStokes.PrimaryPulseBounds.PhaseConstruction.pulse_jets {ι : Type u_1} {D : PhaseJetBounds.Domain ι PhaseJetBounds.Slow} (p : PhaseConstruction D) : EnvelopeJets (productDomain D (fun (x : ι) => Set.Ioo 0 1) ⋯) (fun (i : ι) (z : PhaseJetBounds.Slow × ℝ) => referenceP (p.lam i) (p.u i) (p.L i) (p.L i * z.2)) fun (i : ι) => normalizedPulse (p.frame i) (p.lam i) (p.u i) (p.L i)

theorem NavierStokes.PrimaryPulseBounds.PhaseConstruction.normal_jets {ι : Type u_1} {D : PhaseJetBounds.Domain ι PhaseJetBounds.Slow} (p : PhaseConstruction D) : PhaseJetBounds.PolynomialJets (D.slot p.V ⋯) p.phase.normal

theorem NavierStokes.PrimaryPulseBounds.PhaseConstruction.normal_range {ι : Type u_1} {D : PhaseJetBounds.Domain ι PhaseJetBounds.Slow} (p : PhaseConstruction D) : (∀ (i : ι), ∀ z ∈ (D.slot p.V ⋯).carrier i, p.b ≤ ‖p.phase.normal i z‖) ∧ ∀ (i : ι), ∀ z ∈ (D.slot p.V ⋯).carrier i, ‖p.phase.normal i z‖ ≤ p.M ^ 2 + 3 * p.M

noncomputable def NavierStokes.PrimaryPulseBounds.phaseCovariance {D : PhaseJetBounds.Domain ℕ PhaseJetBounds.Slow} (F : Fin 2 → PhaseConstruction D) (pref : Fin 2 → ℕ → ℝ) : ℕ → PhaseJetBounds.Slow → SmoothCovariance.Mat2

Phase covariance, given by primaryCovariance pref (fun c => (F c).frame) (fun c => (F c).lam) (fun c => (F c).u) (fun c => (F c).L).

Equations

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

noncomputable def NavierStokes.PrimaryPulseBounds.phaseWave {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) {D : PhaseJetBounds.Domain ℕ PhaseJetBounds.Slow} (F : Fin 2 → PhaseConstruction D) (pref : Fin 2 → ℕ → ℝ) (χ : ℕ → E → PhaseJetBounds.Slow × ℝ) (T : ℕ → E → SmoothCovariance.Vec2) (mask : ℕ → E → ℝ) (c : Fin 2) : ℕ → E → HarmonicCalculus.ComplexVector

Phase wave, given by primaryWave s pref (fun c => (F c).frame) (fun c => (F c).lam) (fun c => (F c).u) (fun c => (F c).L) χ T mask c.

Equations

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

theorem NavierStokes.PrimaryPulseBounds.phaseWave_waveClass {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) (D : PhaseJetBounds.Domain ℕ PhaseJetBounds.Slow) (F : Fin 2 → PhaseConstruction D) (pref : Fin 2 → ℕ → ℝ) (χ : ℕ → E → PhaseJetBounds.Slow × ℝ) (T : ℕ → E → SmoothCovariance.Vec2) (mask : ℕ → E → ℝ) (hscale : ∀ (n : ℕ), D.scale n = s.slow n) (hχ : PhaseJetBounds.PolynomialJets (phaseDomain s) χ) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ D.carrier n) (hpref : ∀ (c : Fin 2), PhaseJetBounds.PolynomialJets D fun (n : ℕ) (x : PhaseJetBounds.Slow) => pref c n) (hT : ∀ (i : Fin 2), WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : E) => T n x i) (hmask : PhaseJetBounds.PolynomialJets (phaseDomain s) mask) {b M a : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (ha : 0 < a) (hdet : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (normalizedMatrix (√(s.slow n)) (phaseCovariance F pref n (χ n x).1))|) (hentry : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |√(s.slow n) * phaseCovariance F pref n (χ n x).1 i j| ≤ M) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (j : Fin 2), a * s.zeta x ≤ SmoothCovariance.weights (phaseCovariance F pref n (χ n x).1) (T n x) j) (c : Fin 2) : WeightedClasses.WaveClass s (fun (n : ℕ) (x : E) => GaussianTailFlat.referenceSlotEnvelope ((F c).lam n) ((F c).u n) ((F c).L n) (χ n x).2) (1 / 2) (phaseWave s F pref χ T mask c)

End-to-end primary class membership from the actual phase/base inputs. The covariance matrix in the hypotheses is the integral of these same constructed pulses. Its derivative bounds and all amplitude jets are derived in the proof.

theorem NavierStokes.PrimaryPulseBounds.cutoffPulse_eq_ambient_primary {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) {p : Q} (hp : p ∈ U) {t : ℝ} (ht : t ∈ Set.Icc 0 L) : cutoffPulse d lam u L (p, t / L) = GaussianTailFlat.slotCutoff L t • d.ambient (p, t) (PrimaryODE.primary ⋯ d (fun (z : Q × ℝ) => referenceP lam u L z.2) p t)

The local cutoff uses exactly the already constructed primary ODE solution, including its Gaussian initial normalization.

noncomputable def NavierStokes.PrimaryPulseBounds.localPrimaryProfile {Q : Type} (d : PrimaryODE.FrameData Q) (lam u L radius : ℝ) (p : Q) (z : TorusInverse.Plane) : Space

Local primary profile, given by PartitionedCovariance.cutoff radius z.1 • cutoffPulse d lam u L (p, z.2 / L).

Equations

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

theorem NavierStokes.PrimaryPulseBounds.localPrimaryProfile_radial {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u radius : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) {p : Q} (hp : p ∈ U) (P : PartitionedCovariance.Pulse) (z : TorusInverse.Plane) (hz : z.2 ∈ Set.Icc 0 L) (hψ : P.ψ z.2 = GaussianTailFlat.slotCutoff L z.2) (hx : P.x z.2 = (d.ambient (p, z.2) (PrimaryODE.primary ⋯ d (fun (w : Q × ℝ) => referenceP lam u L w.2) p z.2)).ofLp 0) : P.radialProfile radius z = (localPrimaryProfile d lam u L radius p z).ofLp 0

theorem NavierStokes.PrimaryPulseBounds.localPrimaryProfile_tangent {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u radius : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) {p : Q} (hp : p ∈ U) (P : PartitionedCovariance.Pulse) (z : TorusInverse.Plane) (hz : z.2 ∈ Set.Icc 0 L) (i : Fin 2) (hψ : P.ψ z.2 = GaussianTailFlat.slotCutoff L z.2) (ht : P.t z.2 i = (d.ambient (p, z.2) (PrimaryODE.primary ⋯ d (fun (w : Q × ℝ) => referenceP lam u L w.2) p z.2)).ofLp i.succ) : P.tangentProfile radius i z = (localPrimaryProfile d lam u L radius p z).ofLp i.succ

noncomputable def NavierStokes.PrimaryPulseBounds.PhaseConstruction.chartNormal {E : Type} {D : PhaseJetBounds.Domain ℕ PhaseJetBounds.Slow} (p : PhaseConstruction D) (χ : ℕ → E → PhaseJetBounds.Slow × ℝ) (n : ℕ) (x : E) : Space

Chart normal, given by p.phase.normal n ((χ n x).1, p.L n * (χ n x).2).

Equations

• p.chartNormal χ n x = p.phase.normal n ((χ n x).1, p.L n * (χ n x).2)

theorem NavierStokes.PrimaryPulseBounds.PhaseConstruction.chartNormal_bounds {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {D : PhaseJetBounds.Domain ℕ PhaseJetBounds.Slow} (p : PhaseConstruction D) (χ : ℕ → E → PhaseJetBounds.Slow × ℝ) (hscale : ∀ (n : ℕ), D.scale n = s.slow n) (hχ : PhaseJetBounds.PolynomialJets (phaseDomain s) χ) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ D.carrier n) (hslot : ∀ (n : ℕ), ∀ x ∈ s.domain, p.L n * (χ n x).2 ∈ p.V n) : PhaseJetBounds.PolynomialJets (phaseDomain s) (p.chartNormal χ) ∧ (∀ (n : ℕ), ∀ x ∈ s.domain, p.b ≤ ‖p.chartNormal χ n x‖) ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ‖p.chartNormal χ n x‖ ≤ p.M ^ 2 + 3 * p.M

The normal appearing in the curl coefficient is the actual phase normal. Its jets and lower bound are derived from the same phase inputs.

theorem NavierStokes.PrimaryPulseBounds.PhaseConstruction.curlRemainder_waveClass {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {D : PhaseJetBounds.Domain ℕ PhaseJetBounds.Slow} (p : PhaseConstruction D) (χ : ℕ → E → PhaseJetBounds.Slow × ℝ) (hscale : ∀ (n : ℕ), D.scale n = s.slow n) (hχ : PhaseJetBounds.PolynomialJets (phaseDomain s) χ) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ D.carrier n) (hslot : ∀ (n : ℕ), ∀ x ∈ s.domain, p.L n * (χ n x).2 ∈ p.V n) {P : ℕ → E → ℝ} {a : ℕ → E → HarmonicCalculus.ComplexVector} (ha : WeightedClasses.WaveClass s P (1 / 2) a) {κ : ℝ} (hκ : 0 ≤ κ) {R : E → ℝ} {Vr Vθ Vz : ℕ → E → E} {harmonic : ℕ → ℤ} (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hθ : WeightedClasses.UnweightedClass s 0 Vθ) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hR : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : E) => (R x_1)⁻¹) (hharmonic : ∀ (n : ℕ), harmonic n ≠ 0) : WeightedClasses.WaveClass s P (1 - κ) (primaryCurlRemainder s (p.chartNormal χ) R Vr Vθ Vz harmonic a)

The exact-curl remainder bound specializes to the actual phase normal, without an assumed normal-jet or propagator estimate.

theorem NavierStokes.PrimaryPulseBounds.slotCutoff_zero_of_not_mem_Icc {L t : ℝ} (hL : 0 < L) (ht : t ∉ Set.Icc 0 L) : GaussianTailFlat.slotCutoff L t = 0

theorem NavierStokes.PrimaryPulseBounds.slotCutoff_hasCompactSupport {L : ℝ} (hL : 0 < L) : HasCompactSupport (GaussianTailFlat.slotCutoff L)

noncomputable def NavierStokes.PrimaryPulseBounds.canonicalPrimaryPath {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) (p : Q) (hp : p ∈ U) (hk : d.Kinematics p (Set.Icc 0 L)) : C(↑(Set.Icc 0 L), Space)

The continuous path is obtained from the actual ambient ODE, including both endpoints; no continuity of a clamped derivative is claimed.

Equations

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

noncomputable def NavierStokes.PrimaryPulseBounds.canonicalPrimaryPulse {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) (p : Q) (hp : p ∈ U) (hk : d.Kinematics p (Set.Icc 0 L)) : PartitionedCovariance.Pulse

A literal PartitionedCovariance.Pulse made from this same primary solution. Only its uncut components are continuously clamped; the cutoff has compact support strictly inside the interval.

Equations

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

theorem NavierStokes.PrimaryPulseBounds.canonicalPrimaryPulse_x {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) (p : Q) (hp : p ∈ U) (hk : d.Kinematics p (Set.Icc 0 L)) {t : ℝ} (ht : t ∈ Set.Icc 0 L) : (canonicalPrimaryPulse d lam u hL U hA p hp hk).x t = (d.ambient (p, t) (PrimaryODE.primary ⋯ d (fun (z : Q × ℝ) => referenceP lam u L z.2) p t)).ofLp 0

theorem NavierStokes.PrimaryPulseBounds.canonicalPrimaryPulse_t {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) (p : Q) (hp : p ∈ U) (hk : d.Kinematics p (Set.Icc 0 L)) {t : ℝ} (ht : t ∈ Set.Icc 0 L) (i : Fin 2) : (canonicalPrimaryPulse d lam u hL U hA p hp hk).t t i = (d.ambient (p, t) (PrimaryODE.primary ⋯ d (fun (z : Q × ℝ) => referenceP lam u L z.2) p t)).ofLp i.succ

theorem NavierStokes.PrimaryPulseBounds.canonicalPrimaryPulse_radialProfile {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u radius : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) (p : Q) (hp : p ∈ U) (hk : d.Kinematics p (Set.Icc 0 L)) (z : TorusInverse.Plane) : (canonicalPrimaryPulse d lam u hL U hA p hp hk).radialProfile radius z = (localPrimaryProfile d lam u L radius p z).ofLp 0

Global equality of the literal radial profiles, including off-slot points where both sides vanish by the constructed cutoff.

theorem NavierStokes.PrimaryPulseBounds.canonicalPrimaryPulse_tangentProfile {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u radius : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) (p : Q) (hp : p ∈ U) (hk : d.Kinematics p (Set.Icc 0 L)) (z : TorusInverse.Plane) (i : Fin 2) : (canonicalPrimaryPulse d lam u hL U hA p hp hk).tangentProfile radius i z = (localPrimaryProfile d lam u L radius p z).ofLp i.succ

theorem NavierStokes.PrimaryPulseBounds.canonicalPrimaryPulse_integrand {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) (p : Q) (hp : p ∈ U) (hk : d.Kinematics p (Set.Icc 0 L)) (i : Fin 2) (t : ℝ) : (canonicalPrimaryPulse d lam u hL U hA p hp hk).ψ t ^ 2 * (canonicalPrimaryPulse d lam u hL U hA p hp hk).x t * (canonicalPrimaryPulse d lam u hL U hA p hp hk).t t i = GaussianTailFlat.profile (t / L) ^ 2 * ((normalizedPulse d lam u L (p, t / L)).ofLp 0 * (normalizedPulse d lam u L (p, t / L)).ofLp i.succ)

theorem NavierStokes.PrimaryPulseBounds.primaryCovariance_eq_canonicalPairMatrix {Q : Type} [NormedAddCommGroup Q] {ι : Type u_1} (pref : Fin 2 → ι → ℝ) (d : Fin 2 → ι → PrimaryODE.FrameData Q) (lam u L : Fin 2 → ι → ℝ) (n : ι) (U : Set Q) (p : Q) (hp : p ∈ U) (hL : ∀ (c : Fin 2), 0 < L c n) (hA : ∀ (c : Fin 2), ContinuousOn ((d c n).coefficient 1) (U ×ˢ Set.Icc 0 (L c n))) (hk : ∀ (c : Fin 2), (d c n).Kinematics p (Set.Icc 0 (L c n))) (vr vt : TorusInverse.Plane) (radius : ℝ) (ci : SmoothCovariance.Vec2) (hpref : ∀ (c : Fin 2), pref c n = PartitionedCovariance.nativePrefactor vr vt radius * ci c * L c n) : primaryCovariance pref d lam u L n p = PartitionedCovariance.pairMatrix vr vt radius ci fun (c : Fin 2) => canonicalPrimaryPulse (d c n) (lam c n) (u c n) ⋯ U ⋯ p hp ⋯

theorem NavierStokes.PrimaryPulseBounds.normalizedPulse_hasDerivAt {Q : Type} [NormedAddCommGroup Q] (d : PrimaryODE.FrameData Q) (lam u : ℝ) {L : ℝ} (hL : 0 < L) (U : Set Q) (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) {p : Q} (hp : p ∈ U) (hk : d.Kinematics p (Set.Icc 0 L)) {θ : ℝ} (hθ : θ ∈ Set.Ioo 0 1) : HasDerivAt (fun (t : ℝ) => normalizedPulse d lam u L (p, t)) (L • TangentProjection.projectedRhs (d.normal (p, L * θ)) (d.normalMotion (p, L * θ)) (normalizedPulse d lam u L (p, θ)) (MovingFrameODE.baseAction (d.F (p, L * θ)) (d.shear (p, L * θ)) (normalizedPulse d lam u L (p, θ))) 0 (d.viscosity (p, L * θ))) θ

The uncut normalized pulse satisfies the actual projected equation. This is the unit fundamental used before the separate Gaussian cutoff.

noncomputable def NavierStokes.PrimaryPulseBounds.uncutPrimaryWave {Q E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) (pref : Fin 2 → ℕ → ℝ) (d : Fin 2 → ℕ → PrimaryODE.FrameData Q) (lam u L : Fin 2 → ℕ → ℝ) (χ : ℕ → E → Q × ℝ) (T : ℕ → E → SmoothCovariance.Vec2) (mask : ℕ → E → ℝ) (c : Fin 2) : ℕ → E → HarmonicCalculus.ComplexVector

Uncut primary wave, constructed using primaryCoefficient.

Equations

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

theorem NavierStokes.PrimaryPulseBounds.primaryWave_eq_cutoff {Q E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) (pref : Fin 2 → ℕ → ℝ) (d : Fin 2 → ℕ → PrimaryODE.FrameData Q) (lam u L : Fin 2 → ℕ → ℝ) (χ : ℕ → E → Q × ℝ) (T : ℕ → E → SmoothCovariance.Vec2) (mask : ℕ → E → ℝ) (c : Fin 2) (n : ℕ) (x : E) : primaryWave s pref d lam u L χ T mask c n x = GaussianTailFlat.profile (χ n x).2 • uncutPrimaryWave s pref d lam u L χ T mask c n x

The slot cutoff occurs exactly once. This identity matches a linear-wave coefficient's external withCutoff operation to the physical primary.

theorem NavierStokes.PrimaryPulseBounds.uncutPrimaryWave_waveClass {Q E : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) (D : PhaseJetBounds.Domain ℕ Q) (pref : Fin 2 → ℕ → ℝ) (d : Fin 2 → ℕ → PrimaryODE.FrameData Q) (lam u L : Fin 2 → ℕ → ℝ) (χ : ℕ → E → Q × ℝ) (T : ℕ → E → SmoothCovariance.Vec2) (mask : ℕ → E → ℝ) (hscale : ∀ (n : ℕ), D.scale n = s.slow n) (hχ : PhaseJetBounds.PolynomialJets (phaseDomain s) χ) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, χ n x ∈ D.carrier n ×ˢ Set.Ioo 0 1) (hpref : ∀ (c : Fin 2), PhaseJetBounds.PolynomialJets D fun (n : ℕ) (x : Q) => pref c n) (hpulse : ∀ (c : Fin 2), EnvelopeJets (productDomain D (fun (x : ℕ) => Set.Ioo 0 1) ⋯) (fun (n : ℕ) (z : Q × ℝ) => referenceP (lam c n) (u c n) (L c n) (L c n * z.2)) fun (n : ℕ) => normalizedPulse (d c n) (lam c n) (u c n) (L c n)) (hlam : ∀ (c : Fin 2) (n : ℕ), 0 < lam c n) (hu : ∀ (c : Fin 2) (n : ℕ), 0 < u c n) (hL : ∀ (c : Fin 2) (n : ℕ), 0 < L c n) (hT : ∀ (i : Fin 2), WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : E) => T n x i) (hmask : PhaseJetBounds.PolynomialJets (phaseDomain s) mask) {b M a : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (ha : 0 < a) (hdet : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ |Matrix.det (normalizedMatrix (√(s.slow n)) (chartCovariance pref d lam u L χ n x))|) (hentry : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |√(s.slow n) * chartCovariance pref d lam u L χ n x i j| ≤ M) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (j : Fin 2), a * s.zeta x ≤ SmoothCovariance.weights (chartCovariance pref d lam u L χ n x) (T n x) j) (c : Fin 2) : WeightedClasses.WaveClass s (fun (n : ℕ) (x : E) => referenceP (lam c n) (u c n) (L c n) (L c n * (χ n x).2)) (1 / 2) (uncutPrimaryWave s pref d lam u L χ T mask c)

The same quantitative estimate before applying the external Gaussian slot cutoff. This is the class used for the homogeneous principal equation.