Smooth periodic tilt functions and their actual integral moments

This file advances the finite moment calculations in LoopMoments to genuine smooth functions on the real line, with period 2π and actual interval integrals. The cosine construction realizes all nonnegative variances. A separate, explicit amplitude bound is required to preserve the stress projection. Smoothness in parameters is stated using the amplitude, avoiding an incorrect claim of smoothness of the square root at zero variance.

The positive exponential tilt used by the manuscript is also treated below. Neither a smooth variance-inversion theorem nor a full true-cone result is assumed or asserted.

Exact moment algebra for the true-cone loop construction

This file proves the finite-distribution form of the averaging and rephasing identities in Lemma 6.1 of the candidate manuscript. The formulas are algebraic; no existence, smoothness, or invertibility of a circle reparametrization is asserted here. The hypotheses of rephased_moments are ordinary mass, mean, and variance constraints, not an assumption that a desired loop exists.

The final lemmas give explicit two-point distributions with prescribed variance. They establish finite moment feasibility, including a one-sided support bound.

def NavierStokes.LoopMoments.avg {ι : Type u_1} (s : Finset ι) (w f : ι → ℝ) : ℝ

A finite weighted average. We retain the weights explicitly, so no probabilistic or analytic existence assertion is hidden in the notation.

Equations

• NavierStokes.LoopMoments.avg s w f = ∑ i ∈ s, w i * f i

theorem NavierStokes.LoopMoments.avg_add {ι : Type u_1} (s : Finset ι) (w f g : ι → ℝ) : (avg s w fun (i : ι) => f i + g i) = avg s w f + avg s w g

theorem NavierStokes.LoopMoments.avg_sub {ι : Type u_1} (s : Finset ι) (w f g : ι → ℝ) : (avg s w fun (i : ι) => f i - g i) = avg s w f - avg s w g

theorem NavierStokes.LoopMoments.avg_const_mul {ι : Type u_1} (s : Finset ι) (w f : ι → ℝ) (c : ℝ) : (avg s w fun (i : ι) => c * f i) = c * avg s w f

theorem NavierStokes.LoopMoments.avg_const {ι : Type u_1} (s : Finset ι) (w : ι → ℝ) (c : ℝ) (hmass : ∑ i ∈ s, w i = 1) : (avg s w fun (x : ι) => c) = c

