Uniform applicability of the angular reset

The actual two-bump moment system is uniformly invertible down to lam = 0. The outgoing uniform wait damps the angular-history discrepancy and its parameter derivatives before this nonlinear repair is applied.

A pressure-neutral angular-moment reset

Two identical translated smooth relative bumps repair the angular moment while preserving the pressure integral exactly. The actual two-row derivative matrix is proved nonsingular, and the small smooth nonlinear branch is constructed.

@[reducible, inline]

abbrev NavierStokes.AngularMomentReset.Coeff : Type

Coefficient: an abbreviation for Fin 2 → ℝ.

Equations

• NavierStokes.AngularMomentReset.Coeff = (Fin 2 → ℝ)

noncomputable def NavierStokes.AngularMomentReset.template : ℝ → ℝ

Template, given by LocalizedMomentRepair.bump (-3 / 10) (3 / 10).

Equations

• NavierStokes.AngularMomentReset.template = NavierStokes.LocalizedMomentRepair.bump (-3 / 10) (3 / 10)

noncomputable def NavierStokes.AngularMomentReset.bump (j : Fin 2) (y : ℝ) : ℝ

Bump, given by template (y - 2 * (j.val : ℝ)).

Equations

• NavierStokes.AngularMomentReset.bump j y = NavierStokes.AngularMomentReset.template (y - 2 * ↑↑j)

theorem NavierStokes.AngularMomentReset.template_contDiff : ContDiff ℝ (↑⊤) template

theorem NavierStokes.AngularMomentReset.template_at_zero : template 0 = 1

theorem NavierStokes.AngularMomentReset.template_support : Function.support template ⊆ Set.Icc (-3 / 20) (3 / 20)

theorem NavierStokes.AngularMomentReset.template_hasCompactSupport : HasCompactSupport template

theorem NavierStokes.AngularMomentReset.bump_contDiff (j : Fin 2) : ContDiff ℝ (↑⊤) (bump j)

theorem NavierStokes.AngularMomentReset.bump_nonneg (j : Fin 2) (y : ℝ) : 0 ≤ bump j y

theorem NavierStokes.AngularMomentReset.bump_le_one (j : Fin 2) (y : ℝ) : bump j y ≤ 1

theorem NavierStokes.AngularMomentReset.bump_support (j : Fin 2) : Function.support (bump j) ⊆ Set.Icc (2 * ↑↑j - 3 / 20) (2 * ↑↑j + 3 / 20)

theorem NavierStokes.AngularMomentReset.bump_hasCompactSupport (j : Fin 2) : HasCompactSupport (bump j)

theorem NavierStokes.AngularMomentReset.bumps_disjoint (y : ℝ) : bump 0 y * bump 1 y = 0

noncomputable def NavierStokes.AngularMomentReset.moment (s : ℝ) : ℝ

Moment, given by ∫ y, Real.exp (s * y) * template y.

Equations

• NavierStokes.AngularMomentReset.moment s = ∫ (y : ℝ), Real.exp (s * y) * NavierStokes.AngularMomentReset.template y

theorem NavierStokes.AngularMomentReset.weighted_bump_integrable (s : ℝ) (j : Fin 2) : MeasureTheory.Integrable (fun (y : ℝ) => Real.exp (s * y) * bump j y) MeasureTheory.volume

theorem NavierStokes.AngularMomentReset.weighted_bump_sq_integrable (s : ℝ) (j : Fin 2) : MeasureTheory.Integrable (fun (y : ℝ) => Real.exp (s * y) * bump j y ^ 2) MeasureTheory.volume

theorem NavierStokes.AngularMomentReset.moment_pos (s : ℝ) : 0 < moment s

theorem NavierStokes.AngularMomentReset.bump_moment (s : ℝ) (j : Fin 2) : ∫ (y : ℝ), Real.exp (s * y) * bump j y = Real.exp (s * (2 * ↑↑j)) * moment s

Translation multiplies an exponential bump moment by its exact exponential factor.

def NavierStokes.AngularMomentReset.angularSlope (lam : ℝ) : ℝ

Angular slope, given by 1 - lam.

Equations

• NavierStokes.AngularMomentReset.angularSlope lam = 1 - lam

def NavierStokes.AngularMomentReset.pressureSlope (lam : ℝ) : ℝ

Pressure slope, given by -1 - 2 * lam.

Equations

• NavierStokes.AngularMomentReset.pressureSlope lam = -1 - 2 * lam

