The actual Gaussian slot-cutoff errors

The profile is a constructed smooth bump, with the plateau and support radii from Section 8.2. No error field is set to zero: local vanishing on the plateau, the Gaussian bound off that plateau, and higher Leibniz estimates are used.

noncomputable def NavierStokes.GaussianTailFlat.profileBump : ContDiffBump (1 / 2)

The fixed profile has plateau radius 1/5 and support radius 1/3.

Equations

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

noncomputable def NavierStokes.GaussianTailFlat.profile : ℝ → ℝ

Profile, given by profileBump.

Equations

• NavierStokes.GaussianTailFlat.profile = ↑NavierStokes.GaussianTailFlat.profileBump

theorem NavierStokes.GaussianTailFlat.profile_contDiff : ContDiff ℝ (↑⊤) profile

theorem NavierStokes.GaussianTailFlat.profile_mem_Icc (v : ℝ) : profile v ∈ Set.Icc 0 1

theorem NavierStokes.GaussianTailFlat.profile_one {v : ℝ} (hv : |v - 1 / 2| ≤ 1 / 5) : profile v = 1

theorem NavierStokes.GaussianTailFlat.profile_zero {v : ℝ} (hv : 1 / 3 ≤ |v - 1 / 2|) : profile v = 0

theorem NavierStokes.GaussianTailFlat.profile_eventually_one {v : ℝ} (hv : |v - 1 / 2| < 1 / 5) : profile =ᶠ[nhds v] fun (x : ℝ) => 1

theorem NavierStokes.GaussianTailFlat.profile_eventually_zero {v : ℝ} (hv : 1 / 3 < |v - 1 / 2|) : profile =ᶠ[nhds v] fun (x : ℝ) => 0

theorem NavierStokes.GaussianTailFlat.profile_iteratedDeriv_support (m : ℕ) : Function.support (iteratedDeriv (m + 1) profile) ⊆ {v : ℝ | 1 / 5 ≤ |v - 1 / 2| ∧ |v - 1 / 2| ≤ 1 / 3}

theorem NavierStokes.GaussianTailFlat.profile_iteratedDeriv_compact (m : ℕ) : HasCompactSupport (iteratedDeriv m profile)