theorem NavierStokes.LoopMoments.avg_nonneg {ι : Type u_1} (s : Finset ι) (w f : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hf : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ avg s w f

theorem NavierStokes.LoopMoments.variance_identity {ι : Type u_1} (s : Finset ι) (w t : ι → ℝ) (m : ℝ) (hmass : ∑ i ∈ s, w i = 1) (hmean : avg s w t = m) : (avg s w fun (i : ι) => (t i - m) ^ 2) = (avg s w fun (i : ι) => t i ^ 2) - m ^ 2

The standard variance expansion, with mass and first moment explicit.

theorem NavierStokes.LoopMoments.energy_moment {ι : Type u_1} (s : Finset ι) (w t : ι → ℝ) (a m ρ : ℝ) (ha : a ≠ 0) (hmass : ∑ i ∈ s, w i = 1) (hmean : avg s w t = m) (hvar : (avg s w fun (i : ι) => (t i - m) ^ 2) = ρ / a) : (a * avg s w fun (i : ι) => 1 + t i ^ 2) = a * (1 + m ^ 2) + ρ

This is a ⟨1+t²⟩ = a(1+m²) + ρ from the manuscript.

theorem NavierStokes.LoopMoments.variance_nonneg {ι : Type u_1} (s : Finset ι) (w t : ι → ℝ) (m : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) : 0 ≤ avg s w fun (i : ι) => (t i - m) ^ 2

A nonnegative weighted variance cannot decrease the nominal speed.

theorem NavierStokes.LoopMoments.required_variance_nonneg {ι : Type u_1} (s : Finset ι) (w t : ι → ℝ) (a m ρ : ℝ) (ha : 0 < a) (hw : ∀ i ∈ s, 0 ≤ w i) (hvar : (avg s w fun (i : ι) => (t i - m) ^ 2) = ρ / a) : 0 ≤ ρ

noncomputable def NavierStokes.LoopMoments.phaseDensity (a v t : ℝ) : ℝ

The rephasing density relative to the old averaging parameter.

Equations

• NavierStokes.LoopMoments.phaseDensity a v t = a * (1 + t ^ 2) / v

noncomputable def NavierStokes.LoopMoments.loopA (v t : ℝ) : ℝ

The positive first component of the loop shear.

Equations

• NavierStokes.LoopMoments.loopA v t = v / (1 + t ^ 2)

noncomputable def NavierStokes.LoopMoments.loopC (v t : ℝ) : ℝ

The signed second component; this corresponds to -b_L.

Equations

• NavierStokes.LoopMoments.loopC v t = v * t / (1 + t ^ 2)

theorem NavierStokes.LoopMoments.one_add_sq_pos (t : ℝ) : 0 < 1 + t ^ 2

theorem NavierStokes.LoopMoments.loopA_pos (v t : ℝ) (hv : 0 < v) : 0 < loopA v t

theorem NavierStokes.LoopMoments.phaseDensity_pos (a v t : ℝ) (ha : 0 < a) (hv : 0 < v) : 0 < phaseDensity a v t

theorem NavierStokes.LoopMoments.loop_speed (v t : ℝ) : loopA v t * (1 + t ^ 2) = v

theorem NavierStokes.LoopMoments.loop_slope (v t : ℝ) (hv : v ≠ 0) : loopC v t / loopA v t = t

theorem NavierStokes.LoopMoments.density_times_loopA (a v t : ℝ) (hv : v ≠ 0) : phaseDensity a v t * loopA v t = a

theorem NavierStokes.LoopMoments.density_times_loopC (a v t : ℝ) (hv : v ≠ 0) : phaseDensity a v t * loopC v t = a * t

theorem NavierStokes.LoopMoments.rephased_mass {ι : Type u_1} (s : Finset ι) (w t : ι → ℝ) (a m ρ v : ℝ) (ha : a ≠ 0) (hv : v ≠ 0) (hmass : ∑ i ∈ s, w i = 1) (hmean : avg s w t = m) (hvar : (avg s w fun (i : ι) => (t i - m) ^ 2) = ρ / a) (hspeed : v = a * (1 + m ^ 2) + ρ) : ∑ i ∈ s, w i * phaseDensity a v (t i) = 1

Reweighting by the manuscript's density has total mass one.

theorem NavierStokes.LoopMoments.rephased_meanA {ι : Type u_1} (s : Finset ι) (w t : ι → ℝ) (a v : ℝ) (hv : v ≠ 0) (hmass : ∑ i ∈ s, w i = 1) : (avg s (fun (i : ι) => w i * phaseDensity a v (t i)) fun (i : ι) => loopA v (t i)) = a

The radial shear has the original mean after rephasing.

theorem NavierStokes.LoopMoments.rephased_meanC {ι : Type u_1} (s : Finset ι) (w t : ι → ℝ) (a v m : ℝ) (hv : v ≠ 0) (hmean : avg s w t = m) : (avg s (fun (i : ι) => w i * phaseDensity a v (t i)) fun (i : ι) => loopC v (t i)) = a * m

The signed axial shear has the original mean after rephasing.

theorem NavierStokes.LoopMoments.rephased_moments {ι : Type u_1} (s : Finset ι) (w t : ι → ℝ) (a b ρ v : ℝ) (ha : 0 < a) (hρ : 0 ≤ ρ) (hmass : ∑ i ∈ s, w i = 1) (hmean : avg s w t = -b / a) (hvar : (avg s w fun (i : ι) => (t i - -b / a) ^ 2) = ρ / a) (hspeed : v = a * (1 + (-b / a) ^ 2) + ρ) : ∑ i ∈ s, w i * phaseDensity a v (t i) = 1 ∧ (avg s (fun (i : ι) => w i * phaseDensity a v (t i)) fun (i : ι) => loopA v (t i)) = a ∧ (avg s (fun (i : ι) => w i * phaseDensity a v (t i)) fun (i : ι) => loopC v (t i)) = -b

With m = -b/a, the two rephased means are exactly (a,-b).

structure NavierStokes.LoopMoments.TwoPoint : Type

A two-point probability law. This is a concrete finite object, without any hypothesis asserting the existence of the manuscript's smooth loop.

• leftWeight : ℝ

  Left weight of TwoPoint, of type ℝ.

• rightWeight : ℝ

  Right weight of TwoPoint, of type ℝ.

• leftValue : ℝ

  Left value of TwoPoint, of type ℝ.

• rightValue : ℝ

  Right value of TwoPoint, of type ℝ.

def NavierStokes.LoopMoments.TwoPoint.mean (q : TwoPoint) : ℝ

Mean, given by q.leftWeight * q.leftValue + q.rightWeight * q.rightValue.

Equations

• q.mean = q.leftWeight * q.leftValue + q.rightWeight * q.rightValue

def NavierStokes.LoopMoments.TwoPoint.centeredSecond (q : TwoPoint) (m : ℝ) : ℝ

Centered second, given by q.leftWeight * (q.leftValue - m) ^ 2 + q.rightWeight * (q.rightValue - m) ^ 2.

Equations

• q.centeredSecond m = q.leftWeight * (q.leftValue - m) ^ 2 + q.rightWeight * (q.rightValue - m) ^ 2

def NavierStokes.LoopMoments.TwoPoint.IsProbability (q : TwoPoint) : Prop

Is probability, given by 0 ≤ q.leftWeight ∧ 0 ≤ q.rightWeight ∧ q.leftWeight + q.rightWeight = 1.

Equations

• q.IsProbability = (0 ≤ q.leftWeight ∧ 0 ≤ q.rightWeight ∧ q.leftWeight + q.rightWeight = 1)

noncomputable def NavierStokes.LoopMoments.symmetricPair (m V : ℝ) : TwoPoint

For any nonnegative variance, equal masses at m ± √V realize it.

Equations

• NavierStokes.LoopMoments.symmetricPair m V = { leftWeight := 1 / 2, rightWeight := 1 / 2, leftValue := m - √V, rightValue := m + √V }

theorem NavierStokes.LoopMoments.symmetricPair_probability (m V : ℝ) : (symmetricPair m V).IsProbability

theorem NavierStokes.LoopMoments.symmetricPair_mean (m V : ℝ) : (symmetricPair m V).mean = m

theorem NavierStokes.LoopMoments.symmetricPair_variance (m V : ℝ) (hV : 0 ≤ V) : (symmetricPair m V).centeredSecond m = V

noncomputable def NavierStokes.LoopMoments.oneSidedPair (m p d V : ℝ) : TwoPoint

An asymmetric law preserves a lower bound on the projection p*t, while allowing any nonnegative variance. For p = 0, use symmetricPair. The lower projected deviation is -d, and the upper one is V*p²/d.

Equations

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

theorem NavierStokes.LoopMoments.oneSidedPair_denom_pos (p d V : ℝ) (hd : 0 < d) (hV : 0 ≤ V) : 0 < d ^ 2 + V * p ^ 2

theorem NavierStokes.LoopMoments.oneSidedPair_probability (m p d V : ℝ) (hd : 0 < d) (hV : 0 ≤ V) : (oneSidedPair m p d V).IsProbability

theorem NavierStokes.LoopMoments.oneSidedPair_mean (m p d V : ℝ) (hp : p ≠ 0) (hd : 0 < d) (hV : 0 ≤ V) : (oneSidedPair m p d V).mean = m

theorem NavierStokes.LoopMoments.oneSidedPair_variance (m p d V : ℝ) (hp : p ≠ 0) (hd : 0 < d) (hV : 0 ≤ V) : (oneSidedPair m p d V).centeredSecond m = V

theorem NavierStokes.LoopMoments.oneSidedPair_lower_projection (m p d V : ℝ) (hp : p ≠ 0) : p * ((oneSidedPair m p d V).leftValue - m) = -d

theorem NavierStokes.LoopMoments.oneSidedPair_upper_projection (m p d V : ℝ) : p * ((oneSidedPair m p d V).rightValue - m) = V * p ^ 2 / d

theorem NavierStokes.LoopMoments.exists_projected_twoPoint (p₁ p₂ m V : ℝ) (hP : 2 < p₁ + p₂ * m) (hV : 0 ≤ V) : ∃ (q : TwoPoint), q.IsProbability ∧ q.mean = m ∧ q.centeredSecond m = V ∧ 2 < p₁ + p₂ * q.leftValue ∧ 2 < p₁ + p₂ * q.rightValue

Every mean whose stress projection is strictly above 2 has a finite two-point distribution with any prescribed nonnegative variance, with both support points still strictly above that same projection threshold. This is a feasibility statement for the tilt moments, not the full true-cone test.

theorem NavierStokes.LoopMoments.corrected_speed_bounds (v₀ vstar ζ : ℝ) (hz₀ : 0 ≤ ζ) (hz₁ : ζ ≤ 1) (hv : v₀ ≤ vstar) : v₀ ≤ v₀ + ζ ^ 2 * (vstar - v₀) ∧ v₀ + ζ ^ 2 * (vstar - v₀) ≤ vstar

The cutoff correction used by the manuscript remains between the old speed and the target speed whenever the old speed is below that target.

noncomputable def NavierStokes.SmoothLoop.angularMean (f : ℝ → ℝ) : ℝ

Angular average over one full turn.

Equations

• NavierStokes.SmoothLoop.angularMean f = (∫ (θ : ℝ) in 0..2 * Real.pi, f θ) / (2 * Real.pi)

theorem NavierStokes.SmoothLoop.period_pos : 0 < 2 * Real.pi

theorem NavierStokes.SmoothLoop.period_ne_zero : 2 * Real.pi ≠ 0

theorem NavierStokes.SmoothLoop.angularMean_const (c : ℝ) : (angularMean fun (x : ℝ) => c) = c

theorem NavierStokes.SmoothLoop.angularMean_add (f g : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) : (angularMean fun (θ : ℝ) => f θ + g θ) = angularMean f + angularMean g

theorem NavierStokes.SmoothLoop.angularMean_sub (f g : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) : (angularMean fun (θ : ℝ) => f θ - g θ) = angularMean f - angularMean g

theorem NavierStokes.SmoothLoop.angularMean_const_mul (c : ℝ) (f : ℝ → ℝ) : (angularMean fun (θ : ℝ) => c * f θ) = c * angularMean f

theorem NavierStokes.SmoothLoop.angularMean_div_const (f : ℝ → ℝ) (c : ℝ) : (angularMean fun (θ : ℝ) => f θ / c) = angularMean f / c

theorem NavierStokes.SmoothLoop.angularMean_nonneg (f : ℝ → ℝ) (hf : ∀ (θ : ℝ), 0 ≤ f θ) : 0 ≤ angularMean f

theorem NavierStokes.SmoothLoop.angularMean_pos (f : ℝ → ℝ) (hf : Continuous f) (hpos : ∀ (θ : ℝ), 0 < f θ) : 0 < angularMean f

theorem NavierStokes.SmoothLoop.angularMean_cos : angularMean Real.cos = 0

theorem NavierStokes.SmoothLoop.angularMean_cos_sq : (angularMean fun (θ : ℝ) => Real.cos θ ^ 2) = 1 / 2

noncomputable def NavierStokes.SmoothLoop.cosineTilt (m amplitude θ : ℝ) : ℝ

A smooth tilt parametrized by its mean and its (signed) amplitude.

Equations

• NavierStokes.SmoothLoop.cosineTilt m amplitude θ = m + amplitude * Real.cos θ

theorem NavierStokes.SmoothLoop.cosineTilt_periodic (m amplitude : ℝ) : Function.Periodic (cosineTilt m amplitude) (2 * Real.pi)

theorem NavierStokes.SmoothLoop.cosineTilt_contDiff (m amplitude : ℝ) : ContDiff ℝ (↑⊤) (cosineTilt m amplitude)

theorem NavierStokes.SmoothLoop.cosineTilt_joint_contDiff : ContDiff ℝ ↑⊤ fun (x : (ℝ × ℝ) × ℝ) => cosineTilt x.1.1 x.1.2 x.2

Joint smoothness in mean, amplitude, and angle.

theorem NavierStokes.SmoothLoop.cosineTilt_mean (m amplitude : ℝ) : angularMean (cosineTilt m amplitude) = m

theorem NavierStokes.SmoothLoop.cosineTilt_variance (m amplitude : ℝ) : (angularMean fun (θ : ℝ) => (cosineTilt m amplitude θ - m) ^ 2) = amplitude ^ 2 / 2

theorem NavierStokes.SmoothLoop.exists_cosine_moments (m V : ℝ) (hV : 0 ≤ V) : ∃ (t : ℝ → ℝ), ContDiff ℝ (↑⊤) t ∧ Function.Periodic t (2 * Real.pi) ∧ angularMean t = m ∧ (angularMean fun (θ : ℝ) => (t θ - m) ^ 2) = V

Actual smooth periodic functions realize every nonnegative variance.

theorem NavierStokes.SmoothLoop.cosineTilt_projection_bound (p₁ p₂ m amplitude θ : ℝ) : p₁ + p₂ * m - |p₂ * amplitude| ≤ p₁ + p₂ * cosineTilt m amplitude θ

The full range is controlled by the amplitude, uniformly in the angle.

theorem NavierStokes.SmoothLoop.cosineTilt_stress_positive (p₁ p₂ m amplitude : ℝ) (hmargin : 2 + |p₂ * amplitude| < p₁ + p₂ * m) (θ : ℝ) : 2 < p₁ + p₂ * cosineTilt m amplitude θ

theorem NavierStokes.SmoothLoop.exists_cosine_moments_with_projection (p₁ p₂ m V : ℝ) (hV : 0 ≤ V) (hmargin : 2 + |p₂ * √(2 * V)| < p₁ + p₂ * m) : ∃ (t : ℝ → ℝ), ContDiff ℝ (↑⊤) t ∧ Function.Periodic t (2 * Real.pi) ∧ angularMean t = m ∧ (angularMean fun (θ : ℝ) => (t θ - m) ^ 2) = V ∧ ∀ (θ : ℝ), 2 < p₁ + p₂ * t θ

Sufficient projection margin for the explicit prescribed-variance loop. The margin is an additional hypothesis, not a consequence of P>2.

theorem NavierStokes.SmoothLoop.cosineTilt_smooth_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (m amplitude : E → ℝ) (hm : ContDiff ℝ (↑⊤) m) (hamp : ContDiff ℝ (↑⊤) amplitude) : ContDiff ℝ ↑⊤ fun (x : E × ℝ) => cosineTilt (m x.1) (amplitude x.1) x.2

Smooth parameter data remain smooth when the chosen signed amplitude is smooth. In particular, a smooth square root of a variance correction can be used without asserting that square root is smooth on all of [0,∞).

theorem NavierStokes.SmoothLoop.angular_variance_identity (t : ℝ → ℝ) (m : ℝ) (ht : Continuous t) (hmean : angularMean t = m) : (angularMean fun (θ : ℝ) => (t θ - m) ^ 2) = (angularMean fun (θ : ℝ) => t θ ^ 2) - m ^ 2

Variance expansion for actual angular integrals.

theorem NavierStokes.SmoothLoop.angular_energy_moment (t : ℝ → ℝ) (a m ρ : ℝ) (ha : a ≠ 0) (ht : Continuous t) (hmean : angularMean t = m) (hvar : (angularMean fun (θ : ℝ) => (t θ - m) ^ 2) = ρ / a) : (a * angularMean fun (θ : ℝ) => 1 + t θ ^ 2) = a * (1 + m ^ 2) + ρ

theorem NavierStokes.SmoothLoop.angular_rephasing_moments (t : ℝ → ℝ) (a m ρ v : ℝ) (ha : a ≠ 0) (hv : v ≠ 0) (ht : Continuous t) (hmean : angularMean t = m) (hvar : (angularMean fun (θ : ℝ) => (t θ - m) ^ 2) = ρ / a) (hspeed : v = a * (1 + m ^ 2) + ρ) : (angularMean fun (θ : ℝ) => LoopMoments.phaseDensity a v (t θ)) = 1 ∧ (angularMean fun (θ : ℝ) => LoopMoments.phaseDensity a v (t θ) * LoopMoments.loopA v (t θ)) = a ∧ (angularMean fun (θ : ℝ) => LoopMoments.phaseDensity a v (t θ) * LoopMoments.loopC v (t θ)) = a * m

theorem NavierStokes.SmoothLoop.smooth_loop_shears (t : ℝ → ℝ) (v : ℝ) (ht : ContDiff ℝ (↑⊤) t) : (ContDiff ℝ ↑⊤ fun (θ : ℝ) => LoopMoments.loopA v (t θ)) ∧ ContDiff ℝ ↑⊤ fun (θ : ℝ) => LoopMoments.loopC v (t θ)

theorem NavierStokes.SmoothLoop.periodic_loop_shears (t : ℝ → ℝ) (v : ℝ) (ht : Function.Periodic t (2 * Real.pi)) : Function.Periodic (fun (θ : ℝ) => LoopMoments.loopA v (t θ)) (2 * Real.pi) ∧ Function.Periodic (fun (θ : ℝ) => LoopMoments.loopC v (t θ)) (2 * Real.pi)

noncomputable def NavierStokes.SmoothLoop.expNormalizer (s : ℝ) : ℝ

The normalizing angular mean in the manuscript's exponential family, using cosine instead of sine (a translation of the angular origin).

Equations

• NavierStokes.SmoothLoop.expNormalizer s = NavierStokes.SmoothLoop.angularMean fun (θ : ℝ) => Real.exp (s * Real.cos θ)

theorem NavierStokes.SmoothLoop.expNormalizer_pos (s : ℝ) : 0 < expNormalizer s

theorem NavierStokes.SmoothLoop.expNormalizer_zero : expNormalizer 0 = 1

noncomputable def NavierStokes.SmoothLoop.normalizedExp (s θ : ℝ) : ℝ

Normalized exp, given by Real.exp (s * Real.cos θ) / expNormalizer s.

Equations

• NavierStokes.SmoothLoop.normalizedExp s θ = Real.exp (s * Real.cos θ) / NavierStokes.SmoothLoop.expNormalizer s

theorem NavierStokes.SmoothLoop.normalizedExp_pos (s θ : ℝ) : 0 < normalizedExp s θ

theorem NavierStokes.SmoothLoop.normalizedExp_contDiff (s : ℝ) : ContDiff ℝ (↑⊤) (normalizedExp s)

theorem NavierStokes.SmoothLoop.normalizedExp_periodic (s : ℝ) : Function.Periodic (normalizedExp s) (2 * Real.pi)

theorem NavierStokes.SmoothLoop.normalizedExp_mean (s : ℝ) : angularMean (normalizedExp s) = 1

theorem NavierStokes.SmoothLoop.normalizedExp_second_moment (s : ℝ) : (angularMean fun (θ : ℝ) => normalizedExp s θ ^ 2) = expNormalizer (2 * s) / expNormalizer s ^ 2

theorem NavierStokes.SmoothLoop.normalizedExp_variance (s : ℝ) : (angularMean fun (θ : ℝ) => (normalizedExp s θ - 1) ^ 2) = expNormalizer (2 * s) / expNormalizer s ^ 2 - 1

noncomputable def NavierStokes.SmoothLoop.expTilt (m d μ p θ : ℝ) : ℝ

The divided exponential tilt. Its smooth extension at p=0 is handled separately below; this expression by itself is not that extension.

Equations

• NavierStokes.SmoothLoop.expTilt m d μ p θ = m + d / p * (NavierStokes.SmoothLoop.normalizedExp (μ * p) θ - 1)

theorem NavierStokes.SmoothLoop.expTilt_contDiff (m d μ p : ℝ) : ContDiff ℝ (↑⊤) (expTilt m d μ p)

theorem NavierStokes.SmoothLoop.expTilt_periodic (m d μ p : ℝ) : Function.Periodic (expTilt m d μ p) (2 * Real.pi)

theorem NavierStokes.SmoothLoop.expTilt_mean (m d μ p : ℝ) : angularMean (expTilt m d μ p) = m

theorem NavierStokes.SmoothLoop.expTilt_variance (m d μ p : ℝ) : (angularMean fun (θ : ℝ) => (expTilt m d μ p θ - m) ^ 2) = (d / p) ^ 2 * (expNormalizer (2 * (μ * p)) / expNormalizer (μ * p) ^ 2 - 1)

theorem NavierStokes.SmoothLoop.expTilt_projection (p₁ p₂ m d μ θ : ℝ) (hp : p₂ ≠ 0) : p₁ + p₂ * expTilt m d μ p₂ θ = p₁ + p₂ * m - d + d * normalizedExp (μ * p₂) θ

theorem NavierStokes.SmoothLoop.expTilt_projection_lower (p₁ p₂ m d μ : ℝ) (hp : p₂ ≠ 0) (hd : 0 < d) (θ : ℝ) : p₁ + p₂ * m - d < p₁ + p₂ * expTilt m d μ p₂ θ

noncomputable def NavierStokes.SmoothLoop.extendedExpTilt (m d μ p : ℝ) : ℝ → ℝ

Correct value at vanishing transverse stress. Smooth dependence across p=0 is a separate analytic obligation; only angular smoothness is proved.

Equations

• NavierStokes.SmoothLoop.extendedExpTilt m d μ p = if p = 0 then NavierStokes.SmoothLoop.cosineTilt m (d * μ) else NavierStokes.SmoothLoop.expTilt m d μ p

theorem NavierStokes.SmoothLoop.extendedExpTilt_contDiff (m d μ p : ℝ) : ContDiff ℝ (↑⊤) (extendedExpTilt m d μ p)

theorem NavierStokes.SmoothLoop.extendedExpTilt_periodic (m d μ p : ℝ) : Function.Periodic (extendedExpTilt m d μ p) (2 * Real.pi)

theorem NavierStokes.SmoothLoop.extendedExpTilt_mean (m d μ p : ℝ) : angularMean (extendedExpTilt m d μ p) = m

theorem NavierStokes.SmoothLoop.extendedExpTilt_variance_zero (m d μ : ℝ) : (angularMean fun (θ : ℝ) => (extendedExpTilt m d μ 0 θ - m) ^ 2) = d ^ 2 * μ ^ 2 / 2

theorem NavierStokes.SmoothLoop.extendedExpTilt_projection_positive (p₁ p₂ m d μ : ℝ) (hd : 0 < d) (hmargin : 2 ≤ p₁ + p₂ * m - d) (θ : ℝ) : 2 < p₁ + p₂ * extendedExpTilt m d μ p₂ θ

structure NavierStokes.SmoothLoop.CircleDensity : Type

A positive normalized density on a circle, given as a smooth periodic function on its universal covering line. The construction densityOfTilt below supplies these data from the already proved moment identity.

• rate : ℝ → ℝ

  Rate of CircleDensity, of type ℝ → ℝ.

• smooth : ContDiff ℝ (↑⊤) self.rate
• positive (θ : ℝ) : 0 < self.rate θ
• periodic : Function.Periodic self.rate (2 * Real.pi)
• integral_one : ∫ (θ : ℝ) in 0..2 * Real.pi, self.rate θ = 1

noncomputable def NavierStokes.SmoothLoop.phaseMap (d : CircleDensity) (θ : ℝ) : ℝ

Phase map, given by ∫ x in (0 : ℝ)..θ, d.rate x.

Equations

• NavierStokes.SmoothLoop.phaseMap d θ = ∫ (x : ℝ) in 0..θ, d.rate x

theorem NavierStokes.SmoothLoop.phaseMap_hasDerivAt (d : CircleDensity) (θ : ℝ) : HasDerivAt (phaseMap d) (d.rate θ) θ

theorem NavierStokes.SmoothLoop.phaseMap_contDiff (d : CircleDensity) : ContDiff ℝ (↑⊤) (phaseMap d)

theorem NavierStokes.SmoothLoop.phaseMap_strictMono (d : CircleDensity) : StrictMono (phaseMap d)

theorem NavierStokes.SmoothLoop.phaseMap_zero (d : CircleDensity) : phaseMap d 0 = 0

theorem NavierStokes.SmoothLoop.phaseMap_fullTurn (d : CircleDensity) : phaseMap d (2 * Real.pi) = 1

theorem NavierStokes.SmoothLoop.phaseMap_add_fullTurn (d : CircleDensity) (θ : ℝ) : phaseMap d (θ + 2 * Real.pi) = phaseMap d θ + 1

theorem NavierStokes.SmoothLoop.phaseMap_int_fullTurn (d : CircleDensity) (n : ℤ) : phaseMap d (↑n * (2 * Real.pi)) = ↑n

theorem NavierStokes.SmoothLoop.phaseMap_surjective (d : CircleDensity) : Function.Surjective (phaseMap d)

noncomputable def NavierStokes.SmoothLoop.phaseHomeomorph (d : CircleDensity) : ℝ ≃ₜ ℝ

The phase map is an actual global homeomorphism, not an assumed inverse.

Equations

• NavierStokes.SmoothLoop.phaseHomeomorph d = (StrictMono.orderIsoOfSurjective (NavierStokes.SmoothLoop.phaseMap d) ⋯ ⋯).toHomeomorph

theorem NavierStokes.SmoothLoop.phaseHomeomorph_apply (d : CircleDensity) (θ : ℝ) : (phaseHomeomorph d) θ = phaseMap d θ

theorem NavierStokes.SmoothLoop.phaseInverse_contDiff (d : CircleDensity) : ContDiff ℝ ↑⊤ ⇑(phaseHomeomorph d).symm

theorem NavierStokes.SmoothLoop.phaseInverse_add_one (d : CircleDensity) (φ : ℝ) : (phaseHomeomorph d).symm (φ + 1) = (phaseHomeomorph d).symm φ + 2 * Real.pi

noncomputable def NavierStokes.SmoothLoop.rephase (d : CircleDensity) (f : ℝ → ℝ) (φ : ℝ) : ℝ

Rephase, given by f ((phaseHomeomorph d).symm φ).

Equations

• NavierStokes.SmoothLoop.rephase d f φ = f ((NavierStokes.SmoothLoop.phaseHomeomorph d).symm φ)

theorem NavierStokes.SmoothLoop.rephase_contDiff (d : CircleDensity) (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (rephase d f)

theorem NavierStokes.SmoothLoop.rephase_periodic (d : CircleDensity) (f : ℝ → ℝ) (hf : Function.Periodic f (2 * Real.pi)) : Function.Periodic (rephase d f) 1

theorem NavierStokes.SmoothLoop.rephase_phaseMap (d : CircleDensity) (f : ℝ → ℝ) (θ : ℝ) : rephase d f (phaseMap d θ) = f θ

theorem NavierStokes.SmoothLoop.integral_rephase (d : CircleDensity) (f : ℝ → ℝ) (hf : Continuous f) : ∫ (φ : ℝ) in 0..1, rephase d f φ = ∫ (θ : ℝ) in 0..2 * Real.pi, f θ * d.rate θ

The actual change of variables for the constructed smooth inverse.

noncomputable def NavierStokes.SmoothLoop.densityOfTilt (t : ℝ → ℝ) (a m ρ v : ℝ) (ha : 0 < a) (hv : 0 < v) (ht : ContDiff ℝ (↑⊤) t) (hperiodic : Function.Periodic t (2 * Real.pi)) (hmean : angularMean t = m) (hvar : (angularMean fun (θ : ℝ) => (t θ - m) ^ 2) = ρ / a) (hspeed : v = a * (1 + m ^ 2) + ρ) : CircleDensity

Density of tilt, bundling rate, smooth, positive, periodic and the required compatibility proofs.

Equations

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

theorem NavierStokes.SmoothLoop.exists_rephased_shear_loop (t : ℝ → ℝ) (a m ρ v : ℝ) (ha : 0 < a) (hv : 0 < v) (ht : ContDiff ℝ (↑⊤) t) (hperiodic : Function.Periodic t (2 * Real.pi)) (hmean : angularMean t = m) (hvar : (angularMean fun (θ : ℝ) => (t θ - m) ^ 2) = ρ / a) (hspeed : v = a * (1 + m ^ 2) + ρ) : ∃ (A : ℝ → ℝ) (C : ℝ → ℝ), ContDiff ℝ (↑⊤) A ∧ ContDiff ℝ (↑⊤) C ∧ Function.Periodic A 1 ∧ Function.Periodic C 1 ∧ ∫ (φ : ℝ) in 0..1, A φ = a ∧ ∫ (φ : ℝ) in 0..1, C φ = a * m ∧ ∀ (φ : ℝ), 0 < A φ ∧ A φ * (1 + (C φ / A φ) ^ 2) = v

A complete reparametrization theorem: ordinary mean/variance data produce actual smooth period-one shear functions with the prescribed unweighted integrals. The radial-speed identity is pointwise. No cone condition is included, since that requires further inequalities on the chosen tilts.

theorem NavierStokes.SmoothLoop.rephase_slope (d : CircleDensity) (t : ℝ → ℝ) (v φ : ℝ) (hv : v ≠ 0) : rephase d (fun (θ : ℝ) => LoopMoments.loopC v (t θ)) φ / rephase d (fun (θ : ℝ) => LoopMoments.loopA v (t θ)) φ = t ((phaseHomeomorph d).symm φ)

theorem NavierStokes.SmoothLoop.rephase_preserves_slope_condition (d : CircleDensity) (t : ℝ → ℝ) (v : ℝ) (hv : v ≠ 0) (R : ℝ → Prop) (hR : ∀ (θ : ℝ), R (t θ)) (φ : ℝ) : R (rephase d (fun (θ : ℝ) => LoopMoments.loopC v (t θ)) φ / rephase d (fun (θ : ℝ) => LoopMoments.loopA v (t θ)) φ)

Any verified slope condition survives the constructed phase change.

theorem NavierStokes.SmoothLoop.rephase_projection_positive (d : CircleDensity) (t : ℝ → ℝ) (p₁ p₂ v : ℝ) (hv : v ≠ 0) (hprojection : ∀ (θ : ℝ), 2 < p₁ + p₂ * t θ) (φ : ℝ) : 2 < p₁ + p₂ * (rephase d (fun (θ : ℝ) => LoopMoments.loopC v (t θ)) φ / rephase d (fun (θ : ℝ) => LoopMoments.loopA v (t θ)) φ)

theorem NavierStokes.SmoothLoop.exists_prescribed_mean_shear_loop (a b ρ : ℝ) (ha : 0 < a) (hρ : 0 ≤ ρ) : ∃ (A : ℝ → ℝ) (C : ℝ → ℝ), ContDiff ℝ (↑⊤) A ∧ ContDiff ℝ (↑⊤) C ∧ Function.Periodic A 1 ∧ Function.Periodic C 1 ∧ ∫ (φ : ℝ) in 0..1, A φ = a ∧ ∫ (φ : ℝ) in 0..1, C φ = -b ∧ ∀ (φ : ℝ), 0 < A φ ∧ A φ * (1 + (C φ / A φ) ^ 2) = a * (1 + (-b / a) ^ 2) + ρ

A fully constructed period-one shear loop for arbitrary positive first mean and nonnegative variance increment. No seed function or inverse is assumed. The speed increase is exactly the specified ρ.

theorem NavierStokes.SmoothLoop.rephase_const (d : CircleDensity) (c : ℝ) : (rephase d fun (x : ℝ) => c) = fun (x : ℝ) => c

theorem NavierStokes.SmoothLoop.zero_amplitude_is_nominal (d : CircleDensity) (a m : ℝ) : ((rephase d fun (θ : ℝ) => LoopMoments.loopA (a * (1 + m ^ 2)) (cosineTilt m 0 θ)) = fun (x : ℝ) => a) ∧ (rephase d fun (θ : ℝ) => LoopMoments.loopC (a * (1 + m ^ 2)) (cosineTilt m 0 θ)) = fun (x : ℝ) => a * m

At zero amplitude the loop shears are exactly the nominal constants, independently of the phase parametrization.