noncomputable def NavierStokes.AngularMomentReset.linearMatrix (lam : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

The actual derivative matrix of the two integral changes at zero coefficients.

Equations

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

theorem NavierStokes.AngularMomentReset.linearMatrix_det (lam : ℝ) : (linearMatrix lam).det = 2 * moment (angularSlope lam) * moment (pressureSlope lam) * (Real.exp (2 * pressureSlope lam) - Real.exp (2 * angularSlope lam))

theorem NavierStokes.AngularMomentReset.linearMatrix_det_ne_zero (lam : ℝ) (hlam : 0 < lam) : (linearMatrix lam).det ≠ 0

noncomputable def NavierStokes.AngularMomentReset.linearEquiv (lam : ℝ) (hlam : 0 < lam) : Coeff ≃L[ℝ] Coeff

The integral derivative is an actual continuous linear equivalence.

Equations

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

noncomputable def NavierStokes.AngularMomentReset.relative (c : Coeff) (y : ℝ) : ℝ

Relative, given by c 0 * bump 0 y + c 1 * bump 1 y.

Equations

• NavierStokes.AngularMomentReset.relative c y = c 0 * NavierStokes.AngularMomentReset.bump 0 y + c 1 * NavierStokes.AngularMomentReset.bump 1 y

theorem NavierStokes.AngularMomentReset.relative_contDiff (c : Coeff) : ContDiff ℝ (↑⊤) (relative c)

theorem NavierStokes.AngularMomentReset.relative_support (c : Coeff) : Function.support (relative c) ⊆ Set.Icc (-3 / 20) (43 / 20)

theorem NavierStokes.AngularMomentReset.relative_hasCompactSupport (c : Coeff) : HasCompactSupport (relative c)

noncomputable def NavierStokes.AngularMomentReset.quadraticMoment (lam : ℝ) (j : Fin 2) : ℝ

Quadratic moment, given by ∫ y, Real.exp (pressureSlope lam * y) * (bump j y) ^ 2.

Equations

• NavierStokes.AngularMomentReset.quadraticMoment lam j = ∫ (y : ℝ), Real.exp (NavierStokes.AngularMomentReset.pressureSlope lam * y) * NavierStokes.AngularMomentReset.bump j y ^ 2

noncomputable def NavierStokes.AngularMomentReset.quadraticBilin (lam : ℝ) : Coeff →ₗ[ℝ] Coeff →ₗ[ℝ] Coeff

Quadratic bilin, bundling toFun, map_add, map_smul, map_add and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.AngularMomentReset.quadraticCLM (lam : ℝ) : Coeff →L[ℝ] Coeff →L[ℝ] Coeff

Quadratic continuous linear map, constructed using LinearMap.toContinuousLinearMap.

Equations

• NavierStokes.AngularMomentReset.quadraticCLM lam = LinearMap.toContinuousLinearMap (↑LinearMap.toContinuousLinearMap ∘ₗ NavierStokes.AngularMomentReset.quadraticBilin lam)

theorem NavierStokes.AngularMomentReset.linearEquiv_apply (lam : ℝ) (hlam : 0 < lam) (c : Coeff) : (linearEquiv lam hlam) c = (linearMatrix lam).mulVec c

theorem NavierStokes.AngularMomentReset.quadraticCLM_apply (lam : ℝ) (c d : Coeff) : ((quadraticCLM lam) c) d = ![0, quadraticMoment lam 0 * c 0 * d 0 + quadraticMoment lam 1 * c 1 * d 1]

theorem NavierStokes.AngularMomentReset.weighted_relative_integrable (s : ℝ) (c : Coeff) : MeasureTheory.Integrable (fun (y : ℝ) => Real.exp (s * y) * relative c y) MeasureTheory.volume

theorem NavierStokes.AngularMomentReset.weighted_relative_sq_integrable (s : ℝ) (c : Coeff) : MeasureTheory.Integrable (fun (y : ℝ) => Real.exp (s * y) * relative c y ^ 2) MeasureTheory.volume

theorem NavierStokes.AngularMomentReset.relative_moment (s : ℝ) (c : Coeff) : ∫ (y : ℝ), Real.exp (s * y) * relative c y = moment s * c 0 + Real.exp (2 * s) * moment s * c 1

theorem NavierStokes.AngularMomentReset.relative_square (c : Coeff) (y : ℝ) : relative c y ^ 2 = c 0 ^ 2 * bump 0 y ^ 2 + c 1 ^ 2 * bump 1 y ^ 2

theorem NavierStokes.AngularMomentReset.relative_square_moment (lam : ℝ) (c : Coeff) : ∫ (y : ℝ), Real.exp (pressureSlope lam * y) * relative c y ^ 2 = quadraticMoment lam 0 * c 0 ^ 2 + quadraticMoment lam 1 * c 1 ^ 2

theorem NavierStokes.AngularMomentReset.pressure_change_integrable (lam : ℝ) (c : Coeff) : MeasureTheory.Integrable (fun (y : ℝ) => Real.exp (pressureSlope lam * y) * ((1 + relative c y) ^ 2 - 1)) MeasureTheory.volume

theorem NavierStokes.AngularMomentReset.pressure_change_moment (lam : ℝ) (c : Coeff) : ∫ (y : ℝ), Real.exp (pressureSlope lam * y) * ((1 + relative c y) ^ 2 - 1) = 2 * (moment (pressureSlope lam) * c 0 + Real.exp (2 * pressureSlope lam) * moment (pressureSlope lam) * c 1) + quadraticMoment lam 0 * c 0 ^ 2 + quadraticMoment lam 1 * c 1 ^ 2

theorem NavierStokes.AngularMomentReset.moment_map_identity (lam : ℝ) (hlam : 0 < lam) (c : Coeff) : (linearEquiv lam hlam) c + ((quadraticCLM lam) c) c = ![∫ (y : ℝ), Real.exp (angularSlope lam * y) * relative c y, ∫ (y : ℝ), Real.exp (pressureSlope lam * y) * ((1 + relative c y) ^ 2 - 1)]

The quadratic coefficient map equals the two actual integral changes.

def NavierStokes.AngularMomentReset.debt (δ : ℝ) : Coeff

Debt, given by ![δ, 0].

Equations

• NavierStokes.AngularMomentReset.debt δ = ![δ, 0]

theorem NavierStokes.AngularMomentReset.debt_contDiff : ContDiff ℝ (↑⊤) debt

theorem NavierStokes.AngularMomentReset.debt_norm_le (δ : ℝ) : ‖debt δ‖ ≤ |δ|

theorem NavierStokes.AngularMomentReset.exists_normalized_branch (lam : ℝ) (hlam : 0 < lam) : ∃ (c : ℝ → Coeff) (ε : ℝ) (K : ℝ), 0 < ε ∧ 0 < K ∧ ContDiffOn ℝ (↑⊤) c (Set.Ioo (-ε) ε) ∧ c 0 = 0 ∧ ∀ δ ∈ Set.Ioo (-ε) ε, ∫ (y : ℝ), Real.exp (angularSlope lam * y) * relative (c δ) y = δ ∧ ∫ (y : ℝ), Real.exp (pressureSlope lam * y) * ((1 + relative (c δ) y) ^ 2 - 1) = 0 ∧ ‖c δ‖ ≤ K * |δ|

A smooth small branch is obtained from the proved actual moment derivative, not from an assumed solution or matrix rank.

theorem NavierStokes.AngularMomentReset.relative_deriv (c : Coeff) (y : ℝ) : deriv (relative c) y = c 0 * deriv (bump 0) y + c 1 * deriv (bump 1) y

theorem NavierStokes.AngularMomentReset.relative_first_jet_bound : ∃ (D : ℝ), 0 < D ∧ ∀ (c : Coeff) (y : ℝ), |relative c y| ≤ D * ‖c‖ ∧ |deriv (relative c) y| ≤ D * ‖c‖

The fixed finite family controls both the relative perturbation and its first derivative.

theorem NavierStokes.AngularMomentReset.positive_and_slope_of_small (lam : ℝ) (hlam : 0 < lam) (c : Coeff) (y : ℝ) (h0 : |relative c y| ≤ 1 / 2) (h1 : |deriv (relative c) y| ≤ lam / 4) : 0 < 1 + relative c y ∧ -lam + deriv (relative c) y / (1 + relative c y) ≤ -lam / 2

structure NavierStokes.AngularMomentReset.ResetBranch (lam : ℝ) : Type

A constructed branch, with exact normalized integrals and quantitative first-jet control.

• coefficients : ℝ → Coeff

  Coefficients of ResetBranch, of type ℝ → Coeff.

• radius : ℝ

  Radius of ResetBranch, of type ℝ.

• bound : ℝ

  Bound of ResetBranch, of type ℝ.

• radius_pos : 0 < self.radius
• bound_pos : 0 < self.bound
• smooth : ContDiffOn ℝ (↑⊤) self.coefficients (Set.Ioo (-self.radius) self.radius)
• at_zero : self.coefficients 0 = 0
• angular (δ : ℝ) : δ ∈ Set.Ioo (-self.radius) self.radius → ∫ (y : ℝ), Real.exp (angularSlope lam * y) * relative (self.coefficients δ) y = δ
• pressure (δ : ℝ) : δ ∈ Set.Ioo (-self.radius) self.radius → ∫ (y : ℝ), Real.exp (pressureSlope lam * y) * ((1 + relative (self.coefficients δ) y) ^ 2 - 1) = 0
• coefficient_bound (δ : ℝ) : δ ∈ Set.Ioo (-self.radius) self.radius → ‖self.coefficients δ‖ ≤ self.bound * |δ|
• first_jet_bound (δ : ℝ) : δ ∈ Set.Ioo (-self.radius) self.radius → ∀ (y : ℝ), |relative (self.coefficients δ) y| ≤ self.bound * |δ| ∧ |deriv (relative (self.coefficients δ)) y| ≤ self.bound * |δ|
• small_jets (δ : ℝ) : δ ∈ Set.Ioo (-self.radius) self.radius → ∀ (y : ℝ), |relative (self.coefficients δ) y| ≤ 1 / 2 ∧ |deriv (relative (self.coefficients δ)) y| ≤ lam / 4

theorem NavierStokes.AngularMomentReset.exists_resetBranch (lam : ℝ) (hlam : 0 < lam) : Nonempty (ResetBranch lam)

No branch fields are hypotheses: all of them are constructed from the explicit bumps.

noncomputable def NavierStokes.AngularMomentReset.resetBranch (lam : ℝ) (hlam : 0 < lam) : ResetBranch lam

One fixed choice of the proved small branch.

Equations

• NavierStokes.AngularMomentReset.resetBranch lam hlam = Classical.choice ⋯

Actual modified angular fields

noncomputable def NavierStokes.AngularMomentReset.baseE (lam e0 y : ℝ) : ℝ

Base E, given by e0 * Real.exp ((-1 / 2 - lam) * y).

Equations

• NavierStokes.AngularMomentReset.baseE lam e0 y = e0 * Real.exp ((-1 / 2 - lam) * y)

noncomputable def NavierStokes.AngularMomentReset.modifiedE (lam e0 y0 : ℝ) (c : Coeff) (y : ℝ) : ℝ

The first bump is centered at y0, and the second at y0 + 2.

Equations

• NavierStokes.AngularMomentReset.modifiedE lam e0 y0 c y = NavierStokes.AngularMomentReset.baseE lam e0 y * (1 + NavierStokes.AngularMomentReset.relative c (y - y0))

noncomputable def NavierStokes.AngularMomentReset.radiusX (X0 y : ℝ) : ℝ

Radius X, given by X0 * Real.exp y.

Equations

• NavierStokes.AngularMomentReset.radiusX X0 y = X0 * Real.exp y

noncomputable def NavierStokes.AngularMomentReset.baseH (lam e0 X0 y : ℝ) : ℝ

Base H, given by Real.sqrt (2 * radiusX X0 y) * baseE lam e0 y.

Equations

• NavierStokes.AngularMomentReset.baseH lam e0 X0 y = √(2 * NavierStokes.AngularMomentReset.radiusX X0 y) * NavierStokes.AngularMomentReset.baseE lam e0 y

noncomputable def NavierStokes.AngularMomentReset.modifiedH (lam e0 X0 y0 : ℝ) (c : Coeff) (y : ℝ) : ℝ

Modified H, given by Real.sqrt (2 * radiusX X0 y) * modifiedE lam e0 y0 c y.

Equations

• NavierStokes.AngularMomentReset.modifiedH lam e0 X0 y0 c y = √(2 * NavierStokes.AngularMomentReset.radiusX X0 y) * NavierStokes.AngularMomentReset.modifiedE lam e0 y0 c y

noncomputable def NavierStokes.AngularMomentReset.angularScale (lam e0 X0 y0 : ℝ) : ℝ

Angular scale, given by X0 * Real.sqrt (2 * X0) * e0 * Real.exp (angularSlope lam * y0).

Equations

• NavierStokes.AngularMomentReset.angularScale lam e0 X0 y0 = X0 * √(2 * X0) * e0 * Real.exp (NavierStokes.AngularMomentReset.angularSlope lam * y0)

noncomputable def NavierStokes.AngularMomentReset.logSlope (E : ℝ → ℝ) (y : ℝ) : ℝ

Log slope, given by 1 / 2 + deriv E y / E y.

Equations

• NavierStokes.AngularMomentReset.logSlope E y = 1 / 2 + deriv E y / E y

theorem NavierStokes.AngularMomentReset.baseE_contDiff (lam e0 : ℝ) : ContDiff ℝ (↑⊤) (baseE lam e0)

theorem NavierStokes.AngularMomentReset.modifiedE_contDiff (lam e0 y0 : ℝ) (c : Coeff) : ContDiff ℝ (↑⊤) (modifiedE lam e0 y0 c)

theorem NavierStokes.AngularMomentReset.baseE_pos (lam e0 y : ℝ) (he0 : 0 < e0) : 0 < baseE lam e0 y

theorem NavierStokes.AngularMomentReset.modifiedE_sub_support (lam e0 y0 : ℝ) (c : Coeff) : Function.support (modifiedE lam e0 y0 c - baseE lam e0) ⊆ Set.Icc (y0 - 3 / 20) (y0 + 43 / 20)

theorem NavierStokes.AngularMomentReset.modifiedE_sub_hasCompactSupport (lam e0 y0 : ℝ) (c : Coeff) : HasCompactSupport (modifiedE lam e0 y0 c - baseE lam e0)

theorem NavierStokes.AngularMomentReset.modifiedE_sub_tsupport (lam e0 y0 : ℝ) (c : Coeff) : tsupport (modifiedE lam e0 y0 c - baseE lam e0) ⊆ Set.Ioo (y0 - 1) (y0 + 3)

Choosing y0 = T - 3 places the whole edit strictly inside (T - 4, T).

theorem NavierStokes.AngularMomentReset.modifiedE_unchanged (lam e0 y0 : ℝ) (c : Coeff) {y : ℝ} (hy : y ∉ Set.Ioo (y0 - 1) (y0 + 3)) : modifiedE lam e0 y0 c y = baseE lam e0 y

theorem NavierStokes.AngularMomentReset.baseE_hasDerivAt (lam e0 y : ℝ) : HasDerivAt (baseE lam e0) (baseE lam e0 y * (-1 / 2 - lam)) y

theorem NavierStokes.AngularMomentReset.modifiedE_hasDerivAt (lam e0 y0 : ℝ) (c : Coeff) (y : ℝ) : HasDerivAt (modifiedE lam e0 y0 c) (baseE lam e0 y * (-1 / 2 - lam) * (1 + relative c (y - y0)) + baseE lam e0 y * deriv (relative c) (y - y0)) y

theorem NavierStokes.AngularMomentReset.modifiedE_logSlope (lam e0 y0 : ℝ) (c : Coeff) (y : ℝ) (he0 : e0 ≠ 0) (hpos : 1 + relative c (y - y0) ≠ 0) : logSlope (modifiedE lam e0 y0 c) y = -lam + deriv (relative c) (y - y0) / (1 + relative c (y - y0))

theorem NavierStokes.AngularMomentReset.weighted_translate_integral (s y0 : ℝ) (f : ℝ → ℝ) : ∫ (y : ℝ), Real.exp (s * y) * f (y - y0) = Real.exp (s * y0) * ∫ (y : ℝ), Real.exp (s * y) * f y

theorem NavierStokes.AngularMomentReset.baseE_square (lam e0 y : ℝ) : baseE lam e0 y ^ 2 = e0 ^ 2 * Real.exp (pressureSlope lam * y)

theorem NavierStokes.AngularMomentReset.pressure_integral_formula (lam e0 y0 : ℝ) (c : Coeff) : ∫ (y : ℝ), modifiedE lam e0 y0 c y ^ 2 - baseE lam e0 y ^ 2 = e0 ^ 2 * Real.exp (pressureSlope lam * y0) * ∫ (y : ℝ), Real.exp (pressureSlope lam * y) * ((1 + relative c y) ^ 2 - 1)

theorem NavierStokes.AngularMomentReset.sqrt_exp_half (y : ℝ) : √(Real.exp y) = Real.exp (y / 2)

theorem NavierStokes.AngularMomentReset.angular_weight_formula (lam e0 X0 y : ℝ) (hX : 0 ≤ X0) : radiusX X0 y * baseH lam e0 X0 y = X0 * √(2 * X0) * e0 * Real.exp (angularSlope lam * y)

theorem NavierStokes.AngularMomentReset.angular_integral_formula (lam e0 X0 y0 : ℝ) (c : Coeff) (hX : 0 ≤ X0) : ∫ (y : ℝ), radiusX X0 y * (modifiedH lam e0 X0 y0 c y - baseH lam e0 X0 y) = angularScale lam e0 X0 y0 * ∫ (y : ℝ), Real.exp (angularSlope lam * y) * relative c y

theorem NavierStokes.AngularMomentReset.angularScale_pos (lam e0 X0 y0 : ℝ) (he0 : 0 < e0) (hX : 0 < X0) : 0 < angularScale lam e0 X0 y0

theorem NavierStokes.AngularMomentReset.pressure_delta_integrable (lam e0 y0 : ℝ) (c : Coeff) : MeasureTheory.Integrable (fun (y : ℝ) => modifiedE lam e0 y0 c y ^ 2 - baseE lam e0 y ^ 2) MeasureTheory.volume

The pressure change is an integrable compactly supported difference. We do not subtract divergent integrals of the pure exponential background over ℝ.

theorem NavierStokes.AngularMomentReset.angular_delta_integrable (lam e0 X0 y0 : ℝ) (c : Coeff) : MeasureTheory.Integrable (fun (y : ℝ) => radiusX X0 y * (modifiedH lam e0 X0 y0 c y - baseH lam e0 X0 y)) MeasureTheory.volume

theorem NavierStokes.AngularMomentReset.modifiedH_unchanged (lam e0 X0 y0 : ℝ) (c : Coeff) {y : ℝ} (hy : y ∉ Set.Ioo (y0 - 1) (y0 + 3)) : modifiedH lam e0 X0 y0 c y = baseH lam e0 X0 y

theorem NavierStokes.AngularMomentReset.ResetBranch.pressure_neutral {lam : ℝ} (B : ResetBranch lam) (e0 y0 δ : ℝ) (hδ : δ ∈ Set.Ioo (-B.radius) B.radius) : ∫ (y : ℝ), modifiedE lam e0 y0 (B.coefficients δ) y ^ 2 - baseE lam e0 y ^ 2 = 0

theorem NavierStokes.AngularMomentReset.ResetBranch.angular_change {lam : ℝ} (B : ResetBranch lam) (e0 X0 y0 δ : ℝ) (hX : 0 ≤ X0) (hδ : δ ∈ Set.Ioo (-B.radius) B.radius) : ∫ (y : ℝ), radiusX X0 y * (modifiedH lam e0 X0 y0 (B.coefficients δ) y - baseH lam e0 X0 y) = angularScale lam e0 X0 y0 * δ

theorem NavierStokes.AngularMomentReset.ResetBranch.positive {lam : ℝ} (B : ResetBranch lam) (hlam : 0 < lam) (e0 y0 δ y : ℝ) (he0 : 0 < e0) (hδ : δ ∈ Set.Ioo (-B.radius) B.radius) : 0 < modifiedE lam e0 y0 (B.coefficients δ) y

theorem NavierStokes.AngularMomentReset.ResetBranch.logSlope_le {lam : ℝ} (B : ResetBranch lam) (hlam : 0 < lam) (e0 y0 δ y : ℝ) (he0 : 0 < e0) (hδ : δ ∈ Set.Ioo (-B.radius) B.radius) : logSlope (modifiedE lam e0 y0 (B.coefficients δ)) y ≤ -lam / 2

theorem NavierStokes.AngularMomentReset.ResetBranch.exact_target {lam : ℝ} (B : ResetBranch lam) (e0 X0 y0 Iold Itarget : ℝ) (he0 : 0 < e0) (hX : 0 < X0) (hδ : (Itarget - Iold) / angularScale lam e0 X0 y0 ∈ Set.Ioo (-B.radius) B.radius) : Iold + ∫ (y : ℝ), radiusX X0 y * (modifiedH lam e0 X0 y0 (B.coefficients ((Itarget - Iold) / angularScale lam e0 X0 y0)) y - baseH lam e0 X0 y) = Itarget

Any desired angular endpoint moment is reached when its normalized debt lies in the constructed common small interval.

Finite-interval moments, including an arbitrary earlier prefix

theorem NavierStokes.AngularMomentReset.radiusX_continuous (X0 : ℝ) : Continuous (radiusX X0)

theorem NavierStokes.AngularMomentReset.baseH_continuous (lam e0 X0 : ℝ) : Continuous (baseH lam e0 X0)

theorem NavierStokes.AngularMomentReset.modifiedH_continuous (lam e0 X0 y0 : ℝ) (c : Coeff) : Continuous (modifiedH lam e0 X0 y0 c)

theorem NavierStokes.AngularMomentReset.outside_window {a b y0 y : ℝ} (ha : a ≤ y0 - 1) (hb : y0 + 3 ≤ b) (hy : y ∉ Set.Icc a b) : y ∉ Set.Ioo (y0 - 1) (y0 + 3)

theorem NavierStokes.AngularMomentReset.angular_interval_change (lam e0 X0 y0 a b : ℝ) (c : Coeff) (hX : 0 ≤ X0) (ha : a ≤ y0 - 1) (hb : y0 + 3 ≤ b) : (∫ (y : ℝ) in Set.Icc a b, radiusX X0 y * modifiedH lam e0 X0 y0 c y) - ∫ (y : ℝ) in Set.Icc a b, radiusX X0 y * baseH lam e0 X0 y = angularScale lam e0 X0 y0 * ∫ (y : ℝ), Real.exp (angularSlope lam * y) * relative c y

theorem NavierStokes.AngularMomentReset.pressure_interval_change (lam e0 y0 a b : ℝ) (c : Coeff) (ha : a ≤ y0 - 1) (hb : y0 + 3 ≤ b) : (∫ (y : ℝ) in Set.Icc a b, modifiedE lam e0 y0 c y ^ 2) - ∫ (y : ℝ) in Set.Icc a b, baseE lam e0 y ^ 2 = e0 ^ 2 * Real.exp (pressureSlope lam * y0) * ∫ (y : ℝ), Real.exp (pressureSlope lam * y) * ((1 + relative c y) ^ 2 - 1)

theorem NavierStokes.AngularMomentReset.ResetBranch.pressure_interval_neutral {lam : ℝ} (B : ResetBranch lam) (e0 y0 a b δ : ℝ) (ha : a ≤ y0 - 1) (hb : y0 + 3 ≤ b) (hδ : δ ∈ Set.Ioo (-B.radius) B.radius) : ∫ (y : ℝ) in Set.Icc a b, modifiedE lam e0 y0 (B.coefficients δ) y ^ 2 = ∫ (y : ℝ) in Set.Icc a b, baseE lam e0 y ^ 2

noncomputable def NavierStokes.AngularMomentReset.prefixI (lam e0 X0 a b Iprior : ℝ) : ℝ

Prefix I, given by Iprior + ∫ y in Icc a b, radiusX X0 y * baseH lam e0 X0 y.

Equations

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

theorem NavierStokes.AngularMomentReset.ResetBranch.exact_endpoint_moment {lam : ℝ} (B : ResetBranch lam) (e0 X0 y0 a b Iprior Itarget : ℝ) (he0 : 0 < e0) (hX : 0 < X0) (ha : a ≤ y0 - 1) (hb : y0 + 3 ≤ b) (hδ : (Itarget - prefixI lam e0 X0 a b Iprior) / angularScale lam e0 X0 y0 ∈ Set.Ioo (-B.radius) B.radius) : Iprior + ∫ (y : ℝ) in Set.Icc a b, radiusX X0 y * modifiedH lam e0 X0 y0 (B.coefficients ((Itarget - prefixI lam e0 X0 a b Iprior) / angularScale lam e0 X0 y0)) y = Itarget

Smooth dependence on the angular parameter

theorem NavierStokes.AngularMomentReset.relative_joint_contDiff : ContDiff ℝ ↑⊤ fun (z : Coeff × ℝ) => relative z.1 z.2

theorem NavierStokes.AngularMomentReset.ResetBranch.joint_contDiffOn {lam : ℝ} (B : ResetBranch lam) (e0 y0 : ℝ) {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {S : Set P} {δ : P → ℝ} (hδ : ContDiffOn ℝ (↑⊤) δ S) (hsmall : ∀ p ∈ S, δ p ∈ Set.Ioo (-B.radius) B.radius) : ContDiffOn ℝ (↑⊤) (fun (z : P × ℝ) => modifiedE lam e0 y0 (B.coefficients (δ z.1)) z.2) (S ×ˢ Set.univ)

def NavierStokes.UniformAngularReset.lambdaRange : Set ℝ

Lambda range, given by Icc 0 (1 / 10).

Equations

• NavierStokes.UniformAngularReset.lambdaRange = Set.Icc 0 (1 / 10)

theorem NavierStokes.UniformAngularReset.linearMatrix_det_ne_zero_nonneg (lam : ℝ) (hlam : 0 ≤ lam) : (AngularMomentReset.linearMatrix lam).det ≠ 0

theorem NavierStokes.UniformAngularReset.continuous_moment : Continuous AngularMomentReset.moment

theorem NavierStokes.UniformAngularReset.continuous_quadraticMoment (j : Fin 2) : Continuous fun (lam : ℝ) => AngularMomentReset.quadraticMoment lam j

noncomputable def NavierStokes.UniformAngularReset.linearCLM (lam : ℝ) : AngularMomentReset.Coeff →L[ℝ] AngularMomentReset.Coeff

Linear continuous linear map, constructed using LinearMap.toContinuousLinearMap.

Equations

• NavierStokes.UniformAngularReset.linearCLM lam = LinearMap.toContinuousLinearMap { toFun := (NavierStokes.AngularMomentReset.linearMatrix lam).mulVec, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def NavierStokes.UniformAngularReset.linearEquivNonneg (lam : ℝ) (hlam : 0 ≤ lam) : AngularMomentReset.Coeff ≃L[ℝ] AngularMomentReset.Coeff

Linear equiv nonneg, constructed using LinearEquiv.toContinuousLinearEquiv.

Equations

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

theorem NavierStokes.UniformAngularReset.linearEquivNonneg_coe (lam : ℝ) (hlam : 0 ≤ lam) : ↑(linearEquivNonneg lam hlam) = linearCLM lam

theorem NavierStokes.UniformAngularReset.continuous_linearCLM : Continuous linearCLM

def NavierStokes.UniformAngularReset.quadraticCoefficientsBilin (q : AngularMomentReset.Coeff) : AngularMomentReset.Coeff →ₗ[ℝ] AngularMomentReset.Coeff →ₗ[ℝ] AngularMomentReset.Coeff

Quadratic coefficients bilin, bundling toFun, map_add, map_smul, map_add and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.UniformAngularReset.quadraticCoefficientMap : AngularMomentReset.Coeff →ₗ[ℝ] AngularMomentReset.Coeff →L[ℝ] AngularMomentReset.Coeff →L[ℝ] AngularMomentReset.Coeff

Quadratic coefficient map, bundling toFun, map_add, map_smul.

Equations

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

theorem NavierStokes.UniformAngularReset.continuous_quadraticCLM : Continuous AngularMomentReset.quadraticCLM

theorem NavierStokes.UniformAngularReset.uniform_operator_bounds : ∃ (β : ℝ) (K : ℝ), 0 < β ∧ 0 < K ∧ ∀ lam ∈ lambdaRange, ‖(linearCLM lam).inverse‖ ≤ β ∧ ‖AngularMomentReset.quadraticCLM lam‖ ≤ K

Both operator bounds follow from the compact parameter interval and the proved determinant, including its nonzero value at zero.

theorem NavierStokes.UniformAngularReset.uniform_small_solutions : ∃ (β : ℝ) (ε : ℝ), 0 < β ∧ 0 < ε ∧ ∀ lam ∈ lambdaRange, ∀ (d : AngularMomentReset.Coeff), ‖d‖ ≤ ε → ∃! c : AngularMomentReset.Coeff, ‖c‖ ≤ 2 * β * ‖d‖ ∧ (linearCLM lam) c + ((AngularMomentReset.quadraticCLM lam) c) c = d

noncomputable def NavierStokes.UniformAngularReset.quadraticMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) (c : E) : E

Quadratic map, given by B c + A c c.

Equations

• NavierStokes.UniformAngularReset.quadraticMap B A c = B c + (A c) c

noncomputable def NavierStokes.UniformAngularReset.tangent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) (c : E) : E →L[ℝ] E

Tangent, given by B.toContinuousLinearMap + A c + A.flip c.

Equations

• NavierStokes.UniformAngularReset.tangent B A c = ↑B + A c + A.flip c

theorem NavierStokes.UniformAngularReset.quadraticMap_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) : ContDiff ℝ (↑⊤) (quadraticMap B A)