theorem NavierStokes.GaussianTailFlat.profile_jet_bounded (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (v : ℝ), ‖iteratedFDeriv ℝ m profile v‖ ≤ C

noncomputable def NavierStokes.GaussianTailFlat.slotCutoff (L v : ℝ) : ℝ

Slot cutoff, given by profile (v / L).

Equations

• NavierStokes.GaussianTailFlat.slotCutoff L v = NavierStokes.GaussianTailFlat.profile (v / L)

theorem NavierStokes.GaussianTailFlat.slotCutoff_contDiff (L : ℝ) : ContDiff ℝ (↑⊤) (slotCutoff L)

theorem NavierStokes.GaussianTailFlat.slotCutoff_deriv (L v : ℝ) : deriv (slotCutoff L) v = L⁻¹ * deriv profile (v / L)

theorem NavierStokes.GaussianTailFlat.slot_normalized_distance {L : ℝ} (hL : 0 < L) (v : ℝ) : |v / L - 1 / 2| = |v - L / 2| / L

theorem NavierStokes.GaussianTailFlat.slotCutoff_one {L v : ℝ} (hL : 0 < L) (hv : |v - L / 2| ≤ L / 5) : slotCutoff L v = 1

theorem NavierStokes.GaussianTailFlat.slotCutoff_zero {L v : ℝ} (hL : 0 < L) (hv : L / 3 ≤ |v - L / 2|) : slotCutoff L v = 0

theorem NavierStokes.GaussianTailFlat.slotCutoff_deriv_support {L v : ℝ} (hL : 0 < L) (hv : deriv (slotCutoff L) v ≠ 0) : L / 5 ≤ |v - L / 2| ∧ |v - L / 2| ≤ L / 3

The derivative error is supported strictly inside the slot and outside the central plateau; in particular it lies near the entry or exit.

theorem NavierStokes.GaussianTailFlat.gaussian_off_plateau {c L v : ℝ} (hc : 0 ≤ c) (hL : 0 < L) (hv : L / 5 ≤ |v - L / 2|) : Real.exp (-c * (v - L / 2) ^ 2 / L) ≤ Real.exp (-(c / 25) * L)

The precise Gaussian tail bound uses the full plateau radius.

theorem NavierStokes.GaussianTailFlat.reference_envelope_off_plateau {lam u L v : ℝ} (hlam : 0 < lam) (hu : 0 < u) (hL : 0 < L) (hv : v ∈ Set.Icc 0 L) (htail : L / 5 ≤ |v - L / 2|) : GaussianEnvelope.envelope (GaussianEnvelope.referenceRate lam u L) (L / 2) v ≤ Real.exp (-(u * GaussianEnvelope.referenceMinSlope lam u / 50) * L)

theorem NavierStokes.GaussianTailFlat.sqrt_edge (c x : ℝ) : √(FlatCutoff.edge c x) = FlatCutoff.edge (c / 2) x

The square root of the actual flat edge is another member of that family.

theorem NavierStokes.GaussianTailFlat.sqrt_zeta (cL cR R x : ℝ) : √(WeightedRadialPrimitive.zeta cL cR R x) = WeightedRadialPrimitive.zeta (cL / 2) (cR / 2) R x

theorem NavierStokes.GaussianTailFlat.sqrt_zeta_inverse_power_bounded {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (R : ℝ) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ Set.Ioo 0 R, √(WeightedRadialPrimitive.zeta cL cR R x) * max 1 (WeightedRadialPrimitive.delta R x)⁻¹ ^ k ≤ C

A single constant covers the entire slow shell, including approach to either edge. This is derived from the constructed FlatCutoff.edge.

Exponential decay along the actual bands

theorem NavierStokes.GaussianTailFlat.polynomial_exp_bound {c : ℝ} (hc : 0 < c) (p : ℕ) {x : ℝ} (hx : 0 ≤ x) : (1 + x) ^ p * Real.exp (-c * x) ≤ ↑p.factorial / c ^ p * Real.exp c

An elementary global bound, including the finite initial part of a sequence.

theorem NavierStokes.GaussianTailFlat.Q_rpow_eq_exp (N : ℝ) (n : ℕ) : ChartScales.Q n ^ N = Real.exp (-(N * Real.log 2) * ↑n)

theorem NavierStokes.GaussianTailFlat.gaussian_beats_Q_power {c : ℝ} (hc : 0 < c) (p : ℕ) (N : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), (1 + ChartScales.S n) ^ p * Real.exp (-c * ChartScales.S n) ≤ C * ChartScales.Q n ^ N

Every polynomial in S=n² times a Gaussian tail is bounded by every real power of the actual dyadic Q=2⁻ⁿ. No asymptotic surrogate is used.

theorem NavierStokes.GaussianTailFlat.gaussian_length_comparison {c κ L S : ℝ} (hc : 0 ≤ c) (hL : κ * S ≤ L) : Real.exp (-(c / 25) * L) ≤ Real.exp (-(c * κ / 25) * S)

theorem NavierStokes.GaussianTailFlat.fixed_power_gaussian_bound {c : ℝ} (hc : 0 < c) (r : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), ChartScales.Q n ^ r * Real.exp (-c * ChartScales.S n) ≤ C * Real.exp (-(c / 2) * ChartScales.S n)

A fixed power loss consumes only half of a Gaussian tail.

The actual cutoff products and all their stripped derivatives

theorem NavierStokes.GaussianTailFlat.finite_jet_bounds {g : ℝ → ℝ} (hb : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), ‖iteratedFDeriv ℝ j g x‖ ≤ C) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ j ≤ m, ∀ (x : ℝ), ‖iteratedFDeriv ℝ j g x‖ ≤ C

theorem NavierStokes.GaussianTailFlat.profileDeriv_contDiff : ContDiff ℝ (↑⊤) (deriv profile)

theorem NavierStokes.GaussianTailFlat.profileDeriv_jet_bounded (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), ‖iteratedFDeriv ℝ m (deriv profile) x‖ ≤ C

theorem NavierStokes.GaussianTailFlat.omittedProfile_contDiff : ContDiff ℝ ↑⊤ fun (x : ℝ) => 1 - profile x

theorem NavierStokes.GaussianTailFlat.omittedProfile_jet_bounded (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), ‖iteratedFDeriv ℝ m (fun (y : ℝ) => 1 - profile y) x‖ ≤ C

theorem NavierStokes.GaussianTailFlat.norm_affine_comp_jet_le {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {g : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (A : D →L[ℝ] ℝ) (b : ℝ) (x : D) (j : ℕ) : ‖iteratedFDeriv ℝ j (fun (y : D) => g (b + A y)) x‖ ≤ ‖iteratedFDeriv ℝ j g (b + A x)‖ * ‖A‖ ^ j

theorem NavierStokes.GaussianTailFlat.affine_profile_memClass {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) {g : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hb : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), ‖iteratedFDeriv ℝ j g x‖ ≤ C) (A : ℕ → D →L[ℝ] ℝ) (b : ℕ → ℝ) (hA : ∃ (K : ℝ), 1 ≤ K ∧ ∃ (p : ℕ), ∀ (n : ℕ), ‖A n‖ ≤ K * s.slow n ^ p) : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => g (b n + (A n) x)

The offset never enters the bound. Thus translated copies have the same constants, even when their centers differ by arbitrarily many periods.

noncomputable def NavierStokes.GaussianTailFlat.cutoffError {D : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : ℝ) (θ : D → ℝ) (u f : D → E) (x : D) : E

The two excluded errors, retained as actual functions. θ is the normalized slot coordinate v/L.

Equations

• NavierStokes.GaussianTailFlat.cutoffError L θ u f x = (L⁻¹ * deriv NavierStokes.GaussianTailFlat.profile (θ x)) • u x + (1 - NavierStokes.GaussianTailFlat.profile (θ x)) • f x

theorem NavierStokes.GaussianTailFlat.cutoffError_eq_slot {D : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : ℝ) (v : D → ℝ) (u f : D → E) (x : D) : cutoffError L (fun (y : D) => v y / L) u f x = deriv (slotCutoff L) (v x) • u x + (1 - slotCutoff L (v x)) • f x

theorem NavierStokes.GaussianTailFlat.cutoffError_contDiffOn {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} (L : ℝ) {θ : D → ℝ} {u f : D → E} (hθ : ContDiffOn ℝ (↑⊤) θ U) (hu : ContDiffOn ℝ (↑⊤) u U) (hf : ContDiffOn ℝ (↑⊤) f U) : ContDiffOn ℝ (↑⊤) (cutoffError L θ u f) U

theorem NavierStokes.GaussianTailFlat.cutoffError_eventually_zero {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] [NormedSpace ℝ E] (L : ℝ) {θ : D → ℝ} (u f : D → E) {x : D} (hθ : ContinuousAt θ x) (hx : |θ x - 1 / 2| < 1 / 5) : cutoffError L θ u f =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.GaussianTailFlat.cutoffError_jet_zero_on_plateau {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (L : ℝ) {θ : D → ℝ} (u f : D → E) {x : D} (hθ : ContinuousAt θ x) (hx : |θ x - 1 / 2| < 1 / 5) (j : ℕ) : iteratedFDeriv ℝ j (cutoffError L θ u f) x = 0

theorem NavierStokes.GaussianTailFlat.cutoffError_mem_wave {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} {u f : ℕ → D → E} (hu : WeightedClasses.WaveClass s P α u) (hf : WeightedClasses.WaveClass s P α f) (L : ℕ → ℝ) (A : ℕ → D →L[ℝ] ℝ) (b : ℕ → ℝ) (hA : ∃ (K : ℝ), 1 ≤ K ∧ ∃ (p : ℕ), ∀ (n : ℕ), ‖A n‖ ≤ K * s.slow n ^ p) (hL : WeightedClasses.BandBound s 0 fun (n : ℕ) => (L n)⁻¹) : WeightedClasses.WaveClass s P α fun (n : ℕ) => cutoffError (L n) (fun (x : D) => b n + (A n) x) (u n) (f n)

This class bound is derived by all-order Leibniz, from the actual wave and source classes and the constructed cutoff profile.

structure NavierStokes.GaussianTailFlat.FlatEdges {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) : Type u_1

A slow weight controlled by the actual two-sided exponential-flat edge. The comparison permits additional cutoffs of size at most one.

• leftDecay : ℝ

  Left decay of FlatEdges, of type ℝ.

• rightDecay : ℝ

  Right decay of FlatEdges, of type ℝ.

• left_pos : 0 < self.leftDecay
• right_pos : 0 < self.rightDecay
• width : ℝ

  Width of FlatEdges, of type ℝ.

• position : D → ℝ

  Position of FlatEdges, of type D → ℝ.

• position_mem (x : D) : x ∈ s.domain → self.position x ∈ Set.Ioo 0 self.width
• delta_eq (x : D) : x ∈ s.domain → s.delta x = WeightedRadialPrimitive.delta self.width (self.position x)
• zeta_le (x : D) : x ∈ s.domain → s.zeta x ≤ WeightedRadialPrimitive.zeta self.leftDecay self.rightDecay self.width (self.position x)

theorem NavierStokes.GaussianTailFlat.FlatEdges.uniform_weight {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (e : FlatEdges s) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ s.domain, √(s.zeta x) * max 1 (s.delta x)⁻¹ ^ k ≤ C

structure NavierStokes.GaussianTailFlat.BandScaleControl {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) : Type

Only the actual scale identity and a polynomial slow-scale upper bound are used. The exponent may be any real number.

• power : ℝ

  Power of BandScaleControl, of type ℝ.

• epsilon_eq (n : ℕ) : s.epsilon n = ChartScales.Q n ^ self.power
• boundConstant : ℝ

  Bound constant of BandScaleControl, of type ℝ.

• constant_one_le : 1 ≤ self.boundConstant
• degree : ℕ

  Degree of BandScaleControl, of type ℕ.

• slow_le (n : ℕ) : s.slow n ≤ self.boundConstant * (1 + ChartScales.S n) ^ self.degree

structure NavierStokes.GaussianTailFlat.SlotFamily {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) : Type u_1

Native slot data before restriction to the physical graph. The cutoff coordinate is affine, and no spatial derivatives of a band index occur.

• length : ℕ → ℝ

  Length of SlotFamily, of type ℕ → ℝ.

• length_pos (n : ℕ) : 0 < self.length n
• linear : ℕ → D →L[ℝ] ℝ

  Linear of SlotFamily, of type ℕ → D →L[ℝ] ℝ.

• offset : ℕ → ℝ

  Offset of SlotFamily, of type ℕ → ℝ.

• linear_bound : ∃ (K : ℝ), 1 ≤ K ∧ ∃ (p : ℕ), ∀ (n : ℕ), ‖self.linear n‖ ≤ K * s.slow n ^ p
• inverse_length_bound : WeightedClasses.BandBound s 0 fun (n : ℕ) => (self.length n)⁻¹
• lengthScale : ℝ

  Length scale of SlotFamily, of type ℝ.

• length_scale_pos : 0 < self.lengthScale
• length_lower (n : ℕ) : self.lengthScale * ChartScales.S n ≤ self.length n

noncomputable def NavierStokes.GaussianTailFlat.SlotFamily.coordinate {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (g : SlotFamily s) (n : ℕ) (x : D) : ℝ

Coordinate, given by g.offset n + g.linear n x.

Equations

• g.coordinate n x = g.offset n + (g.linear n) x

noncomputable def NavierStokes.GaussianTailFlat.SlotFamily.cutoff {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (g : SlotFamily s) (n : ℕ) (x : D) : ℝ

Cutoff, given by profile (g.coordinate n x).

Equations

• g.cutoff n x = NavierStokes.GaussianTailFlat.profile (g.coordinate n x)

noncomputable def NavierStokes.GaussianTailFlat.SlotFamily.error {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (u f : ℕ → D → E) (n : ℕ) : D → E

Error, given by cutoffError (g.length n) (g.coordinate n) (u n) (f n).

Equations

• g.error u f n = NavierStokes.GaussianTailFlat.cutoffError (g.length n) (g.coordinate n) (u n) (f n)

theorem NavierStokes.GaussianTailFlat.SlotFamily.coordinate_contDiff {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (g : SlotFamily s) (n : ℕ) : ContDiff ℝ (↑⊤) (g.coordinate n)

theorem NavierStokes.GaussianTailFlat.SlotFamily.cutoff_memClass {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (g : SlotFamily s) : WeightedClasses.UnweightedClass s 0 g.cutoff

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_mem_wave {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) {P : ℕ → D → ℝ} {α : ℝ} {u f : ℕ → D → E} (hu : WeightedClasses.WaveClass s P α u) (hf : WeightedClasses.WaveClass s P α f) : WeightedClasses.WaveClass s P α (g.error u f)

theorem NavierStokes.GaussianTailFlat.SlotFamily.cutoff_directional {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (g : SlotFamily s) (n : ℕ) (x w : D) (hw : (g.linear n) w = (g.length n)⁻¹) : (fderiv ℝ (g.cutoff n) x) w = (g.length n)⁻¹ * deriv profile (g.coordinate n x)

The derivative in a direction with D(v)=1 is the exact coefficient used in the retained cutoff error, because v=L θ.

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_eq_directional {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (u f : ℕ → D → E) (n : ℕ) (x w : D) (hw : (g.linear n) w = (g.length n)⁻¹) : g.error u f n x = (fderiv ℝ (g.cutoff n) x) w • u n x + (1 - g.cutoff n x) • f n x

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_gaussian_bound {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (edges : FlatEdges s) (scales : BandScaleControl s) {P : ℕ → D → ℝ} {α c : ℝ} {u f : ℕ → D → E} (hu : WeightedClasses.WaveClass s P α u) (hf : WeightedClasses.WaveClass s P α f) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (d : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (g.error u f n) x‖ ≤ C * (1 + ChartScales.S n) ^ d * Real.exp (-(c * g.lengthScale / 50) * ChartScales.S n)

Uniform polynomial-times-Gaussian bound for the two exact cutoff products. The only field estimates assumed are the original wave/source classes and the Gaussian upper bound for their common envelope.

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_stripped_bound {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (edges : FlatEdges s) (scales : BandScaleControl s) {P : ℕ → D → ℝ} {α c : ℝ} {u f : ℕ → D → E} (hu : WeightedClasses.WaveClass s P α u) (hf : WeightedClasses.WaveClass s P α f) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (m : ℕ) (N : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (g.error u f n) x‖ ≤ C * ChartScales.Q n ^ N

Every prescribed dyadic power is gained, for all actual stripped jets.

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_all_gains {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (edges : FlatEdges s) (scales : BandScaleControl s) {P : ℕ → D → ℝ} {α c : ℝ} {u f : ℕ → D → E} (hu : WeightedClasses.WaveClass s P α u) (hf : WeightedClasses.WaveClass s P α f) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (N : ℝ) : WeightedClasses.UnweightedClass s N (g.error u f)

The excluded field belongs to every unweighted decay class. Its bound has polynomial degree zero, so no inverse-edge factor remains hidden.

theorem NavierStokes.GaussianTailFlat.native_slot_length_lower (r0 h : ℝ) (hr0 : 0 < r0) (hh : 0 ≤ h) : ∃ (κ : ℝ), 0 < κ ∧ ∀ (n : ℕ), κ * (1 + ChartScales.S n) ≤ ChartScales.slotLength r0 h n

The true native slot length is uniformly comparable from below to 1+n²; finitely many small bands are included by a finite minimum.

noncomputable def NavierStokes.GaussianTailFlat.actualSlotFamily {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (r0 h : ℝ) (hr0 : 0 < r0) (hh : 0 ≤ h) (η : D →L[ℝ] ℝ) (center : ℕ → ℝ) : SlotFamily s

Actual native slots. η is the fixed longitudinal coordinate functional; only the centers depend on the band. Normalizing v by L cancels ci.

Equations

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

@[simp]

theorem NavierStokes.GaussianTailFlat.actualSlotFamily_length {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (r0 h : ℝ) (hr0 : 0 < r0) (hh : 0 ≤ h) (η : D →L[ℝ] ℝ) (center : ℕ → ℝ) (n : ℕ) : (actualSlotFamily s r0 h hr0 hh η center).length n = ChartScales.slotLength r0 h n

theorem NavierStokes.GaussianTailFlat.actualSlotFamily_coordinate {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (r0 h : ℝ) (hr0 : 0 < r0) (hh : 0 ≤ h) (η : D →L[ℝ] ℝ) (center : ℕ → ℝ) (n : ℕ) (x : D) : (actualSlotFamily s r0 h hr0 hh η center).coordinate n x = (η x - center n + r0) / (2 * r0)

theorem NavierStokes.GaussianTailFlat.actualSlotFamily_cutoff {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (r0 h : ℝ) (hr0 : 0 < r0) (hh : 0 ≤ h) (η : D →L[ℝ] ℝ) (center : ℕ → ℝ) (n : ℕ) (x : D) : (actualSlotFamily s r0 h hr0 hh η center).cutoff n x = slotCutoff (ChartScales.slotLength r0 h n) ((η x - center n + r0) / ChartScales.timeCoefficient h n)

noncomputable def NavierStokes.GaussianTailFlat.referenceSlotEnvelope (lam u L θ : ℝ) : ℝ

The reference Gaussian envelope, extended by zero away from its slot. This is a weight, not a redefinition of either retained error.

Equations

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

theorem NavierStokes.GaussianTailFlat.referenceSlotEnvelope_bound {lam u L : ℝ} (hlam : 0 < lam) (hu : 0 < u) (hL : 0 < L) (θ : ℝ) : referenceSlotEnvelope lam u L θ ≤ Real.exp (-(u * GaussianEnvelope.referenceMinSlope lam u / 2) * (θ - 1 / 2) ^ 2 * L)

Restriction to the actual physical graph and carrier

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_contDiff {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) {u f : ℕ → D → E} (hu : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (u n)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (n : ℕ) : ContDiff ℝ (↑⊤) (g.error u f n)

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_contDiff_of_slot {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) {u f : ℕ → D → E} (hu : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u n) {x : D | g.coordinate n x ∈ Set.Ioo 0 1}) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (n : ℕ) : ContDiff ℝ (↑⊤) (g.error u f n)

The fundamental need only be smooth in the open slot. Away from that slot the exact error agrees locally with the smooth source. This avoids any smoothness assertion for a clamped ODE extension across its endpoints.

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_physical_bound {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData PhysicalGraphBounds.LiftPoint} (g : SlotFamily s) (edges : FlatEdges s) (scales : BandScaleControl s) {P : ℕ → PhysicalGraphBounds.LiftPoint → ℝ} {α c : ℝ} {u f : ℕ → PhysicalGraphBounds.LiftPoint → E} (hu : WeightedClasses.WaveClass s P α u) (hf : WeightedClasses.WaveClass s P α f) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (hu_smooth : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u n) {x : PhysicalGraphBounds.LiftPoint | g.coordinate n x ∈ Set.Ioo 0 1}) (hf_smooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (m : ℕ) (N : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (p : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) p ∈ PhysicalGraphBounds.annulus a b → |p.1| ≤ 1 → PhysicalGraphBounds.physicalLift h n p ∈ s.domain → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ‖iteratedFDeriv ℝ m (g.error u f n ∘ PhysicalGraphBounds.physicalLift h n) p‖ ≤ C * q ^ N

Every fixed physical derivative retains arbitrarily high decay powers. The loss is supplied by the proved physical graph theorem.

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_physical_isBigO {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData PhysicalGraphBounds.LiftPoint} (g : SlotFamily s) (edges : FlatEdges s) (scales : BandScaleControl s) {P : ℕ → PhysicalGraphBounds.LiftPoint → ℝ} {α c : ℝ} {u f : ℕ → PhysicalGraphBounds.LiftPoint → E} (hu : WeightedClasses.WaveClass s P α u) (hf : WeightedClasses.WaveClass s P α f) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (hu_smooth : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u n) {x : PhysicalGraphBounds.LiftPoint | g.coordinate n x ∈ Set.Ioo 0 1}) (hf_smooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (p : ℕ → ProblemStatement.SpaceTime) (hp : ∀ (n : ℕ), 4 ≤ n → (PhysicalGraphBounds.scaledRadial n) (p n) ∈ PhysicalGraphBounds.annulus a b ∧ |(p n).1| ≤ 1 ∧ PhysicalGraphBounds.physicalLift h n (p n) ∈ s.domain) (m : ℕ) (N : ℝ) : (fun (n : ℕ) => iteratedFDeriv ℝ m (g.error u f n ∘ PhysicalGraphBounds.physicalLift h n) (p n)) =O[Filter.atTop] fun (n : ℕ) => ChartScales.Q n ^ N

Big-O formulation along any sequence of physical points in the controlled annulus and slow domain. The derivative order and power are arbitrary.

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_carrier_physical_bound {s : WeightedClasses.StripData PhysicalGraphBounds.LiftPoint} (g : SlotFamily s) (edges : FlatEdges s) (scales : BandScaleControl s) {P : ℕ → PhysicalGraphBounds.LiftPoint → ℝ} {α c : ℝ} {u f : ℕ → PhysicalGraphBounds.LiftPoint → ℂ} (hu : WeightedClasses.WaveClass s P α u) (hf : WeightedClasses.WaveClass s P α f) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (hu_smooth : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u n) {x : PhysicalGraphBounds.LiftPoint | g.coordinate n x ∈ Set.Ioo 0 1}) (hf_smooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) {h a b B e H : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (hB : 1 ≤ B) (he : 0 ≤ e) (hH : 0 ≤ H) (m : ℕ) (N : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (p : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) p ∈ PhysicalGraphBounds.annulus a b → |p.1| ≤ 1 → PhysicalGraphBounds.physicalLift h n p ∈ s.domain → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (Φ : PhysicalGraphBounds.LiftPoint → ℝ) (j : ℤ), ContDiff ℝ (↑⊤) Φ → |↑j| ≤ H → (∀ i ≤ m, ‖iteratedFDeriv ℝ i Φ (PhysicalGraphBounds.physicalLift h n p)‖ ≤ B * ChartScales.S n ^ e * ChartScales.Q n ^ (-1)) → ‖iteratedFDeriv ℝ m ((fun (y : PhysicalGraphBounds.LiftPoint) => g.error u f n y * PhysicalGraphBounds.character (↑(ChartScales.carrier h n) * ↑j) (Φ y)) ∘ PhysicalGraphBounds.physicalLift h n) p‖ ≤ C * q ^ N

The same result for the actual oscillatory carrier. The phase estimates are the primitive estimates consumed by carrier_class_physical_bound.

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_native_carrier_physical_bound {s : WeightedClasses.StripData PhysicalGraphBounds.LiftPoint} (g : SlotFamily s) (edges : FlatEdges s) (scales : BandScaleControl s) {Penv : ℕ → PhysicalGraphBounds.LiftPoint → ℝ} {α c : ℝ} {u f : ℕ → PhysicalGraphBounds.LiftPoint → ℂ} (hu : WeightedClasses.WaveClass s Penv α u) (hf : WeightedClasses.WaveClass s Penv α f) (hc : 0 < c) (hPenv : ∀ (n : ℕ), ∀ x ∈ s.domain, Penv n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (hu_smooth : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u n) {x : PhysicalGraphBounds.LiftPoint | g.coordinate n x ∈ Set.Ioo 0 1}) (hf_smooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) {h a b Z r0 P B dBase H : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hB : 1 ≤ B) (hdBase : 0 ≤ dBase) (hH : 0 ≤ H) (m : ℕ) (N : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → PhysicalGraphBounds.physicalLift h n w ∈ s.domain → ‖PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h n w)‖ ≤ Z → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (chart : PolarCharts.Index) (center : PhysicalGraphBounds.Plane) (p pz x0 : ℝ), |p| ≤ P → |pz| ≤ P → |x0| ≤ P → |PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h n w - center)| ≤ r0 → ∀ (F G : PhysicalGraphBounds.Slow → ℝ) (j : ℤ), ContDiff ℝ (↑⊤) F → ContDiff ℝ (↑⊤) G → |↑j| ≤ H → (∀ i ≤ m, ‖iteratedFDeriv ℝ i F (PhysicalGraphBounds.slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h n) center r0 (PhysicalGraphBounds.physicalLift h n w)).1‖ ≤ B * ChartScales.S n ^ dBase) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i G (PhysicalGraphBounds.slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h n) center r0 (PhysicalGraphBounds.physicalLift h n w)).1‖ ≤ B * ChartScales.S n ^ dBase) → ‖iteratedFDeriv ℝ m ((fun (y : PhysicalGraphBounds.LiftPoint) => g.error u f n y * PhysicalGraphBounds.character (↑(ChartScales.carrier h n) * ↑j) (PhysicalGraphBounds.liftedPhase (PolarCharts.chart a chart) h n center r0 p pz x0 F G y)) ∘ PhysicalGraphBounds.physicalLift h n) w‖ ≤ C * q ^ N

Version with the manuscript's actual native phase, polar charts and rounded carrier. No phase-derivative hypothesis replaces the base-field jets.

The two summands separately

noncomputable def NavierStokes.GaussianTailFlat.SlotFamily.derivativeError {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (u : ℕ → D → E) (n : ℕ) (x : D) : E

Derivative error, given by ((g.length n)⁻¹ * deriv profile (g.coordinate n x)) • u n x.

Equations

• g.derivativeError u n x = ((g.length n)⁻¹ * deriv NavierStokes.GaussianTailFlat.profile (g.coordinate n x)) • u n x

noncomputable def NavierStokes.GaussianTailFlat.SlotFamily.omittedSource {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (f : ℕ → D → E) (n : ℕ) (x : D) : E

Omitted source, given by (1 - profile (g.coordinate n x)) • f n x.

Equations

• g.omittedSource f n x = (1 - NavierStokes.GaussianTailFlat.profile (g.coordinate n x)) • f n x

theorem NavierStokes.GaussianTailFlat.SlotFamily.error_eq_sum {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (u f : ℕ → D → E) (n : ℕ) (x : D) : g.error u f n x = g.derivativeError u n x + g.omittedSource f n x

theorem NavierStokes.GaussianTailFlat.SlotFamily.derivativeError_jet_support {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (u : ℕ → D → E) (n j : ℕ) : Function.support (iteratedFDeriv ℝ j (g.derivativeError u n)) ⊆ {x : D | 1 / 5 ≤ |g.coordinate n x - 1 / 2| ∧ |g.coordinate n x - 1 / 2| ≤ 1 / 3}

theorem NavierStokes.GaussianTailFlat.SlotFamily.derivativeError_jet_near_ends {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (u : ℕ → D → E) (n j : ℕ) {x : D} (hx : iteratedFDeriv ℝ j (g.derivativeError u n) x ≠ 0) : g.coordinate n x ∈ Set.Icc (1 / 6) (3 / 10) ∪ Set.Icc (7 / 10) (5 / 6)

Both transition collars, with the exact normalized slot endpoints. This holds for every actual parameter jet, without any regularity needed of u where the multiplier vanishes on a neighborhood.

theorem NavierStokes.GaussianTailFlat.SlotFamily.omittedSource_jet_support {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (f : ℕ → D → E) (n j : ℕ) : Function.support (iteratedFDeriv ℝ j (g.omittedSource f n)) ⊆ {x : D | 1 / 5 ≤ |g.coordinate n x - 1 / 2|}

theorem NavierStokes.GaussianTailFlat.SlotFamily.derivativeError_gaussian_bound {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (edges : FlatEdges s) (scales : BandScaleControl s) {P : ℕ → D → ℝ} {α c : ℝ} {u : ℕ → D → E} (hu : WeightedClasses.WaveClass s P α u) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (d : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (g.derivativeError u n) x‖ ≤ C * (1 + ChartScales.S n) ^ d * Real.exp (-(c * g.lengthScale / 50) * ChartScales.S n)

theorem NavierStokes.GaussianTailFlat.SlotFamily.omittedSource_gaussian_bound {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (edges : FlatEdges s) (scales : BandScaleControl s) {P : ℕ → D → ℝ} {α c : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.WaveClass s P α f) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (d : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (g.omittedSource f n) x‖ ≤ C * (1 + ChartScales.S n) ^ d * Real.exp (-(c * g.lengthScale / 50) * ChartScales.S n)

theorem NavierStokes.GaussianTailFlat.SlotFamily.reference_error_all_gains {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} (g : SlotFamily s) (edges : FlatEdges s) (scales : BandScaleControl s) {lam v α : ℝ} (hlam : 0 < lam) (hv : 0 < v) {u f : ℕ → D → E} (hu : WeightedClasses.WaveClass s (fun (n : ℕ) (x : D) => referenceSlotEnvelope lam v (g.length n) (g.coordinate n x)) α u) (hf : WeightedClasses.WaveClass s (fun (n : ℕ) (x : D) => referenceSlotEnvelope lam v (g.length n) (g.coordinate n x)) α f) (N : ℝ) : WeightedClasses.UnweightedClass s N (g.error u f)

Full all-gain specialization to the actually constructed reference Gaussian envelope. Only the proved original wave classes are inputs.