theorem NavierStokes.UniformAngularReset.quadraticMap_hasFDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) (c : E) : HasFDerivAt (quadraticMap B A) (tangent B A c) c

theorem NavierStokes.UniformAngularReset.tangent_lower_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) (β K r : ℝ) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hinv : ∀ (x : E), ‖B.symm x‖ ≤ β * ‖x‖) (hA : ‖A‖ ≤ K) (hsmall : 4 * β * K * r ≤ 1) (c : E) (hc : ‖c‖ ≤ r) (x : E) : ‖x‖ ≤ 2 * β * ‖(tangent B A c) x‖

theorem NavierStokes.UniformAngularReset.tangent_invertible {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) (β K r : ℝ) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hinv : ∀ (x : E), ‖B.symm x‖ ≤ β * ‖x‖) (hA : ‖A‖ ≤ K) (hsmall : 4 * β * K * r ≤ 1) (c : E) (hc : ‖c‖ ≤ r) : (tangent B A c).IsInvertible

theorem NavierStokes.UniformAngularReset.quadratic_solution_distance {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) (β K r : ℝ) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hinv : ∀ (x : E), ‖B.symm x‖ ≤ β * ‖x‖) (hA : ‖A‖ ≤ K) (hsmall : 4 * β * K * r ≤ 1) (c e d f : E) (hc : ‖c‖ ≤ r) (he : ‖e‖ ≤ r) (hceq : quadraticMap B A c = d) (heeq : quadraticMap B A e = f) : ‖c - e‖ ≤ 2 * β * ‖d - f‖

theorem NavierStokes.UniformAngularReset.exists_smooth_solver_on_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [CompleteSpace E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) (β K r : ℝ) (hβ : 0 < β) (hK : 0 ≤ K) (hr : 0 < r) (hinv : ∀ (x : E), ‖B.symm x‖ ≤ β * ‖x‖) (hA : ‖A‖ ≤ K) (hsmall : 4 * β * K * r ≤ 1) : ∃ (g : E → E), ContDiffOn ℝ (↑⊤) g (Metric.ball 0 (r / (4 * β))) ∧ (∀ d ∈ Metric.ball 0 (r / (4 * β)), quadraticMap B A (g d) = d ∧ ‖g d‖ ≤ 2 * β * ‖d‖) ∧ ∀ d ∈ Metric.ball 0 (r / (4 * β)), ∀ e ∈ Metric.ball 0 (r / (4 * β)), ‖g d - g e‖ ≤ 2 * β * ‖d - e‖

Contraction uniqueness patches the local smooth inverses throughout one uniform debt ball. The resulting smoothness radius is quantitative.

theorem NavierStokes.UniformAngularReset.actual_moment_map (lam : ℝ) (c : AngularMomentReset.Coeff) : (linearCLM lam) c + ((AngularMomentReset.quadraticCLM lam) c) c = ![∫ (y : ℝ), Real.exp (AngularMomentReset.angularSlope lam * y) * AngularMomentReset.relative c y, ∫ (y : ℝ), Real.exp (AngularMomentReset.pressureSlope lam * y) * ((1 + AngularMomentReset.relative c y) ^ 2 - 1)]

theorem NavierStokes.UniformAngularReset.uniform_reset_branch : ∃ (ε : ℝ) (L : ℝ), 0 < ε ∧ 0 < L ∧ ∀ lam ∈ lambdaRange, ∃ (c : ℝ → AngularMomentReset.Coeff), ContDiffOn ℝ (↑⊤) c (Set.Ioo (-ε) ε) ∧ c 0 = 0 ∧ ∀ δ ∈ Set.Ioo (-ε) ε, ∫ (y : ℝ), Real.exp (AngularMomentReset.angularSlope lam * y) * AngularMomentReset.relative (c δ) y = δ ∧ ∫ (y : ℝ), Real.exp (AngularMomentReset.pressureSlope lam * y) * ((1 + AngularMomentReset.relative (c δ) y) ^ 2 - 1) = 0 ∧ ‖c δ‖ ≤ L * |δ| ∧ ‖deriv c δ‖ ≤ L ∧ ∀ (y : ℝ), |AngularMomentReset.relative (c δ) y| ≤ L * |δ| ∧ |deriv (AngularMomentReset.relative (c δ)) y| ≤ L * |δ|

A single radius and a single bound work for the actual two-bump system for every lam ∈ [0,1/10]. Smoothness and the derivative bound concern the debt variable; no smoothness of an arbitrary choice in lam is asserted.

noncomputable def NavierStokes.UniformAngularReset.baseWeight (d : OutgoingTail.TailData) (y : ℝ) : ℝ

The factor sqrt 2 cancels in every angular-history ratio.

Equations

• NavierStokes.UniformAngularReset.baseWeight d y = Real.exp (3 * y / 2) * NavierStokes.OutgoingSchedule.radialAmplitude d.core.P d.core.dropLength d.core.lam y

noncomputable def NavierStokes.UniformAngularReset.baseHistory (d : OutgoingTail.TailData) (y : ℝ) : ℝ

Base history, given by (5 / 8) * d.core.P + OutgoingSchedule.primitive (baseWeight d) y.

Equations

• NavierStokes.UniformAngularReset.baseHistory d y = 5 / 8 * d.core.P + NavierStokes.OutgoingSchedule.primitive (NavierStokes.UniformAngularReset.baseWeight d) y

theorem NavierStokes.UniformAngularReset.baseWeight_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (baseWeight d)

theorem NavierStokes.UniformAngularReset.baseWeight_pos (d : OutgoingTail.TailData) (y : ℝ) : 0 < baseWeight d y

theorem NavierStokes.UniformAngularReset.baseWeight_zero (d : OutgoingTail.TailData) : baseWeight d 0 = d.core.P

theorem NavierStokes.UniformAngularReset.core_slope_lower (d : OutgoingTail.TailData) (y : ℝ) : -d.core.lam ≤ OutgoingSchedule.slope d.core.dropLength d.core.lam y

theorem NavierStokes.UniformAngularReset.baseWeight_hasDerivAt (d : OutgoingTail.TailData) (y : ℝ) : HasDerivAt (baseWeight d) (baseWeight d y * (1 + OutgoingSchedule.slope d.core.dropLength d.core.lam y)) y

theorem NavierStokes.UniformAngularReset.baseHistory_hasDerivAt (d : OutgoingTail.TailData) (y : ℝ) : HasDerivAt (baseHistory d) (baseWeight d y) y

theorem NavierStokes.UniformAngularReset.baseHistory_nonneg (d : OutgoingTail.TailData) {y : ℝ} (hy : 0 ≤ y) : 0 ≤ baseHistory d y

theorem NavierStokes.UniformAngularReset.baseHistory_le (d : OutgoingTail.TailData) {y : ℝ} (hy : 0 ≤ y) : baseHistory d y ≤ baseWeight d y / (1 - d.core.lam)

The actual unflattened angular-history ratio is uniformly bounded; the ideal incoming prefix is included explicitly.

noncomputable def NavierStokes.UniformAngularReset.flattenShape (d : OutgoingTail.TailData) (y eta : ℝ) : ℝ

Flatten shape, constructed using Real.exp.

Equations

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

theorem NavierStokes.UniformAngularReset.shape_eq_exp (eta : ℝ) : OutgoingSchedule.shape eta = Real.exp (-OutgoingTail.logShape eta)

theorem NavierStokes.UniformAngularReset.flattened_eq (d : OutgoingTail.TailData) (y eta : ℝ) : OutgoingTail.flattened d (y, eta) = OutgoingSchedule.radialAmplitude d.core.P d.core.dropLength d.core.lam y * flattenShape d y eta

theorem NavierStokes.UniformAngularReset.flattenShape_pos (d : OutgoingTail.TailData) (y eta : ℝ) : 0 < flattenShape d y eta

theorem NavierStokes.UniformAngularReset.flattenShape_le_one (d : OutgoingTail.TailData) (y eta : ℝ) : flattenShape d y eta ≤ 1

noncomputable def NavierStokes.UniformAngularReset.flatWeight (d : OutgoingTail.TailData) (eta y : ℝ) : ℝ

Flat weight, given by Real.exp (3 * y / 2) * flattened d (y, eta).

Equations

• NavierStokes.UniformAngularReset.flatWeight d eta y = Real.exp (3 * y / 2) * NavierStokes.OutgoingTail.flattened d (y, eta)

noncomputable def NavierStokes.UniformAngularReset.flatHistory (d : OutgoingTail.TailData) (eta y : ℝ) : ℝ

Flat history, given by (5 / 8) * d.core.P * shape eta + OutgoingSchedule.primitive (flatWeight d eta) y.

Equations

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

theorem NavierStokes.UniformAngularReset.flatWeight_contDiff (d : OutgoingTail.TailData) (eta : ℝ) : ContDiff ℝ (↑⊤) (flatWeight d eta)

theorem NavierStokes.UniformAngularReset.flatWeight_pos (d : OutgoingTail.TailData) (eta y : ℝ) : 0 < flatWeight d eta y

theorem NavierStokes.UniformAngularReset.flatWeight_le_base (d : OutgoingTail.TailData) (eta y : ℝ) : flatWeight d eta y ≤ baseWeight d y

theorem NavierStokes.UniformAngularReset.flatHistory_bounds (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : 0 ≤ flatHistory d eta y ∧ flatHistory d eta y ≤ baseHistory d y

theorem NavierStokes.UniformAngularReset.compact_integral_contDiff (F : ℝ → ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hF : ContDiff ℝ (↑⊤) (Function.uncurry F)) : ContDiff ℝ ↑⊤ fun (p : ℝ) => ∫ (t : ℝ) in a..b, F p t

theorem NavierStokes.UniformAngularReset.flatWeight_joint_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (Function.uncurry (flatWeight d))

theorem NavierStokes.UniformAngularReset.flatHistory_contDiff (d : OutgoingTail.TailData) {y : ℝ} (hy : 0 ≤ y) : ContDiff ℝ ↑⊤ fun (eta : ℝ) => flatHistory d eta y

noncomputable def NavierStokes.UniformAngularReset.etaRate (d : OutgoingTail.TailData) (eta y : ℝ) : ℝ

Eta rate, given by (sigma ((y - d.core.endpoint) / flattenLength) - 1) * (2 * eta / (1 + eta ^ 2)).

Equations

• NavierStokes.UniformAngularReset.etaRate d eta y = (NavierStokes.OutgoingSchedule.sigma ((y - d.core.endpoint) / NavierStokes.OutgoingTail.flattenLength) - 1) * (2 * eta / (1 + eta ^ 2))

theorem NavierStokes.UniformAngularReset.logShape_hasDerivAt (eta : ℝ) : HasDerivAt OutgoingTail.logShape (2 * eta / (1 + eta ^ 2)) eta

theorem NavierStokes.UniformAngularReset.logShape_deriv_bound (eta : ℝ) : |2 * eta / (1 + eta ^ 2)| ≤ 1

theorem NavierStokes.UniformAngularReset.etaRate_bound (d : OutgoingTail.TailData) (eta y : ℝ) : |etaRate d eta y| ≤ 1

theorem NavierStokes.UniformAngularReset.flatWeight_eq (d : OutgoingTail.TailData) (eta y : ℝ) : flatWeight d eta y = baseWeight d y * flattenShape d y eta

theorem NavierStokes.UniformAngularReset.flatWeight_eta_hasDerivAt (d : OutgoingTail.TailData) (eta y : ℝ) : HasDerivAt (fun (eta : ℝ) => flatWeight d eta y) (flatWeight d eta y * etaRate d eta y) eta

theorem NavierStokes.UniformAngularReset.flatWeight_eta_bound (d : OutgoingTail.TailData) (eta y : ℝ) : |flatWeight d eta y * etaRate d eta y| ≤ baseWeight d y

theorem NavierStokes.UniformAngularReset.etaRate_continuous (d : OutgoingTail.TailData) (eta : ℝ) : Continuous (etaRate d eta)

theorem NavierStokes.UniformAngularReset.shape_hasDerivAt (eta : ℝ) : HasDerivAt OutgoingSchedule.shape (OutgoingSchedule.shape eta * -(2 * eta / (1 + eta ^ 2))) eta

theorem NavierStokes.UniformAngularReset.shape_le_one (eta : ℝ) : OutgoingSchedule.shape eta ≤ 1

theorem NavierStokes.UniformAngularReset.flatHistory_hasDerivAt (d : OutgoingTail.TailData) (eta y : ℝ) : HasDerivAt (fun (eta : ℝ) => flatHistory d eta y) (5 / 8 * d.core.P * (OutgoingSchedule.shape eta * -(2 * eta / (1 + eta ^ 2))) + ∫ (t : ℝ) in 0..y, flatWeight d eta t * etaRate d eta t) eta

theorem NavierStokes.UniformAngularReset.flatHistory_deriv_bound (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : |deriv (fun (eta : ℝ) => flatHistory d eta y) eta| ≤ baseHistory d y

theorem NavierStokes.UniformAngularReset.flattenEnd_pos (d : OutgoingTail.TailData) : 0 < d.flattenEnd

theorem NavierStokes.UniformAngularReset.flatWeight_uniform (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.flattenEnd ≤ y) : flatWeight d eta y = baseWeight d y / 2

theorem NavierStokes.UniformAngularReset.baseWeight_hold (d : OutgoingTail.TailData) {a y : ℝ} (ha : d.core.holdStart ≤ a) (hay : a ≤ y) : baseWeight d y = baseWeight d a * Real.exp ((1 - d.core.lam) * (y - a))

theorem NavierStokes.UniformAngularReset.flatHistory_increment (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.flattenEnd ≤ y) : flatHistory d eta y = flatHistory d eta d.flattenEnd + (baseWeight d y - baseWeight d d.flattenEnd) / (2 * (1 - d.core.lam))

noncomputable def NavierStokes.UniformAngularReset.flatRatio (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Flat ratio, given by flatHistory d eta d.flattenEnd / (baseWeight d d.flattenEnd / 2).

Equations

• NavierStokes.UniformAngularReset.flatRatio d eta = NavierStokes.UniformAngularReset.flatHistory d eta d.flattenEnd / (NavierStokes.UniformAngularReset.baseWeight d d.flattenEnd / 2)

theorem NavierStokes.UniformAngularReset.flatRatio_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (flatRatio d)

theorem NavierStokes.UniformAngularReset.flatRatio_bounds (d : OutgoingTail.TailData) (eta : ℝ) : 0 ≤ flatRatio d eta ∧ flatRatio d eta ≤ 2 / (1 - d.core.lam)

theorem NavierStokes.UniformAngularReset.flatRatio_deriv_bound (d : OutgoingTail.TailData) (eta : ℝ) : |deriv (flatRatio d) eta| ≤ 2 / (1 - d.core.lam)

noncomputable def NavierStokes.UniformAngularReset.decayFactor (d : OutgoingTail.TailData) : ℝ

Decay factor, given by Real.exp (-(1 - d.core.lam) * (d.uniformWait - 3)).

Equations

• NavierStokes.UniformAngularReset.decayFactor d = Real.exp (-(1 - d.core.lam) * (d.uniformWait - 3))

noncomputable def NavierStokes.UniformAngularReset.normalizedDebt (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

The actual normalized discrepancy at the first correction center.

Equations

• NavierStokes.UniformAngularReset.normalizedDebt d eta = NavierStokes.UniformAngularReset.decayFactor d * (1 / (1 - d.core.lam) - NavierStokes.UniformAngularReset.flatRatio d eta)

theorem NavierStokes.UniformAngularReset.normalizedDebt_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (normalizedDebt d)

theorem NavierStokes.UniformAngularReset.normalizedDebt_bounds (d : OutgoingTail.TailData) (eta : ℝ) : |normalizedDebt d eta| ≤ 3 * decayFactor d ∧ |deriv (normalizedDebt d) eta| ≤ 3 * decayFactor d

theorem NavierStokes.UniformAngularReset.decayFactor_le (d : OutgoingTail.TailData) (hlam : d.core.lam ≤ 1 / 15) : decayFactor d ≤ Real.exp 3 * d.core.lam ^ 28

theorem NavierStokes.UniformAngularReset.actual_debt_first_jet_bound (d : OutgoingTail.TailData) (hlam : d.core.lam ≤ 1 / 15) (eta : ℝ) : |normalizedDebt d eta| ≤ 3 * Real.exp 3 * d.core.lam ^ 28 ∧ |deriv (normalizedDebt d) eta| ≤ 3 * Real.exp 3 * d.core.lam ^ 28

The normalized debt and its first angular derivative obey the requested power bound for the actual waiting duration. The constant is universal.

theorem NavierStokes.UniformAngularReset.finalAngular_before_release (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : y ≤ d.releaseStart) : OutgoingTail.finalAngular d (y, eta) = OutgoingTail.flattened d (y, eta)

noncomputable def NavierStokes.UniformAngularReset.fullHistory (d : OutgoingTail.TailData) (eta y : ℝ) : ℝ

The angular history of the actual unedited full outgoing profile, divided by its common harmless factor sqrt 2.

Equations

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

theorem NavierStokes.UniformAngularReset.fullHistory_eq_flat (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy0 : 0 ≤ y) (hyR : y ≤ d.releaseStart) : fullHistory d eta y = flatHistory d eta y

theorem NavierStokes.UniformAngularReset.first_center_after_flatten (d : OutgoingTail.TailData) : d.flattenEnd ≤ d.releaseStart - 3

theorem NavierStokes.UniformAngularReset.normalizedDebt_eq_actual (d : OutgoingTail.TailData) (eta : ℝ) : normalizedDebt d eta = (baseWeight d d.releaseStart / (2 * (1 - d.core.lam)) - fullHistory d eta d.releaseStart) / (baseWeight d (d.releaseStart - 3) / 2)

Identification with the literal endpoint discrepancy and first-center normalization of the actual full profile.

theorem NavierStokes.UniformAngularReset.power28_le_self (d : OutgoingTail.TailData) : d.core.lam ^ 28 ≤ d.core.lam

theorem NavierStokes.UniformAngularReset.power28_le_square (d : OutgoingTail.TailData) : d.core.lam ^ 28 ≤ d.core.lam ^ 2

theorem NavierStokes.UniformAngularReset.actual_debt_tends_to_zero (ε : ℝ) (hε : 0 < ε) : ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (d : OutgoingTail.TailData), d.core.lam < lam0 → ∀ (eta : ℝ), |normalizedDebt d eta| < ε ∧ |deriv (normalizedDebt d) eta| < ε

Uniform convergence of both actual first jets, with no hypotheses on the earlier scalar choices or on the angular parameter.

structure NavierStokes.UniformAngularReset.ResetWitness (d : OutgoingTail.TailData) (K : ℝ) : Type

A reset for the actual scheduled debt, including the uniform first angular jet estimate needed for later profile estimates.

• coefficients : ℝ → AngularMomentReset.Coeff

  Coefficients of ResetWitness, of type ℝ → Coeff.

• smooth : ContDiff ℝ (↑⊤) self.coefficients
• angular (eta : ℝ) : ∫ (u : ℝ), Real.exp (AngularMomentReset.angularSlope d.core.lam * u) * AngularMomentReset.relative (self.coefficients eta) u = normalizedDebt d eta
• pressure (eta : ℝ) : ∫ (u : ℝ), Real.exp (AngularMomentReset.pressureSlope d.core.lam * u) * ((1 + AngularMomentReset.relative (self.coefficients eta) u) ^ 2 - 1) = 0
• coefficient_bound (eta : ℝ) : ‖self.coefficients eta‖ ≤ K * d.core.lam ^ 28
• eta_derivative_bound (eta : ℝ) : ‖deriv self.coefficients eta‖ ≤ K * d.core.lam ^ 28
• small_jets (eta u : ℝ) : |AngularMomentReset.relative (self.coefficients eta) u| ≤ 1 / 2 ∧ |deriv (AngularMomentReset.relative (self.coefficients eta)) u| ≤ d.core.lam / 4

theorem NavierStokes.UniformAngularReset.exists_scheduled_reset : ∃ (lam0 : ℝ) (K : ℝ), 0 < lam0 ∧ 0 < K ∧ ∀ (d : OutgoingTail.TailData), d.core.lam < lam0 → Nonempty (ResetWitness d K)

The complete outgoing data themselves supply a sufficiently small debt. No small-debt assumption or parameter-derivative assumption remains.

noncomputable def NavierStokes.UniformAngularReset.correctionCenter (d : OutgoingTail.TailData) : ℝ

Correction center, given by d.releaseStart - 3.

Equations

• NavierStokes.UniformAngularReset.correctionCenter d = d.releaseStart - 3

noncomputable def NavierStokes.UniformAngularReset.referenceAmplitude (d : OutgoingTail.TailData) : ℝ

Reference amplitude, given by (radialAmplitude d.core.P d.core.dropLength d.core.lam d.flattenEnd / 2) * Real.exp ((1 / 2 + d.core.lam) * d.flattenEnd).

Equations

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

theorem NavierStokes.UniformAngularReset.referenceAmplitude_pos (d : OutgoingTail.TailData) : 0 < referenceAmplitude d

theorem NavierStokes.UniformAngularReset.reference_matches (d : OutgoingTail.TailData) {y : ℝ} (hy : d.flattenEnd ≤ y) : AngularMomentReset.baseE d.core.lam (referenceAmplitude d) y = OutgoingSchedule.radialAmplitude d.core.P d.core.dropLength d.core.lam y / 2

theorem NavierStokes.UniformAngularReset.last_four_after_flatten (d : OutgoingTail.TailData) : d.flattenEnd < d.releaseStart - 4

theorem NavierStokes.UniformAngularReset.original_matches_reference (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : y ∈ Set.Icc (d.releaseStart - 4) d.releaseStart) : OutgoingTail.finalAngular d (y, eta) = AngularMomentReset.baseE d.core.lam (referenceAmplitude d) y

theorem NavierStokes.UniformAngularReset.weighted_baseE (lam e0 y : ℝ) : Real.exp (3 * y / 2) * AngularMomentReset.baseE lam e0 y = e0 * Real.exp ((1 - lam) * y)

theorem NavierStokes.UniformAngularReset.reference_scale (d : OutgoingTail.TailData) : referenceAmplitude d * Real.exp ((1 - d.core.lam) * correctionCenter d) = baseWeight d (correctionCenter d) / 2

theorem NavierStokes.UniformAngularReset.relative_zero_outside (d : OutgoingTail.TailData) (c : AngularMomentReset.Coeff) {y : ℝ} (hy : y ∉ Set.Ioo (d.releaseStart - 4) d.releaseStart) : AngularMomentReset.relative c (y - correctionCenter d) = 0

noncomputable def NavierStokes.UniformAngularReset.correctedAngular (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (p : ℝ × ℝ) : ℝ

The actual complete outgoing angular field after the two relative bumps.

Equations

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

theorem NavierStokes.UniformAngularReset.correctedAngular_contDiff (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ (↑⊤) (correctedAngular d c)

theorem NavierStokes.UniformAngularReset.correctedAngular_unchanged (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) {y : ℝ} (hy : y ∉ Set.Ioo (d.releaseStart - 4) d.releaseStart) : correctedAngular d c (y, eta) = OutgoingTail.finalAngular d (y, eta)

theorem NavierStokes.UniformAngularReset.corrected_matches_reference (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) {y : ℝ} (hy : y ∈ Set.Ioo (d.releaseStart - 4) d.releaseStart) : correctedAngular d c (y, eta) = AngularMomentReset.modifiedE d.core.lam (referenceAmplitude d) (correctionCenter d) (c eta) y

theorem NavierStokes.UniformAngularReset.corrected_difference_reference (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta y : ℝ) : correctedAngular d c (y, eta) - OutgoingTail.finalAngular d (y, eta) = AngularMomentReset.modifiedE d.core.lam (referenceAmplitude d) (correctionCenter d) (c eta) y - AngularMomentReset.baseE d.core.lam (referenceAmplitude d) y

theorem NavierStokes.UniformAngularReset.corrected_pressure_reference (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta y : ℝ) : correctedAngular d c (y, eta) ^ 2 - OutgoingTail.finalAngular d (y, eta) ^ 2 = AngularMomentReset.modifiedE d.core.lam (referenceAmplitude d) (correctionCenter d) (c eta) y ^ 2 - AngularMomentReset.baseE d.core.lam (referenceAmplitude d) y ^ 2

theorem NavierStokes.UniformAngularReset.ResetWitness.positive {d : OutgoingTail.TailData} {K : ℝ} (w : ResetWitness d K) (p : ℝ × ℝ) : 0 < correctedAngular d w.coefficients p

theorem NavierStokes.UniformAngularReset.ResetWitness.logSlope_le {d : OutgoingTail.TailData} {K : ℝ} (w : ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ∈ Set.Ioo (d.releaseStart - 4) d.releaseStart) : AngularMomentReset.logSlope (fun (t : ℝ) => correctedAngular d w.coefficients (t, eta)) y ≤ -d.core.lam / 2

theorem NavierStokes.UniformAngularReset.ResetWitness.pressure_neutral {d : OutgoingTail.TailData} {K : ℝ} (w : ResetWitness d K) (eta : ℝ) : ∫ (y : ℝ), correctedAngular d w.coefficients (y, eta) ^ 2 - OutgoingTail.finalAngular d (y, eta) ^ 2 = 0

theorem NavierStokes.UniformAngularReset.ResetWitness.angular_change {d : OutgoingTail.TailData} {K : ℝ} (w : ResetWitness d K) (eta : ℝ) : ∫ (y : ℝ), Real.exp (3 * y / 2) * (correctedAngular d w.coefficients (y, eta) - OutgoingTail.finalAngular d (y, eta)) = baseWeight d (correctionCenter d) / 2 * normalizedDebt d eta

theorem NavierStokes.UniformAngularReset.integral_edit_window (d : OutgoingTail.TailData) (f : ℝ → ℝ) (hf : ∀ y ∉ Set.Ioo (d.releaseStart - 4) d.releaseStart, f y = 0) : ∫ (y : ℝ) in 0..d.releaseStart, f y = ∫ (y : ℝ), f y

noncomputable def NavierStokes.UniformAngularReset.correctedHistory (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : ℝ

Corrected history, given by (5 / 8) * d.core.P * shape eta + ∫ t in (0 : ℝ)..d.releaseStart, Real.exp (3 * t / 2) * correctedAngular d c (t, eta).

Equations

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

theorem NavierStokes.UniformAngularReset.ResetWitness.exact_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : ResetWitness d K) (eta : ℝ) : correctedHistory d w.coefficients eta = baseWeight d d.releaseStart / (2 * (1 - d.core.lam))

theorem NavierStokes.UniformAngularReset.ResetWitness.pressure_interval_neutral {d : OutgoingTail.TailData} {K : ℝ} (w : ResetWitness d K) (eta : ℝ) : ∫ (y : ℝ) in 0..d.releaseStart, correctedAngular d w.coefficients (y, eta) ^ 2 = ∫ (y : ℝ) in 0..d.releaseStart, OutgoingTail.finalAngular d (y, eta) ^ 2

theorem NavierStokes.UniformAngularReset.ResetWitness.physical_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : ResetWitness d K) (eta : ℝ) : √2 * correctedHistory d w.coefficients eta = Real.exp d.releaseStart * √(2 * Real.exp d.releaseStart) * correctedAngular d w.coefficients (d.releaseStart, eta) / (1 - d.core.lam)

theorem NavierStokes.UniformAngularReset.complete_angular_reset : ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (d : OutgoingTail.TailData), d.core.lam < lam0 → ∃ (c : ℝ → AngularMomentReset.Coeff), ContDiff ℝ (↑⊤) (correctedAngular d c) ∧ (∀ (p : ℝ × ℝ), 0 < correctedAngular d c p) ∧ (∀ (eta y : ℝ), y ∉ Set.Ioo (d.releaseStart - 4) d.releaseStart → correctedAngular d c (y, eta) = OutgoingTail.finalAngular d (y, eta)) ∧ (∀ (eta : ℝ), ∫ (y : ℝ), correctedAngular d c (y, eta) ^ 2 - OutgoingTail.finalAngular d (y, eta) ^ 2 = 0 ∧ √2 * correctedHistory d c eta = Real.exp d.releaseStart * √(2 * Real.exp d.releaseStart) * correctedAngular d c (d.releaseStart, eta) / (1 - d.core.lam)) ∧ ∀ (eta y : ℝ), y ∈ Set.Ioo (d.releaseStart - 4) d.releaseStart → AngularMomentReset.logSlope (fun (t : ℝ) => correctedAngular d c (t, eta)) y ≤ -d.core.lam / 2

The actual complete outgoing profile allows the pressure-neutral angular reset for sufficiently small lam, with a common scalar threshold.

theorem NavierStokes.UniformAngularReset.full_weight_ideal (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : Real.exp (3 * y / 2) * OutgoingTail.finalAngular d (y, eta) = d.core.P * OutgoingSchedule.shape eta * Real.exp (8 / 5 * y)

theorem NavierStokes.UniformAngularReset.history_from_ideal_prefix (d : OutgoingTail.TailData) (eta : ℝ) (f : ℝ → ℝ) (hf : Continuous f) (hprefix : ∀ y ≤ 0, f y = d.core.P * OutgoingSchedule.shape eta * Real.exp (8 / 5 * y)) {y : ℝ} (hy : 0 ≤ y) : MeasureTheory.IntegrableOn f (Set.Iic y) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Iic y, f t = 5 / 8 * d.core.P * OutgoingSchedule.shape eta + ∫ (t : ℝ) in 0..y, f t

The ideal incoming segment fixes the prefix as an actual improper integral.

theorem NavierStokes.UniformAngularReset.fullHistory_eq_integral (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : fullHistory d eta y = ∫ (t : ℝ) in Set.Iic y, Real.exp (3 * t / 2) * OutgoingTail.finalAngular d (t, eta)

theorem NavierStokes.UniformAngularReset.ResetWitness.correctedHistory_eq_integral {d : OutgoingTail.TailData} {K : ℝ} (w : ResetWitness d K) (eta : ℝ) : correctedHistory d w.coefficients eta = ∫ (t : ℝ) in Set.Iic d.releaseStart, Real.exp (3 * t / 2) * correctedAngular d w.coefficients (t, eta)

theorem NavierStokes.UniformAngularReset.ResetWitness.physical_integral_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : ResetWitness d K) (eta : ℝ) : ∫ (t : ℝ) in Set.Iic d.releaseStart, Real.exp t * √(2 * Real.exp t) * correctedAngular d w.coefficients (t, eta) = Real.exp d.releaseStart * √(2 * Real.exp d.releaseStart) * correctedAngular d w.coefficients (d.releaseStart, eta) / (1 - d.core.lam)

The reset identity for the full physical angular integral, including the incoming ideal segment, with X = exp y and H = sqrt (2*X) * E.