Documentation

LeanPool.NavierStokesAndEuler.NavierStokes.ParametricModulation

Joint periodic primitives and realization of the constructed true-cone loops #

The primitives in this file are actual normalized interval integrals. Their joint smoothness is derived through compact-interval parameter integration.

Construction of the true-cone loop #

This file assembles the actual exponential moment inverse, a smooth speed correction, compact uniform cone margins, and the smooth phase change.

The actual exponential tilt variance #

This file studies the integral normalizer and variance used by Lemma 6.1. All moments below are Lebesgue integrals of the actual cosine exponential family, not postulated properties of an abstract variance map.

noncomputable def NavierStokes.LoopVariance.angleMeasure :

MeasureTheory.Measure ℝ

Angle measure, given by volume.restrict (Ioc 0 (2 * Real.pi)).

Equations

NavierStokes.LoopVariance.angleMeasure = MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))

Instances For

theorem NavierStokes.LoopVariance.integrable_exp_cos (s : ℝ) :

MeasureTheory.Integrable (fun (θ : ℝ) => Real.exp (s * Real.cos θ)) angleMeasure

theorem NavierStokes.LoopVariance.integrableExpSet_cos :

ProbabilityTheory.integrableExpSet Real.cos angleMeasure = Set.univ

theorem NavierStokes.LoopVariance.mem_interior_integrableExpSet (s : ℝ) :

s ∈ interior (ProbabilityTheory.integrableExpSet Real.cos angleMeasure)

noncomputable def NavierStokes.LoopVariance.moment (n : ℕ) (s : ℝ) :

The angular exponential moments, including the normalizer at order zero.

Equations

NavierStokes.LoopVariance.moment n s = (∫ (θ : ℝ), Real.cos θ ^ n * Real.exp (s * Real.cos θ) ∂NavierStokes.LoopVariance.angleMeasure) / (2 * Real.pi)

Instances For

theorem NavierStokes.LoopVariance.moment_eq_angularMean (n : ℕ) (s : ℝ) :

moment n s = SmoothLoop.angularMean fun (θ : ℝ) => Real.cos θ ^ n * Real.exp (s * Real.cos θ)

theorem NavierStokes.LoopVariance.normalizer_eq_moment (s : ℝ) :

SmoothLoop.expNormalizer s = moment 0 s

theorem NavierStokes.LoopVariance.moment_zero_pos (s : ℝ) :

0 < moment 0 s

theorem NavierStokes.LoopVariance.moment_hasDerivAt (n : ℕ) (s : ℝ) :

HasDerivAt (moment n) (moment (n + 1) s) s

theorem NavierStokes.LoopVariance.moment_analyticAt (n : ℕ) (s : ℝ) :

AnalyticAt ℝ (moment n) s

theorem NavierStokes.LoopVariance.moment_contDiff (n : ℕ) :

ContDiff ℝ (↑⊤) (moment n)

theorem NavierStokes.LoopVariance.normalizer_analyticAt (s : ℝ) :

AnalyticAt ℝ SmoothLoop.expNormalizer s

theorem NavierStokes.LoopVariance.normalizer_contDiff :

ContDiff ℝ (↑⊤) SmoothLoop.expNormalizer

theorem NavierStokes.LoopVariance.normalizer_hasDerivAt (s : ℝ) :

HasDerivAt SmoothLoop.expNormalizer (moment 1 s) s

noncomputable def NavierStokes.LoopVariance.weightedSquare (s c : ℝ) :

Weighted square, given by angularMean (fun θ => (Real.cos θ - c) ^ 2 * Real.exp (s * Real.cos θ)).

Equations

NavierStokes.LoopVariance.weightedSquare s c = NavierStokes.SmoothLoop.angularMean fun (θ : ℝ) => (Real.cos θ - c) ^ 2 * Real.exp (s * Real.cos θ)

Instances For

theorem NavierStokes.LoopVariance.weightedSquare_pos (s c : ℝ) :

0 < weightedSquare s c

theorem NavierStokes.LoopVariance.weightedSquare_expansion (s c : ℝ) :

weightedSquare s c = moment 2 s - 2 * c * moment 1 s + c ^ 2 * moment 0 s

noncomputable def NavierStokes.LoopVariance.logSlope (s : ℝ) :

Log slope, given by moment 1 s / moment 0 s.

Equations

NavierStokes.LoopVariance.logSlope s = NavierStokes.LoopVariance.moment 1 s / NavierStokes.LoopVariance.moment 0 s

Instances For

theorem NavierStokes.LoopVariance.moment_determinant_pos (s : ℝ) :

0 < moment 2 s * moment 0 s - moment 1 s ^ 2

theorem NavierStokes.LoopVariance.logSlope_hasDerivAt (s : ℝ) :

HasDerivAt logSlope ((moment 2 s * moment 0 s - moment 1 s ^ 2) / moment 0 s ^ 2) s

theorem NavierStokes.LoopVariance.logSlope_strictMono :

StrictMono logSlope

noncomputable def NavierStokes.LoopVariance.baseVariance (s : ℝ) :

The variance of the normalized exponential density itself. The scaled tilt variance is obtained by multiplication and the substitution s=μp.

Equations

NavierStokes.LoopVariance.baseVariance s = NavierStokes.SmoothLoop.expNormalizer (2 * s) / NavierStokes.SmoothLoop.expNormalizer s ^ 2 - 1

Instances For

theorem NavierStokes.LoopVariance.baseVariance_eq_integral (s : ℝ) :

baseVariance s = SmoothLoop.angularMean fun (θ : ℝ) => (SmoothLoop.normalizedExp s θ - 1) ^ 2

theorem NavierStokes.LoopVariance.baseVariance_zero :

baseVariance 0 = 0

theorem NavierStokes.LoopVariance.baseVariance_nonneg (s : ℝ) :

0 ≤ baseVariance s

theorem NavierStokes.LoopVariance.baseVariance_add_one_pos (s : ℝ) :

0 < baseVariance s + 1

theorem NavierStokes.LoopVariance.baseVariance_analyticAt (s : ℝ) :

AnalyticAt ℝ baseVariance s

theorem NavierStokes.LoopVariance.baseVariance_contDiff :

ContDiff ℝ (↑⊤) baseVariance

theorem NavierStokes.LoopVariance.baseVariance_hasDerivAt (s : ℝ) :

HasDerivAt baseVariance (2 * (baseVariance s + 1) * (logSlope (2 * s) - logSlope s)) s

theorem NavierStokes.LoopVariance.baseVariance_deriv_pos {s : ℝ} (hs : 0 < s) :

0 < deriv baseVariance s

theorem NavierStokes.LoopVariance.baseVariance_strictMonoOn :

StrictMonoOn baseVariance (Set.Ici 0)

theorem NavierStokes.LoopVariance.normalizer_even (s : ℝ) :

SmoothLoop.expNormalizer (-s) = SmoothLoop.expNormalizer s

theorem NavierStokes.LoopVariance.baseVariance_even (s : ℝ) :

baseVariance (-s) = baseVariance s

theorem NavierStokes.LoopVariance.baseVariance_pos {s : ℝ} (hs : s ≠ 0) :

0 < baseVariance s

theorem NavierStokes.LoopVariance.moment_zero_at_zero :

moment 0 0 = 1

theorem NavierStokes.LoopVariance.moment_one_at_zero :

moment 1 0 = 0

theorem NavierStokes.LoopVariance.moment_two_at_zero :

moment 2 0 = 1 / 2

theorem NavierStokes.LoopVariance.logSlope_zero :

theorem NavierStokes.LoopVariance.logSlope_hasDerivAt_zero :

HasDerivAt logSlope (1 / 2) 0

theorem NavierStokes.LoopVariance.baseVariance_hasDerivAt_zero :

HasDerivAt baseVariance 0 0

theorem NavierStokes.LoopVariance.baseVariance_deriv_zero :

deriv baseVariance 0 = 0

theorem NavierStokes.LoopVariance.baseVariance_deriv_hasDerivAt_zero :

HasDerivAt (deriv baseVariance) 1 0

theorem NavierStokes.LoopVariance.baseVariance_second_deriv_zero :

iteratedDeriv 2 baseVariance 0 = 1

noncomputable def NavierStokes.LoopVariance.quadraticFactor :

The second divided difference extends R(s)/s² analytically across zero.

Equations

NavierStokes.LoopVariance.quadraticFactor = dslope (dslope NavierStokes.LoopVariance.baseVariance 0) 0

Instances For

theorem NavierStokes.LoopVariance.quadraticFactor_zero :

quadraticFactor 0 = 1 / 2

theorem NavierStokes.LoopVariance.quadraticFactor_identity (s : ℝ) :

baseVariance s = s ^ 2 * quadraticFactor s

theorem NavierStokes.LoopVariance.quadraticFactor_analyticAt (s : ℝ) :

AnalyticAt ℝ quadraticFactor s

theorem NavierStokes.LoopVariance.quadraticFactor_pos (s : ℝ) :

0 < quadraticFactor s

theorem NavierStokes.LoopVariance.quadraticFactor_even (s : ℝ) :

quadraticFactor (-s) = quadraticFactor s

noncomputable def NavierStokes.LoopVariance.signedRoot (s : ℝ) :

This signed square root is analytic even at the zero-variance point.

Equations

NavierStokes.LoopVariance.signedRoot s = s * √(NavierStokes.LoopVariance.quadraticFactor s)

Instances For

theorem NavierStokes.LoopVariance.signedRoot_contDiff :

ContDiff ℝ ⊤ signedRoot

theorem NavierStokes.LoopVariance.signedRoot_sq (s : ℝ) :

signedRoot s ^ 2 = baseVariance s

theorem NavierStokes.LoopVariance.signedRoot_zero :

signedRoot 0 = 0

theorem NavierStokes.LoopVariance.signedRoot_odd (s : ℝ) :

signedRoot (-s) = -signedRoot s

theorem NavierStokes.LoopVariance.signedRoot_hasDerivAt_zero :

HasDerivAt signedRoot (√(1 / 2)) 0

theorem NavierStokes.LoopVariance.normalizer_centered (s : ℝ) :

SmoothLoop.expNormalizer s = (∫ (θ : ℝ) in -Real.pi ..Real.pi , Real.exp (s * Real.cos θ)) / (2 * Real.pi)

noncomputable def NavierStokes.LoopVariance.gaussianMass :

Gaussian mass, given by ∫ x : ℝ, Real.exp (-(2 / Real.pi ^ 2) * x ^ 2).

Equations

NavierStokes.LoopVariance.gaussianMass = ∫ (x : ℝ), Real.exp (-(2 / Real.pi ^ 2) * x ^ 2)

Instances For

theorem NavierStokes.LoopVariance.gaussianCoefficient_pos :

0 < 2 / Real.pi ^ 2

theorem NavierStokes.LoopVariance.gaussianMass_pos :

0 < gaussianMass

theorem NavierStokes.LoopVariance.gaussian_scaled_integrable (t : ℝ) (ht : 0 < t) :

MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-(2 / Real.pi ^ 2) * (t * x) ^ 2)) MeasureTheory.volume

theorem NavierStokes.LoopVariance.gaussian_scaled_integral (t : ℝ) (ht : 0 < t) :

∫ (x : ℝ), Real.exp (-(2 / Real.pi ^ 2) * (t * x) ^ 2) = gaussianMass / t

theorem NavierStokes.LoopVariance.normalizer_square_upper (t : ℝ) (ht : 0 < t) :

SmoothLoop.expNormalizer (t ^ 2) ≤ Real.exp (t ^ 2) * gaussianMass / (2 * Real.pi * t)

The upper Laplace bound uses Jordan's quadratic cosine inequality and the ordinary Gaussian integral on the whole real line.

theorem NavierStokes.LoopVariance.normalizer_double_square_lower (t : ℝ) (ht : 1 ≤ t) :

2 * Real.exp (2 * t ^ 2 - 1) / (2 * Real.pi * t) ≤ SmoothLoop.expNormalizer (2 * t ^ 2)

A matching lower bound follows by integrating over [-1/t,1/t]. Only t≥1 is required, and every constant is explicit.

noncomputable def NavierStokes.LoopVariance.growthConstant :

Growth constant, given by 2 * (2 * Real.pi) * Real.exp (-1) / gaussianMass ^ 2.

Equations

NavierStokes.LoopVariance.growthConstant = 2 * (2 * Real.pi) * Real.exp (-1) / NavierStokes.LoopVariance.gaussianMass ^ 2

Instances For

theorem NavierStokes.LoopVariance.growthConstant_pos :

0 < growthConstant

theorem NavierStokes.LoopVariance.baseVariance_square_growth (t : ℝ) (ht : 1 ≤ t) :

growthConstant * t ≤ baseVariance (t ^ 2) + 1

theorem NavierStokes.LoopVariance.baseVariance_unbounded (B : ℝ) :

∃ (s : ℝ), 0 ≤ s ∧ B ≤ baseVariance s

theorem NavierStokes.LoopVariance.baseVariance_tendsto_atTop :

Filter.Tendsto baseVariance Filter.atTop Filter.atTop

theorem NavierStokes.LoopVariance.baseVariance_deriv_neg {s : ℝ} (hs : s < 0) :

deriv baseVariance s < 0

theorem NavierStokes.LoopVariance.signedRoot_deriv_pos (s : ℝ) :

0 < deriv signedRoot s

theorem NavierStokes.LoopVariance.signedRoot_strictMono :

StrictMono signedRoot

theorem NavierStokes.LoopVariance.signedRoot_surjective :

Function.Surjective signedRoot

noncomputable def NavierStokes.LoopVariance.rootHomeomorph :

Root homeomorph, given by (StrictMono.orderIsoOfSurjective signedRoot signedRoot_strictMono signedRoot_surjective).toHomeomorph.

Equations

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

Instances For

noncomputable def NavierStokes.LoopVariance.inverseRoot :

Inverse root, given by rootHomeomorph.symm.

Equations

NavierStokes.LoopVariance.inverseRoot = ⇑NavierStokes.LoopVariance.rootHomeomorph.symm

Instances For

theorem NavierStokes.LoopVariance.inverseRoot_right (s : ℝ) :

signedRoot (inverseRoot s) = s

theorem NavierStokes.LoopVariance.inverseRoot_left (s : ℝ) :

inverseRoot (signedRoot s) = s

theorem NavierStokes.LoopVariance.inverseRoot_contDiff :

ContDiff ℝ ⊤ inverseRoot

theorem NavierStokes.LoopVariance.inverseRoot_zero :

inverseRoot 0 = 0

theorem NavierStokes.LoopVariance.inverseRoot_odd (s : ℝ) :

inverseRoot (-s) = -inverseRoot s

theorem NavierStokes.LoopVariance.inverseRoot_deriv_zero :

deriv inverseRoot 0 = 1 / √(1 / 2)

noncomputable def NavierStokes.LoopVariance.inverseSlope :

An analytic divided difference of the actual inverse, which removes the apparent 1/p singularity in the parameter-dependent variance solve.

Equations

NavierStokes.LoopVariance.inverseSlope = dslope NavierStokes.LoopVariance.inverseRoot 0

Instances For

theorem NavierStokes.LoopVariance.inverseSlope_zero :

inverseSlope 0 = 1 / √(1 / 2)

theorem NavierStokes.LoopVariance.inverseSlope_identity (s : ℝ) :

s * inverseSlope s = inverseRoot s

theorem NavierStokes.LoopVariance.inverseSlope_analyticAt (s : ℝ) :

AnalyticAt ℝ inverseSlope s

theorem NavierStokes.LoopVariance.inverseSlope_contDiff :

ContDiff ℝ ⊤ inverseSlope

noncomputable def NavierStokes.LoopVariance.scaledRoot (d p μ : ℝ) :

Scaled root, given by d * μ * Real.sqrt (quadraticFactor (μ * p)).

Equations

NavierStokes.LoopVariance.scaledRoot d p μ = d * μ * √(NavierStokes.LoopVariance.quadraticFactor (μ * p))

Instances For

noncomputable def NavierStokes.LoopVariance.solveScale (d p r : ℝ) :

Solve scale, given by (r / d) * inverseSlope (p * (r / d)).

Equations

NavierStokes.LoopVariance.solveScale d p r = r / d * NavierStokes.LoopVariance.inverseSlope (p * (r / d))

Instances For

theorem NavierStokes.LoopVariance.solveScale_mul (d p r : ℝ) :

solveScale d p r * p = inverseRoot (p * (r / d))

theorem NavierStokes.LoopVariance.solveScale_spec (d p r : ℝ) (hd : d ≠ 0) :

scaledRoot d p (solveScale d p r) = r

theorem NavierStokes.LoopVariance.scaledRoot_hasDerivAt (d p μ : ℝ) :

HasDerivAt (scaledRoot d p) (d * deriv signedRoot (μ * p)) μ

theorem NavierStokes.LoopVariance.scaledRoot_strictMono (d p : ℝ) (hd : 0 < d) :

StrictMono (scaledRoot d p)

theorem NavierStokes.LoopVariance.scaledRoot_zero (d p : ℝ) :

scaledRoot d p 0 = 0

theorem NavierStokes.LoopVariance.solveScale_nonneg (d p r : ℝ) (hd : 0 < d) (hr : 0 ≤ r) :

0 ≤ solveScale d p r

theorem NavierStokes.LoopVariance.solveScale_unique (d p r μ : ℝ) (hd : 0 < d) (hμ : scaledRoot d p μ = r) :

μ = solveScale d p r

theorem NavierStokes.LoopVariance.solveScale_joint_contDiff (d : ℝ) :

ContDiff ℝ ⊤ fun (x : ℝ × ℝ) => solveScale d x.1 x.2

Smooth dependence on the prescribed signed square root of variance, including at p=0 and r=0.

theorem NavierStokes.LoopVariance.solveScale_smooth_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (d p r : E → ℝ) (hd : ContDiff ℝ (↑⊤) d) (hp : ContDiff ℝ (↑⊤) p) (hr : ContDiff ℝ (↑⊤) r) (hdne : ∀ (x : E), d x ≠ 0) :

ContDiff ℝ ↑⊤ fun (x : E) => solveScale (d x) (p x) (r x)

noncomputable def NavierStokes.LoopVariance.tiltVariance (d p μ : ℝ) :

The globally regular formula for the manuscript's scaled variance.

Equations

NavierStokes.LoopVariance.tiltVariance d p μ = d ^ 2 * μ ^ 2 * NavierStokes.LoopVariance.quadraticFactor (μ * p)

Instances For

theorem NavierStokes.LoopVariance.scaledRoot_sq (d p μ : ℝ) :

scaledRoot d p μ ^ 2 = tiltVariance d p μ

theorem NavierStokes.LoopVariance.tiltVariance_formula (d p μ : ℝ) (hp : p ≠ 0) :

tiltVariance d p μ = (d / p) ^ 2 * baseVariance (μ * p)

theorem NavierStokes.LoopVariance.tiltVariance_zero_parameter (d μ : ℝ) :

tiltVariance d 0 μ = d ^ 2 * μ ^ 2 / 2

theorem NavierStokes.LoopVariance.tiltVariance_zero_amplitude (d p : ℝ) :

tiltVariance d p 0 = 0

theorem NavierStokes.LoopVariance.solveScale_variance (d p r : ℝ) (hd : d ≠ 0) :

tiltVariance d p (solveScale d p r) = r ^ 2

theorem NavierStokes.LoopVariance.exists_unique_nonneg_variance_parameter (d p V : ℝ) (hd : 0 < d) (hV : 0 ≤ V) :

∃! μ : ℝ , 0 ≤ μ ∧ tiltVariance d p μ = V

theorem NavierStokes.LoopVariance.tiltVariance_strictMonoOn (d p : ℝ) (hd : 0 < d) :

StrictMonoOn (tiltVariance d p) (Set.Ici 0)

theorem NavierStokes.LoopVariance.tiltVariance_tendsto_atTop (d p : ℝ) (hd : 0 < d) :

Filter.Tendsto (tiltVariance d p) Filter.atTop Filter.atTop

theorem NavierStokes.LoopVariance.tiltVariance_eq_extended_integral (m d p μ : ℝ) :

tiltVariance d p μ = SmoothLoop.angularMean fun (θ : ℝ) => (SmoothLoop.extendedExpTilt m d μ p θ - m) ^ 2

theorem NavierStokes.LoopVariance.dslope_zero_analyticAt (f : ℝ → ℝ) (hf : ∀ (s : ℝ), AnalyticAt ℝ f s) (s : ℝ) :

AnalyticAt ℝ (dslope f 0) s

noncomputable def NavierStokes.LoopVariance.expDivided :

Exp divided, given by dslope Real.exp 0.

Equations

NavierStokes.LoopVariance.expDivided = dslope Real.exp 0

Instances For

noncomputable def NavierStokes.LoopVariance.normalizerDivided :

Normalizer divided, given by dslope expNormalizer 0.

Equations

NavierStokes.LoopVariance.normalizerDivided = dslope NavierStokes.SmoothLoop.expNormalizer 0

Instances For

theorem NavierStokes.LoopVariance.expDivided_contDiff :

ContDiff ℝ ⊤ expDivided

theorem NavierStokes.LoopVariance.normalizerDivided_contDiff :

ContDiff ℝ ⊤ normalizerDivided

theorem NavierStokes.LoopVariance.expDivided_zero :

expDivided 0 = 1

theorem NavierStokes.LoopVariance.normalizerDivided_zero :

normalizerDivided 0 = 0

noncomputable def NavierStokes.LoopVariance.regularizedDensitySlope (s θ : ℝ) :

Regularized density slope, given by (Real.cos θ * expDivided (s * Real.cos θ) - normalizerDivided s) / expNormalizer s.

Equations

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

Instances For

theorem NavierStokes.LoopVariance.regularizedDensitySlope_zero (θ : ℝ) :

regularizedDensitySlope 0 θ = Real.cos θ

theorem NavierStokes.LoopVariance.regularizedDensitySlope_identity (s θ : ℝ) :

s * regularizedDensitySlope s θ = SmoothLoop.normalizedExp s θ - 1

theorem NavierStokes.LoopVariance.regularizedDensitySlope_joint_contDiff :

ContDiff ℝ ⊤ fun (x : ℝ × ℝ) => regularizedDensitySlope x.1 x.2

noncomputable def NavierStokes.LoopVariance.regularizedTilt (m d μ p θ : ℝ) :

A formula with no transverse-stress denominator, equal to the manuscript's extended family for all parameters.

Equations

NavierStokes.LoopVariance.regularizedTilt m d μ p θ = m + d * μ * NavierStokes.LoopVariance.regularizedDensitySlope (μ * p) θ

Instances For

theorem NavierStokes.LoopVariance.regularizedTilt_eq_extended (m d μ p θ : ℝ) :

regularizedTilt m d μ p θ = SmoothLoop.extendedExpTilt m d μ p θ

theorem NavierStokes.LoopVariance.extendedExpTilt_smooth_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (m d μ p θ : E → ℝ) (hm : ContDiff ℝ (↑⊤) m) (hd : ContDiff ℝ (↑⊤) d) (hμ : ContDiff ℝ (↑⊤) μ) (hp : ContDiff ℝ (↑⊤) p) (hθ : ContDiff ℝ (↑⊤) θ) :

ContDiff ℝ ↑⊤ fun (x : E) => SmoothLoop.extendedExpTilt (m x) (d x) (μ x) (p x) (θ x)

noncomputable def NavierStokes.LoopVariance.solvedTilt (m d p r θ : ℝ) :

Solved tilt, given by extendedExpTilt m d (solveScale d p r) p θ.

Equations

NavierStokes.LoopVariance.solvedTilt m d p r θ = NavierStokes.SmoothLoop.extendedExpTilt m d (NavierStokes.LoopVariance.solveScale d p r) p θ

Instances For

theorem NavierStokes.LoopVariance.solvedTilt_periodic (m d p r : ℝ) :

Function.Periodic (solvedTilt m d p r) (2 * Real.pi)

theorem NavierStokes.LoopVariance.solvedTilt_mean (m d p r : ℝ) :

SmoothLoop.angularMean (solvedTilt m d p r) = m

theorem NavierStokes.LoopVariance.solvedTilt_variance (m d p r : ℝ) (hd : d ≠ 0) :

(SmoothLoop.angularMean fun (θ : ℝ) => (solvedTilt m d p r θ - m) ^ 2) = r ^ 2

theorem NavierStokes.LoopVariance.solvedTilt_projection (p₁ m d p r : ℝ) (hd : 0 < d) (hmargin : 2 ≤ p₁ + p * m - d) (θ : ℝ) :

2 < p₁ + p * solvedTilt m d p r θ

theorem NavierStokes.LoopVariance.solvedTilt_smooth_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (m d p r θ : E → ℝ) (hm : ContDiff ℝ (↑⊤) m) (hd : ContDiff ℝ (↑⊤) d) (hp : ContDiff ℝ (↑⊤) p) (hr : ContDiff ℝ (↑⊤) r) (hθ : ContDiff ℝ (↑⊤) θ) (hdne : ∀ (x : E), d x ≠ 0) :

ContDiff ℝ ↑⊤ fun (x : E) => solvedTilt (m x) (d x) (p x) (r x) (θ x)

The solved exponential tilt is jointly C∞ in smooth mean/stress data, angle, and prescribed signed square root of variance. This includes both the p=0 and r=0 loci.

theorem NavierStokes.LoopVariance.solvedTilt_contDiff (m d p r : ℝ) :

ContDiff ℝ (↑⊤) (solvedTilt m d p r)

theorem NavierStokes.LoopVariance.solvedTilt_zero_target (m d p θ : ℝ) :

solvedTilt m d p 0 θ = m

theorem NavierStokes.LoopVariance.exists_smooth_projected_tilt (p₁ p₂ m V : ℝ) (hP : 2 < p₁ + p₂ * m) (hV : 0 ≤ V) :

∃ (t : ℝ → ℝ), ContDiff ℝ (↑⊤) t ∧ Function.Periodic t (2 * Real.pi) ∧ SmoothLoop.angularMean t = m ∧ (SmoothLoop.angularMean fun (θ : ℝ) => (t θ - m) ^ 2) = V ∧ ∀ (θ : ℝ), 2 < p₁ + p₂ * t θ

The actual periodic analogue of LoopMoments.exists_projected_twoPoint: all prescribed nonnegative variances are realized, with no cosine-amplitude restriction.

theorem NavierStokes.LoopVariance.uniform_variance_amplitude {K : Set ℝ} (hK : IsCompact K) (d V : ℝ) (hd : 0 < d) (hV : 0 ≤ V) :

∃ (M : ℝ), 0 < M ∧ ∀ p ∈ K, V < tiltVariance d p M

Compact transverse-stress data have one amplitude that exceeds a prescribed variance target everywhere, as required before choosing the uniform cone margin in the manuscript.

noncomputable def NavierStokes.TrueConeLoop.lowSpeed (δ : ℝ) :

Low speed, given by 2 + δ / 8.

Equations

NavierStokes.TrueConeLoop.lowSpeed δ = 2 + δ / 8

Instances For

noncomputable def NavierStokes.TrueConeLoop.highSpeed (δ : ℝ) :

High speed, given by 2 + δ / 4.

Equations

NavierStokes.TrueConeLoop.highSpeed δ = 2 + δ / 4

Instances For

noncomputable def NavierStokes.TrueConeLoop.targetSpeed (δ : ℝ) :

Target speed, given by 2 + δ / 2.

Equations

NavierStokes.TrueConeLoop.targetSpeed δ = 2 + δ / 2

Instances For

noncomputable def NavierStokes.TrueConeLoop.speedCutoff (δ v : ℝ) :

Speed cutoff, given by 1 - Real.smoothTransition ((v - lowSpeed δ) / (δ / 8)).

Equations

NavierStokes.TrueConeLoop.speedCutoff δ v = 1 - ((v - NavierStokes.TrueConeLoop.lowSpeed δ) / (δ / 8)).smoothTransition

Instances For

theorem NavierStokes.TrueConeLoop.speedCutoff_contDiff (δ : ℝ) :

ContDiff ℝ (↑⊤) (speedCutoff δ)

theorem NavierStokes.TrueConeLoop.speedCutoff_mem_Icc (δ v : ℝ) :

speedCutoff δ v ∈ Set.Icc 0 1

theorem NavierStokes.TrueConeLoop.speedCutoff_one (δ v : ℝ) (hδ : 0 < δ) (hv : v ≤ lowSpeed δ) :

speedCutoff δ v = 1

theorem NavierStokes.TrueConeLoop.speedCutoff_zero (δ v : ℝ) (hδ : 0 < δ) (hv : highSpeed δ ≤ v) :

speedCutoff δ v = 0

noncomputable def NavierStokes.TrueConeLoop.correctionRoot (δ v : ℝ) :

Correction root, given by speedCutoff δ v * Real.sqrt (targetSpeed δ - v).

Equations

NavierStokes.TrueConeLoop.correctionRoot δ v = NavierStokes.TrueConeLoop.speedCutoff δ v * √(NavierStokes.TrueConeLoop.targetSpeed δ - v)

Instances For

noncomputable def NavierStokes.TrueConeLoop.correction (δ v : ℝ) :

Correction, given by correctionRoot δ v ^ 2.

Equations

NavierStokes.TrueConeLoop.correction δ v = NavierStokes.TrueConeLoop.correctionRoot δ v ^ 2

Instances For

noncomputable def NavierStokes.TrueConeLoop.correctedSpeed (δ v : ℝ) :

Corrected speed, given by v + correction δ v.

Equations

NavierStokes.TrueConeLoop.correctedSpeed δ v = v + NavierStokes.TrueConeLoop.correction δ v

Instances For

theorem NavierStokes.TrueConeLoop.correctionRoot_zero (δ v : ℝ) (hδ : 0 < δ) (hv : highSpeed δ ≤ v) :

correctionRoot δ v = 0

theorem NavierStokes.TrueConeLoop.correctionRoot_contDiff (δ : ℝ) (hδ : 0 < δ) :

ContDiff ℝ (↑⊤) (correctionRoot δ)

theorem NavierStokes.TrueConeLoop.correctionRoot_nonneg (δ v : ℝ) :

0 ≤ correctionRoot δ v

theorem NavierStokes.TrueConeLoop.correction_nonneg (δ v : ℝ) :

0 ≤ correction δ v

theorem NavierStokes.TrueConeLoop.correction_formula (δ v : ℝ) (hδ : 0 < δ) :

correction δ v = speedCutoff δ v ^ 2 * (targetSpeed δ - v)

theorem NavierStokes.TrueConeLoop.correction_zero (δ v : ℝ) (hδ : 0 < δ) (hv : highSpeed δ ≤ v) :

correction δ v = 0

theorem NavierStokes.TrueConeLoop.correction_le_gap (δ v : ℝ) (hδ : 0 < δ) (hv : v ≤ highSpeed δ) :

correction δ v ≤ targetSpeed δ - v

theorem NavierStokes.TrueConeLoop.correction_lt_three (δ v : ℝ) (hδ : 0 < δ) (hδ₁ : δ ≤ 1) (hv : 0 < v) :

correction δ v < 3

theorem NavierStokes.TrueConeLoop.correctedSpeed_gt_two (δ v : ℝ) (hδ : 0 < δ) :

2 < correctedSpeed δ v

theorem NavierStokes.TrueConeLoop.correctedSpeed_le_target_of_active (δ v : ℝ) (hδ : 0 < δ) (hactive : speedCutoff δ v ≠ 0) :

correctedSpeed δ v ≤ targetSpeed δ

noncomputable def NavierStokes.TrueConeLoop.varianceRoot (a δ v : ℝ) :

Variance root, given by correctionRoot δ v / Real.sqrt a.

Equations

NavierStokes.TrueConeLoop.varianceRoot a δ v = NavierStokes.TrueConeLoop.correctionRoot δ v / √a

Instances For

theorem NavierStokes.TrueConeLoop.varianceRoot_nonneg (a δ v : ℝ) :

0 ≤ varianceRoot a δ v

theorem NavierStokes.TrueConeLoop.varianceRoot_sq (a δ v : ℝ) (ha : 0 < a) :

varianceRoot a δ v ^ 2 = correction δ v / a

theorem NavierStokes.TrueConeLoop.varianceRoot_zero (a δ v : ℝ) (hδ : 0 < δ) (hv : highSpeed δ ≤ v) :

varianceRoot a δ v = 0

theorem NavierStokes.TrueConeLoop.varianceRoot_bound (amin a δ v : ℝ) (hmin : 0 < amin) (ha : amin ≤ a) (hδ : 0 < δ) (hδ₁ : δ ≤ 1) (hv : 0 < v) :

varianceRoot a δ v ≤ √(3 / amin)

theorem NavierStokes.TrueConeLoop.solvedTilt_fixed_joint_contDiff (d : ℝ) (hd : d ≠ 0) :

ContDiff ℝ ↑⊤ fun (z : (ℝ × ℝ) × ℝ × ℝ) => LoopVariance.solvedTilt z.1.1 d z.1.2 z.2.1 z.2.2

theorem NavierStokes.TrueConeLoop.solvedTilt_continuous_family {X : Type u_1} [TopologicalSpace X] (m p r θ : X → ℝ) (d : ℝ) (hd : d ≠ 0) (hm : Continuous m) (hp : Continuous p) (hr : Continuous r) (hθ : Continuous θ) :

Continuous fun (x : X) => LoopVariance.solvedTilt (m x) d (p x) (r x) (θ x)

theorem NavierStokes.TrueConeLoop.uniform_tilt_cone_margin {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (m p₁ p₂ : X → ℝ) (hm : Continuous m) (hp₁ : Continuous p₁) (hp₂ : Continuous p₂) (d R : ℝ) (hd : 0 < d) (hmargin : ∀ x ∈ K, 2 ≤ p₁ x + p₂ x * m x - d) :

∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ K, ∀ r ∈ Set.Icc 0 R, ∀ (θ : ℝ), 2 + ε ≤ ConeAlgebra.coneBound (p₁ x + p₂ x * LoopVariance.solvedTilt (m x) d (p₂ x) r θ) (p₂ x - p₁ x * LoopVariance.solvedTilt (m x) d (p₂ x) r θ)

def NavierStokes.TrueConeLoop.nominalSpeed (a m : ℝ) :

Nominal speed, given by a * (1 + m ^ 2).

Equations

NavierStokes.TrueConeLoop.nominalSpeed a m = a * (1 + m ^ 2)

Instances For

noncomputable def NavierStokes.TrueConeLoop.seedRho (a m δ : ℝ) :

Seed rho, given by correction δ (nominalSpeed a m).

Equations

NavierStokes.TrueConeLoop.seedRho a m δ = NavierStokes.TrueConeLoop.correction δ (NavierStokes.TrueConeLoop.nominalSpeed a m)

Instances For

noncomputable def NavierStokes.TrueConeLoop.seedSpeed (a m δ : ℝ) :

Seed speed, given by correctedSpeed δ (nominalSpeed a m).

Equations

NavierStokes.TrueConeLoop.seedSpeed a m δ = NavierStokes.TrueConeLoop.correctedSpeed δ (NavierStokes.TrueConeLoop.nominalSpeed a m)

Instances For

noncomputable def NavierStokes.TrueConeLoop.seedTilt (a m d p δ θ : ℝ) :

Seed tilt, given by solvedTilt m d p (varianceRoot a δ (nominalSpeed a m)) θ.

Equations

NavierStokes.TrueConeLoop.seedTilt a m d p δ θ = NavierStokes.LoopVariance.solvedTilt m d p (NavierStokes.TrueConeLoop.varianceRoot a δ (NavierStokes.TrueConeLoop.nominalSpeed a m)) θ

Instances For

theorem NavierStokes.TrueConeLoop.seedSpeed_gt_two (a m δ : ℝ) (hδ : 0 < δ) :

2 < seedSpeed a m δ

theorem NavierStokes.TrueConeLoop.seedTilt_contDiff (a m d p δ : ℝ) :

ContDiff ℝ (↑⊤) (seedTilt a m d p δ)

theorem NavierStokes.TrueConeLoop.seedTilt_periodic (a m d p δ : ℝ) :

Function.Periodic (seedTilt a m d p δ) (2 * Real.pi)

theorem NavierStokes.TrueConeLoop.seedTilt_mean (a m d p δ : ℝ) :

SmoothLoop.angularMean (seedTilt a m d p δ) = m

theorem NavierStokes.TrueConeLoop.seedTilt_variance (a m d p δ : ℝ) (ha : 0 < a) (hd : d ≠ 0) :

(SmoothLoop.angularMean fun (θ : ℝ) => (seedTilt a m d p δ θ - m) ^ 2) = seedRho a m δ / a

theorem NavierStokes.TrueConeLoop.seedTilt_nominal_of_inactive (a m d p δ : ℝ) (hzero : speedCutoff δ (nominalSpeed a m) = 0) :

seedTilt a m d p δ = fun (x : ℝ) => m

theorem NavierStokes.TrueConeLoop.seedSpeed_nominal_of_inactive (a m δ : ℝ) (hzero : speedCutoff δ (nominalSpeed a m) = 0) :

seedSpeed a m δ = nominalSpeed a m

theorem NavierStokes.TrueConeLoop.seedTilt_nominal (a m d p δ : ℝ) (hδ : 0 < δ) (hh : highSpeed δ ≤ nominalSpeed a m) :

seedTilt a m d p δ = fun (x : ℝ) => m

theorem NavierStokes.TrueConeLoop.seed_cone (a m p₁ p₂ d δ R : ℝ) (ha : 0 < a) (hd : 0 < d) (hδ : 0 < δ) (hδ₁ : δ ≤ 1) (hR : √(3 / a) ≤ R) (hmargin : 2 ≤ p₁ + p₂ * m - d) (hrelaxed : nominalSpeed a m < ConeAlgebra.coneBound (p₁ + p₂ * m) (p₂ - p₁ * m)) (hU : ∀ r ∈ Set.Icc 0 R, ∀ (θ : ℝ), 2 + δ ≤ ConeAlgebra.coneBound (p₁ + p₂ * LoopVariance.solvedTilt m d p₂ r θ) (p₂ - p₁ * LoopVariance.solvedTilt m d p₂ r θ)) (θ : ℝ) :

2 < p₁ + p₂ * seedTilt a m d p₂ δ θ ∧ seedSpeed a m δ < ConeAlgebra.coneBound (p₁ + p₂ * seedTilt a m d p₂ δ θ) (p₂ - p₁ * seedTilt a m d p₂ δ θ)

noncomputable def NavierStokes.TrueConeLoop.seedDensity (a m d p δ : ℝ) (ha : 0 < a) (hd : d ≠ 0) (hδ : 0 < δ) :

SmoothLoop.CircleDensity

Seed density, constructed using densityOfTilt.

Equations

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

Instances For

noncomputable def NavierStokes.TrueConeLoop.constructedA (a m d p δ : ℝ) (ha : 0 < a) (hd : d ≠ 0) (hδ : 0 < δ) :

Constructed A, given by rephase (seedDensity a m d p δ ha hd hδ) (fun θ => loopA (seedSpeed a m δ) (seedTilt a m d p δ θ)).

Equations

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

Instances For

noncomputable def NavierStokes.TrueConeLoop.constructedC (a m d p δ : ℝ) (ha : 0 < a) (hd : d ≠ 0) (hδ : 0 < δ) :

Constructed C, given by rephase (seedDensity a m d p δ ha hd hδ) (fun θ => loopC (seedSpeed a m δ) (seedTilt a m d p δ θ)).

Equations

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

Instances For

def NavierStokes.TrueConeLoop.InTrueCone (p₁ p₂ A C : ℝ) :

In true cone, constructed using 0.

Equations

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

Instances For

def NavierStokes.TrueConeLoop.HasConeMargin (ε p₁ p₂ A C : ℝ) :

Positive additive margins for all four scalar inequalities, including the positive first shear component.

Equations

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

Instances For

theorem NavierStokes.TrueConeLoop.compact_periodic_trueCone_margins {X : Type u_1} [TopologicalSpace X] (p₁ p₂ : X → ℝ) (A C : X × ℝ → ℝ) {K : Set X} (hK : IsCompact K) (hp₁ : ContinuousOn p₁ K) (hp₂ : ContinuousOn p₂ K) (hA : ContinuousOn A (K ×ˢ Set.univ)) (hC : ContinuousOn C (K ×ˢ Set.univ)) (hAp : ∀ x ∈ K, Function.Periodic (fun (φ : ℝ) => A (x, φ)) 1) (hCp : ∀ x ∈ K, Function.Periodic (fun (φ : ℝ) => C (x, φ)) 1) (hcone : ∀ x ∈ K, ∀ (φ : ℝ), InTrueCone (p₁ x) (p₂ x) (A (x, φ)) (C (x, φ))) :

∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ K, ∀ (φ : ℝ), HasConeMargin ε (p₁ x) (p₂ x) (A (x, φ)) (C (x, φ))

Compact slow parameters and a periodic fast parameter turn strict pointwise cone inequalities into one positive margin at every fast angle.

theorem NavierStokes.TrueConeLoop.constructed_smooth (a m d p δ : ℝ) (ha : 0 < a) (hd : d ≠ 0) (hδ : 0 < δ) :

ContDiff ℝ (↑⊤) (constructedA a m d p δ ha hd hδ) ∧ ContDiff ℝ (↑⊤) (constructedC a m d p δ ha hd hδ)

theorem NavierStokes.TrueConeLoop.constructed_periodic (a m d p δ : ℝ) (ha : 0 < a) (hd : d ≠ 0) (hδ : 0 < δ) :

Function.Periodic (constructedA a m d p δ ha hd hδ) 1 ∧ Function.Periodic (constructedC a m d p δ ha hd hδ) 1

theorem NavierStokes.TrueConeLoop.constructed_means (a m d p δ : ℝ) (ha : 0 < a) (hd : d ≠ 0) (hδ : 0 < δ) :

∫ (φ : ℝ) in 0..1, constructedA a m d p δ ha hd hδ φ = a ∧ ∫ (φ : ℝ) in 0..1, constructedC a m d p δ ha hd hδ φ = a * m

theorem NavierStokes.TrueConeLoop.constructed_trueCone (a m p₁ p₂ d δ R : ℝ) (ha : 0 < a) (hd : 0 < d) (hδ : 0 < δ) (hδ₁ : δ ≤ 1) (hR : √(3 / a) ≤ R) (hmargin : 2 ≤ p₁ + p₂ * m - d) (hrelaxed : nominalSpeed a m < ConeAlgebra.coneBound (p₁ + p₂ * m) (p₂ - p₁ * m)) (hU : ∀ r ∈ Set.Icc 0 R, ∀ (θ : ℝ), 2 + δ ≤ ConeAlgebra.coneBound (p₁ + p₂ * LoopVariance.solvedTilt m d p₂ r θ) (p₂ - p₁ * LoopVariance.solvedTilt m d p₂ r θ)) (φ : ℝ) :

InTrueCone p₁ p₂ (constructedA a m d p₂ δ ha ⋯ hδ φ) (constructedC a m d p₂ δ ha ⋯ hδ φ)

theorem NavierStokes.TrueConeLoop.constructed_nominal (a m d p δ : ℝ) (ha : 0 < a) (hd : d ≠ 0) (hδ : 0 < δ) (hh : highSpeed δ ≤ nominalSpeed a m) :

(constructedA a m d p δ ha hd hδ = fun (x : ℝ) => a) ∧ constructedC a m d p δ ha hd hδ = fun (x : ℝ) => a * m

theorem NavierStokes.TrueConeLoop.exists_trueCone_loop (a m p₁ p₂ : ℝ) (ha : 0 < a) (hP : 2 < p₁ + p₂ * m) (hrelaxed : nominalSpeed a m < ConeAlgebra.coneBound (p₁ + p₂ * m) (p₂ - p₁ * m)) :

∃ (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 ∧ ∀ (φ : ℝ), InTrueCone p₁ p₂ (A φ) (C φ)

Fixed-parameter true-cone realization, with no assumed loop or margin. The nominal data need only satisfy the relaxed cone.

structure NavierStokes.TrueConeLoop.FamilyChoices {X : Type u_1} (a m p₁ p₂ : X → ℝ) (K B : Set X) :

Family choices data, collecting aMin, d, radius, maxAmplitude, delta, aMin_pos and their compatibility conditions.

aMin : ℝ
A min of FamilyChoices, of type ℝ.
d : ℝ
D of FamilyChoices, of type ℝ.
radius : ℝ
Radius of FamilyChoices, of type ℝ.
maxAmplitude : ℝ
Max amplitude of FamilyChoices, of type ℝ.
delta : ℝ
Delta of FamilyChoices, of type ℝ.
aMin_pos : 0 < self.aMin
d_pos : 0 < self.d
radius_eq : self.radius = √(3 / self.aMin)
maxAmplitude_pos : 0 < self.maxAmplitude
delta_pos : 0 < self.delta
delta_le_one : self.delta ≤ 1
aMin_le (x : X) : x ∈ K → self.aMin ≤ a x
projection_margin (x : X) : x ∈ K → 2 ≤ p₁ x + p₂ x * m x - self.d
amplitude_large (x : X) : x ∈ K → 3 / self.aMin < LoopVariance.tiltVariance self.d (p₂ x) self.maxAmplitude
cone_margin (x : X) : x ∈ K → ∀ r ∈ Set.Icc 0 self.radius, ∀ (θ : ℝ), 2 + self.delta ≤ ConeAlgebra.coneBound (p₁ x + p₂ x * LoopVariance.solvedTilt (m x) self.d (p₂ x) r θ) (p₂ x - p₁ x * LoopVariance.solvedTilt (m x) self.d (p₂ x) r θ)
boundary_inactive (x : X) : x ∈ B → highSpeed self.delta < nominalSpeed (a x) (m x)

Instances For

theorem NavierStokes.TrueConeLoop.exists_family_choices {X : Type u_1} [TopologicalSpace X] (a m p₁ p₂ : X → ℝ) {K B : Set X} (hK : IsCompact K) (hB : IsCompact B) (ha : Continuous a) (hm : Continuous m) (hp₁ : Continuous p₁) (hp₂ : Continuous p₂) (haK : ∀ x ∈ K, 0 < a x) (hPK : ∀ x ∈ K, 2 < p₁ x + p₂ x * m x) (htrueB : ∀ x ∈ B, 2 < nominalSpeed (a x) (m x)) :

Nonempty (FamilyChoices a m p₁ p₂ K B)

theorem NavierStokes.TrueConeLoop.FamilyChoices.root_bound {X : Type u_1} {a m p₁ p₂ : X → ℝ} {K B : Set X} (c : FamilyChoices a m p₁ p₂ K B) {x : X} (hx : x ∈ K) :

varianceRoot (a x) c.delta (nominalSpeed (a x) (m x)) ∈ Set.Icc 0 c.radius

theorem NavierStokes.TrueConeLoop.FamilyChoices.amplitude_bound {X : Type u_1} {a m p₁ p₂ : X → ℝ} {K B : Set X} (c : FamilyChoices a m p₁ p₂ K B) {x : X} (hx : x ∈ K) :

0 ≤ LoopVariance.solveScale c.d (p₂ x) (varianceRoot (a x) c.delta (nominalSpeed (a x) (m x))) ∧ LoopVariance.solveScale c.d (p₂ x) (varianceRoot (a x) c.delta (nominalSpeed (a x) (m x))) < c.maxAmplitude

theorem NavierStokes.TrueConeLoop.nominalSpeed_family_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a m : E → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) :

ContDiff ℝ ↑⊤ fun (x : E) => nominalSpeed (a x) (m x)

theorem NavierStokes.TrueConeLoop.seedSpeed_family_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a m : E → ℝ) (δ : ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hδ : 0 < δ) :

ContDiff ℝ ↑⊤ fun (x : E) => seedSpeed (a x) (m x) δ

theorem NavierStokes.TrueConeLoop.seedTilt_family_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a m p : E → ℝ) (d δ : ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp : ContDiff ℝ (↑⊤) p) (hd : d ≠ 0) (hδ : 0 < δ) :

ContDiffOn ℝ (↑⊤) (fun (z : E × ℝ) => seedTilt (a z.1) (m z.1) d (p z.1) δ z.2) ({x : E | 0 < a x} ×ˢ Set.univ)

noncomputable def NavierStokes.TrueConeLoop.constantDensity :

SmoothLoop.CircleDensity

Constant density, bundling rate, smooth, positive, periodic and the required compatibility proofs.

Equations

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

Instances For

noncomputable def NavierStokes.TrueConeLoop.familyDensity {E : Type u_1} (a m p : E → ℝ) (d δ : ℝ) (hd : d ≠ 0) (hδ : 0 < δ) :

E → SmoothLoop.CircleDensity

Family density, defined pointwise by if hx : 0 < a x then seedDensity (a x) (m x) d (p x) δ hx hd hδ else constantDensity.

Equations

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

Instances For

theorem NavierStokes.TrueConeLoop.familyDensity_eq {E : Type u_1} (a m p : E → ℝ) (d δ : ℝ) (hd : d ≠ 0) (hδ : 0 < δ) (x : E) (hx : 0 < a x) :

familyDensity a m p d δ hd hδ x = seedDensity (a x) (m x) d (p x) δ hx hd hδ

theorem NavierStokes.TrueConeLoop.familyDensity_rate_eq {E : Type u_1} (a m p : E → ℝ) (d δ : ℝ) (hd : d ≠ 0) (hδ : 0 < δ) (x : E) (hx : 0 < a x) (θ : ℝ) :

(familyDensity a m p d δ hd hδ x).rate θ = LoopMoments.phaseDensity (a x) (seedSpeed (a x) (m x) δ) (seedTilt (a x) (m x) d (p x) δ θ) / (2 * Real.pi)

theorem NavierStokes.TrueConeLoop.familyDensity_rate_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a m p : E → ℝ) (d δ : ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp : ContDiff ℝ (↑⊤) p) (hd : d ≠ 0) (hδ : 0 < δ) :

ContDiffOn ℝ (↑⊤) (fun (z : E × ℝ) => (familyDensity a m p d δ hd hδ z.1).rate z.2) ({x : E | 0 < a x} ×ˢ Set.univ)

noncomputable def NavierStokes.TrueConeLoop.unphasedA {E : Type u_1} (a m p : E → ℝ) (d δ : ℝ) (z : E × ℝ) :

Unphased A, given by loopA (seedSpeed (a z.1) (m z.1) δ) (seedTilt (a z.1) (m z.1) d (p z.1) δ z.2).

Equations

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

Instances For

noncomputable def NavierStokes.TrueConeLoop.unphasedC {E : Type u_1} (a m p : E → ℝ) (d δ : ℝ) (z : E × ℝ) :

Unphased C, given by loopC (seedSpeed (a z.1) (m z.1) δ) (seedTilt (a z.1) (m z.1) d (p z.1) δ z.2).

Equations

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

Instances For

theorem NavierStokes.TrueConeLoop.unphased_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a m p : E → ℝ) (d δ : ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp : ContDiff ℝ (↑⊤) p) (hd : d ≠ 0) (hδ : 0 < δ) :

ContDiffOn ℝ (↑⊤) (unphasedA a m p d δ) ({x : E | 0 < a x} ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) (unphasedC a m p d δ) ({x : E | 0 < a x} ×ˢ Set.univ)

noncomputable def NavierStokes.TrueConeLoop.familyA {E : Type u_1} (a m p : E → ℝ) (d δ : ℝ) (hd : d ≠ 0) (hδ : 0 < δ) (z : E × ℝ) :

Family A, given by rephase (familyDensity a m p d δ hd hδ z.1) (fun θ => unphasedA a m p d δ (z.1, θ)) z.2.

Equations

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

Instances For

noncomputable def NavierStokes.TrueConeLoop.familyC {E : Type u_1} (a m p : E → ℝ) (d δ : ℝ) (hd : d ≠ 0) (hδ : 0 < δ) (z : E × ℝ) :

Family C, given by rephase (familyDensity a m p d δ hd hδ z.1) (fun θ => unphasedC a m p d δ (z.1, θ)) z.2.

Equations

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

Instances For

theorem NavierStokes.TrueConeLoop.familyA_eq_constructed {E : Type u_1} (a m p : E → ℝ) (d δ : ℝ) (hd : d ≠ 0) (hδ : 0 < δ) (x : E) (hx : 0 < a x) :

(fun (φ : ℝ) => familyA a m p d δ hd hδ (x, φ)) = constructedA (a x) (m x) d (p x) δ hx hd hδ

theorem NavierStokes.TrueConeLoop.familyC_eq_constructed {E : Type u_1} (a m p : E → ℝ) (d δ : ℝ) (hd : d ≠ 0) (hδ : 0 < δ) (x : E) (hx : 0 < a x) :

(fun (φ : ℝ) => familyC a m p d δ hd hδ (x, φ)) = constructedC (a x) (m x) d (p x) δ hx hd hδ

theorem NavierStokes.TrueConeLoop.family_pointwise_properties {E : Type u_1} (a m p₁ p₂ : E → ℝ) {K B : Set E} (c : FamilyChoices a m p₁ p₂ K B) (hrelaxed : ∀ x ∈ K, nominalSpeed (a x) (m x) < ConeAlgebra.coneBound (p₁ x + p₂ x * m x) (p₂ x - p₁ x * m x)) (x : E) :

x ∈ K → Function.Periodic (fun (φ : ℝ) => familyA a m p₂ c.d c.delta ⋯ ⋯ (x, φ)) 1 ∧ Function.Periodic (fun (φ : ℝ) => familyC a m p₂ c.d c.delta ⋯ ⋯ (x, φ)) 1 ∧ ∫ (φ : ℝ) in 0..1, familyA a m p₂ c.d c.delta ⋯ ⋯ (x, φ) = a x ∧ ∫ (φ : ℝ) in 0..1, familyC a m p₂ c.d c.delta ⋯ ⋯ (x, φ) = a x * m x ∧ ∀ (φ : ℝ), InTrueCone (p₁ x) (p₂ x) (familyA a m p₂ c.d c.delta ⋯ ⋯ (x, φ)) (familyC a m p₂ c.d c.delta ⋯ ⋯ (x, φ))

theorem NavierStokes.TrueConeLoop.family_nominal_neighborhood {E : Type u_1} [NormedAddCommGroup E] (a m p₁ p₂ : E → ℝ) {K B : Set E} (c : FamilyChoices a m p₁ p₂ K B) (ha : Continuous a) (hm : Continuous m) (hBK : B ⊆ K) :

∃ (N : Set E), IsOpen N ∧ B ⊆ N ∧ N ⊆ {x : E | 0 < a x} ∧ ∀ x ∈ N, ∀ (φ : ℝ), familyA a m p₂ c.d c.delta ⋯ ⋯ (x, φ) = a x ∧ familyC a m p₂ c.d c.delta ⋯ ⋯ (x, φ) = a x * m x

theorem NavierStokes.TrueConeLoop.family_joint_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (a m p : E → ℝ) (d δ : ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp : ContDiff ℝ (↑⊤) p) (hd : d ≠ 0) (hδ : 0 < δ) :

ContDiffOn ℝ (↑⊤) (familyA a m p d δ hd hδ) ({x : E | 0 < a x} ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) (familyC a m p d δ hd hδ) ({x : E | 0 < a x} ×ˢ Set.univ)

theorem NavierStokes.TrueConeLoop.exists_compact_trueCone_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (a m p₁ p₂ : E → ℝ) {K B : Set E} (hK : IsCompact K) (hB : IsCompact B) (hBK : B ⊆ K) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₁ : ContDiff ℝ (↑⊤) p₁) (hp₂ : ContDiff ℝ (↑⊤) p₂) (haK : ∀ x ∈ K, 0 < a x) (hPK : ∀ x ∈ K, 2 < p₁ x + p₂ x * m x) (hrelaxed : ∀ x ∈ K, nominalSpeed (a x) (m x) < ConeAlgebra.coneBound (p₁ x + p₂ x * m x) (p₂ x - p₁ x * m x)) (htrueB : ∀ x ∈ B, 2 < nominalSpeed (a x) (m x)) :

∃ (U : Set E) (N : Set E) (A : E × ℝ → ℝ) (C : E × ℝ → ℝ), IsOpen U ∧ K ⊆ U ∧ IsOpen N ∧ B ⊆ N ∧ N ⊆ U ∧ ContDiffOn ℝ (↑⊤) A (U ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) C (U ×ˢ Set.univ) ∧ (∀ x ∈ K, Function.Periodic (fun (φ : ℝ) => A (x, φ)) 1 ∧ Function.Periodic (fun (φ : ℝ) => C (x, φ)) 1 ∧ ∫ (φ : ℝ) in 0..1, A (x, φ) = a x ∧ ∫ (φ : ℝ) in 0..1, C (x, φ) = a x * m x ∧ ∀ (φ : ℝ), InTrueCone (p₁ x) (p₂ x) (A (x, φ)) (C (x, φ))) ∧ ∀ x ∈ N, ∀ (φ : ℝ), A (x, φ) = a x ∧ C (x, φ) = a x * m x

Full compact-family true-cone realization. The set B can be the two interval boundary faces (including any compact auxiliary parameter set). The output agrees exactly with the nominal shear on an open neighborhood of B, and is jointly C∞ in slow parameters and periodic angle.

theorem NavierStokes.TrueConeLoop.exists_compact_trueCone_family_with_margin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (a m p₁ p₂ : E → ℝ) {K B : Set E} (hK : IsCompact K) (hB : IsCompact B) (hBK : B ⊆ K) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₁ : ContDiff ℝ (↑⊤) p₁) (hp₂ : ContDiff ℝ (↑⊤) p₂) (haK : ∀ x ∈ K, 0 < a x) (hPK : ∀ x ∈ K, 2 < p₁ x + p₂ x * m x) (hrelaxed : ∀ x ∈ K, nominalSpeed (a x) (m x) < ConeAlgebra.coneBound (p₁ x + p₂ x * m x) (p₂ x - p₁ x * m x)) (htrueB : ∀ x ∈ B, 2 < nominalSpeed (a x) (m x)) :

∃ (ε : ℝ) (U : Set E) (N : Set E) (A : E × ℝ → ℝ) (C : E × ℝ → ℝ), 0 < ε ∧ IsOpen U ∧ K ⊆ U ∧ IsOpen N ∧ B ⊆ N ∧ N ⊆ U ∧ ContDiffOn ℝ (↑⊤) A (U ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) C (U ×ˢ Set.univ) ∧ (∀ x ∈ K, Function.Periodic (fun (φ : ℝ) => A (x, φ)) 1 ∧ Function.Periodic (fun (φ : ℝ) => C (x, φ)) 1 ∧ ∫ (φ : ℝ) in 0..1, A (x, φ) = a x ∧ ∫ (φ : ℝ) in 0..1, C (x, φ) = a x * m x ∧ ∀ (φ : ℝ), InTrueCone (p₁ x) (p₂ x) (A (x, φ)) (C (x, φ)) ∧ HasConeMargin ε (p₁ x) (p₂ x) (A (x, φ)) (C (x, φ))) ∧ ∀ x ∈ N, ∀ (φ : ℝ), A (x, φ) = a x ∧ C (x, φ) = a x * m x

The complete family theorem with one strictly positive margin valid for every slow parameter in K and every fast angle.

Rapid radial modulation #

Concrete chain rules, shear identities, and estimates for the modulation in Proposition 6.2. Frequencies are positive real numbers; hence the results apply in particular to positive integer frequencies. All derivatives are genuine deriv/fderiv derivatives, rather than formal differential symbols.

@[reducible, inline]

abbrev NavierStokes.RadialModulation.PhasePoint :

Phase point: an abbreviation for ℝ × ℝ × ℝ.

Equations

NavierStokes.RadialModulation.PhasePoint = (ℝ × ℝ × ℝ)

Instances For

@[reducible, inline]

abbrev NavierStokes.RadialModulation.BaseProfile :

Base profile: an abbreviation for ℝ → ℝ → ℝ.

Equations

NavierStokes.RadialModulation.BaseProfile = (ℝ → ℝ → ℝ)

Instances For

@[reducible, inline]

abbrev NavierStokes.RadialModulation.PrimitiveProfile :

Primitive profile: an abbreviation for PhasePoint → ℝ.

Equations

NavierStokes.RadialModulation.PrimitiveProfile = (NavierStokes.RadialModulation.PhasePoint → ℝ)

Instances For

noncomputable def NavierStokes.RadialModulation.phasePoint (n X η : ℝ) :

Phase point, given by (X, η, n * Real.log X).

Equations

NavierStokes.RadialModulation.phasePoint n X η = (X, η, n * Real.log X)

Instances For

noncomputable def NavierStokes.RadialModulation.partialX (A : PrimitiveProfile) (z : PhasePoint) :

Partial X, given by fderiv ℝ A z (1, 0, 0).

Equations

NavierStokes.RadialModulation.partialX A z = (fderiv ℝ A z) (1, 0, 0)

Instances For

noncomputable def NavierStokes.RadialModulation.partialEta (A : PrimitiveProfile) (z : PhasePoint) :

Partial eta, given by fderiv ℝ A z (0, 1, 0).

Equations

NavierStokes.RadialModulation.partialEta A z = (fderiv ℝ A z) (0, 1, 0)

Instances For

noncomputable def NavierStokes.RadialModulation.partialTheta (A : PrimitiveProfile) (z : PhasePoint) :

Partial theta, given by fderiv ℝ A z (0, 0, 1).

Equations

NavierStokes.RadialModulation.partialTheta A z = (fderiv ℝ A z) (0, 0, 1)

Instances For

noncomputable def NavierStokes.RadialModulation.modulatedE (n : ℝ) (E : BaseProfile) (A : PrimitiveProfile) (X η : ℝ) :

Modulated E, given by E X η * Real.exp (A (phasePoint n X η) / n).

Equations

NavierStokes.RadialModulation.modulatedE n E A X η = E X η * Real.exp (A (NavierStokes.RadialModulation.phasePoint n X η) / n)

Instances For

noncomputable def NavierStokes.RadialModulation.modulatedU (n : ℝ) (U : BaseProfile) (B : PrimitiveProfile) (X η : ℝ) :

Modulated U, given by U X η + B (phasePoint n X η) / n.

Equations

NavierStokes.RadialModulation.modulatedU n U B X η = U X η + B (NavierStokes.RadialModulation.phasePoint n X η) / n

Instances For

theorem NavierStokes.RadialModulation.modulatedE_contDiffAt (E : BaseProfile) (A : PrimitiveProfile) (n X η : ℝ) (hE : ContDiff ℝ (↑⊤) (Function.uncurry E)) (hA : ContDiff ℝ (↑⊤) A) (hX : X ≠ 0) :

ContDiffAt ℝ (↑⊤) (Function.uncurry (modulatedE n E A)) (X, η)

The logarithmic graph and modulated angular profile are genuinely smooth at every positive radius (indeed at every nonzero radius).

theorem NavierStokes.RadialModulation.modulatedU_contDiffAt (U : BaseProfile) (B : PrimitiveProfile) (n X η : ℝ) (hU : ContDiff ℝ (↑⊤) (Function.uncurry U)) (hB : ContDiff ℝ (↑⊤) B) (hX : X ≠ 0) :

ContDiffAt ℝ (↑⊤) (Function.uncurry (modulatedU n U B)) (X, η)

theorem NavierStokes.RadialModulation.phase_hasDerivAt_X (A : PrimitiveProfile) (n X η : ℝ) (hX : X ≠ 0) (hA : DifferentiableAt ℝ A (phasePoint n X η)) :

HasDerivAt (fun (r : ℝ) => A (phasePoint n r η)) (partialX A (phasePoint n X η) + n / X * partialTheta A (phasePoint n X η)) X

The rapid radial phase contributes exactly (n/X) A_θ.

theorem NavierStokes.RadialModulation.phase_hasDerivAt_eta (A : PrimitiveProfile) (n X η : ℝ) (hA : DifferentiableAt ℝ A (phasePoint n X η)) :

HasDerivAt (fun (e : ℝ) => A (phasePoint n X e)) (partialEta A (phasePoint n X η)) η

The rapid phase is independent of η, so no frequency enters this derivative.

theorem NavierStokes.RadialModulation.modulatedE_hasDerivAt_X (E : BaseProfile) (A : PrimitiveProfile) (n X η : ℝ) (hn : n ≠ 0) (hX : X ≠ 0) (hE : DifferentiableAt ℝ (fun (r : ℝ) => E r η) X) (hA : DifferentiableAt ℝ A (phasePoint n X η)) :

HasDerivAt (fun (r : ℝ) => modulatedE n E A r η) (Real.exp (A (phasePoint n X η) / n) * (deriv (fun (r : ℝ) => E r η) X + E X η * (partialX A (phasePoint n X η) / n + partialTheta A (phasePoint n X η) / X))) X

Exact radial derivative of the multiplicative angular modulation.

theorem NavierStokes.RadialModulation.modulatedU_hasDerivAt_X (U : BaseProfile) (B : PrimitiveProfile) (n X η : ℝ) (hn : n ≠ 0) (hX : X ≠ 0) (hU : DifferentiableAt ℝ (fun (r : ℝ) => U r η) X) (hB : DifferentiableAt ℝ B (phasePoint n X η)) :

HasDerivAt (fun (r : ℝ) => modulatedU n U B r η) (deriv (fun (r : ℝ) => U r η) X + partialX B (phasePoint n X η) / n + partialTheta B (phasePoint n X η) / X) X

Exact radial derivative of the additive axial modulation.

theorem NavierStokes.RadialModulation.modulatedE_hasDerivAt_eta (E : BaseProfile) (A : PrimitiveProfile) (n X η : ℝ) (hE : DifferentiableAt ℝ (E X) η) (hA : DifferentiableAt ℝ A (phasePoint n X η)) :

HasDerivAt (modulatedE n E A X) (deriv (E X) η * Real.exp (A (phasePoint n X η) / n) + E X η * (Real.exp (A (phasePoint n X η) / n) * (partialEta A (phasePoint n X η) / n))) η

theorem NavierStokes.RadialModulation.modulatedU_hasDerivAt_eta (U : BaseProfile) (B : PrimitiveProfile) (n X η : ℝ) (hU : DifferentiableAt ℝ (U X) η) (hB : DifferentiableAt ℝ B (phasePoint n X η)) :

HasDerivAt (modulatedU n U B X) (deriv (U X) η + partialEta B (phasePoint n X η) / n) η

theorem NavierStokes.RadialModulation.angular_shear_exact (E : BaseProfile) (A : PrimitiveProfile) (n X η aL : ℝ) (hn : n ≠ 0) (hX : X ≠ 0) (hE0 : E X η ≠ 0) (hE : DifferentiableAt ℝ (fun (r : ℝ) => E r η) X) (hA : DifferentiableAt ℝ A (phasePoint n X η)) (hprescribed : partialTheta A (phasePoint n X η) = -(aL - (1 - 2 * X * deriv (fun (r : ℝ) => E r η) X / E X η)) / 2) :

1 - 2 * X * deriv (fun (r : ℝ) => modulatedE n E A r η) X / modulatedE n E A X η = aL - 2 * X * partialX A (phasePoint n X η) / n

Exact angular shear: the only error after the primitive prescription is the slow radial derivative of A, divided by frequency.

theorem NavierStokes.RadialModulation.axial_shear_exact (E U : BaseProfile) (A B : PrimitiveProfile) (n X η bL : ℝ) (hn : n ≠ 0) (hX : X ≠ 0) (hE0 : E X η ≠ 0) (hU : DifferentiableAt ℝ (fun (r : ℝ) => U r η) X) (hB : DifferentiableAt ℝ B (phasePoint n X η)) (hprescribed : partialTheta B (phasePoint n X η) = E X η * (bL - 2 * X * deriv (fun (r : ℝ) => U r η) X / E X η) / 2) :

2 * X * deriv (fun (r : ℝ) => modulatedU n U B r η) X / modulatedE n E A X η = (bL + 2 * X * partialX B (phasePoint n X η) / (n * E X η)) / Real.exp (A (phasePoint n X η) / n)

Exact axial shear, including the multiplicative correction caused by the changed angular velocity in its denominator.

theorem NavierStokes.RadialModulation.angular_value_bound (E A n CE CA : ℝ) (hn : 0 < n) (hE : |E| ≤ CE) (hA : |A| ≤ CA) (hCA : CA ≤ n) :

|E * Real.exp (A / n) - E| ≤ 2 * CE * CA / n

Explicit uniform value estimate once the frequency exceeds the bound on A.

theorem NavierStokes.RadialModulation.axial_value_bound (U B n CB : ℝ) (hn : 0 < n) (hB : |B| ≤ CB) :

|U + B / n - U| ≤ CB / n

noncomputable def NavierStokes.RadialModulation.periodicPrimitive (q : ℝ → ℝ) (θ : ℝ) :

The primitive is an actual interval integral.

Equations

NavierStokes.RadialModulation.periodicPrimitive q θ = intervalIntegral q 0 θ MeasureTheory.volume

Instances For

theorem NavierStokes.RadialModulation.periodicPrimitive_hasDerivAt (q : ℝ → ℝ) (hq : Continuous q) (θ : ℝ) :

HasDerivAt (periodicPrimitive q) (q θ) θ

theorem NavierStokes.RadialModulation.periodicPrimitive_periodic (q : ℝ → ℝ) (hq : Continuous q) (hperiodic : Function.Periodic q 1) (hzero : intervalIntegral q 0 1 MeasureTheory.volume = 0) :

Function.Periodic (periodicPrimitive q) 1

Zero mean is precisely what removes the drift of the integral primitive.

theorem NavierStokes.RadialModulation.periodicPrimitive_contDiff (q : ℝ → ℝ) (hq : ContDiff ℝ (↑⊤) q) :

ContDiff ℝ (↑⊤) (periodicPrimitive q)

The integral primitive inherits all finite smoothness orders from q.

noncomputable def NavierStokes.RadialModulation.zeroMeanPrimitive (q : ℝ → ℝ) (θ : ℝ) :

Subtracting the primitive's mean fixes the zero-mean normalization.

Equations

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

Instances For

theorem NavierStokes.RadialModulation.zeroMeanPrimitive_hasDerivAt (q : ℝ → ℝ) (hq : Continuous q) (θ : ℝ) :

HasDerivAt (zeroMeanPrimitive q) (q θ) θ

theorem NavierStokes.RadialModulation.zeroMeanPrimitive_integral (q : ℝ → ℝ) (hq : Continuous q) :

intervalIntegral (zeroMeanPrimitive q) 0 1 MeasureTheory.volume = 0

theorem NavierStokes.RadialModulation.exists_smooth_periodic_zeroMean_primitive (q : ℝ → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hperiodic : Function.Periodic q 1) (hzero : intervalIntegral q 0 1 MeasureTheory.volume = 0) :

∃ (A : ℝ → ℝ), ContDiff ℝ (↑⊤) A ∧ Function.Periodic A 1 ∧ intervalIntegral A 0 1 MeasureTheory.volume = 0 ∧ ∀ (θ : ℝ), HasDerivAt A (q θ) θ

Every smooth period-one, mean-zero source has an actual smooth period-one, mean-zero primitive, with its derivative proved by the fundamental theorem.

theorem NavierStokes.RadialModulation.exists_primitive_of_prescribed_mean (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hperiodic : Function.Periodic f 1) (m c : ℝ) (hmean : intervalIntegral f 0 1 MeasureTheory.volume = m) :

∃ (A : ℝ → ℝ), ContDiff ℝ (↑⊤) A ∧ Function.Periodic A 1 ∧ intervalIntegral A 0 1 MeasureTheory.volume = 0 ∧ ∀ (θ : ℝ), HasDerivAt A (c * (f θ - m)) θ

Interface for a loop with prescribed mean: subtract the nominal shear and scale it, then construct its normalized primitive. Choosing c = -1/2 gives the angular primitive; c = E/2 gives the axial primitive.

Uniform bounds for every fixed parameter jet #

@[reducible, inline]

abbrev NavierStokes.RadialModulation.FamilyPoint :

Coordinates are amplitude, radius, parameter, periodic angle.

Equations

NavierStokes.RadialModulation.FamilyPoint = (ℝ × NavierStokes.RadialModulation.PhasePoint)

Instances For

def NavierStokes.RadialModulation.etaDirection :

Eta direction, given by (0, 0, 1, 0).

Equations

NavierStokes.RadialModulation.etaDirection = (0, 0, 1, 0)

Instances For

def NavierStokes.RadialModulation.amplitudeDirection :

Amplitude direction, given by (1, 0, 0, 0).

Equations

NavierStokes.RadialModulation.amplitudeDirection = (1, 0, 0, 0)

Instances For

def NavierStokes.RadialModulation.etaJet :

ℕ → (FamilyPoint → ℝ) → FamilyPoint → ℝ

Iterated genuine directional derivatives in the parameter coordinate.

Equations

One or more equations did not get rendered due to their size.
NavierStokes.RadialModulation.etaJet 0 x✝ = x✝

Instances For

theorem NavierStokes.RadialModulation.etaJet_contDiff (F : FamilyPoint → ℝ) (hF : ContDiff ℝ (↑⊤) F) (k : ℕ) :

ContDiff ℝ (↑⊤) (etaJet k F)

theorem NavierStokes.RadialModulation.etaJet_eq_iteratedDeriv (F : FamilyPoint → ℝ) (hF : ContDiff ℝ (↑⊤) F) (k : ℕ) (ε X η θ : ℝ) :

iteratedDeriv k (fun (e : ℝ) => F (ε, X, e, θ)) η = etaJet k F (ε, X, η, θ)

The directional jet is exactly the ordinary iterated derivative along η.

theorem NavierStokes.RadialModulation.uniform_periodic_family_eta_jets (F : FamilyPoint → ℝ) (hF : ContDiff ℝ (↑⊤) F) (hperiodic : ∀ (ε X η : ℝ), Function.Periodic (fun (θ : ℝ) => F (ε, X, η, θ)) 1) (KX Kη : Set ℝ) (hKX : IsCompact KX) (hKη : IsCompact Kη) (k : ℕ) :

∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℝ), 1 ≤ n → ∀ X ∈ KX, ∀ η ∈ Kη, ∀ (θ : ℝ), |iteratedDeriv k (fun (e : ℝ) => F (1 / n, X, e, θ)) η - iteratedDeriv k (fun (e : ℝ) => F (0, X, e, θ)) η| ≤ C / n

A smooth periodic family varies by C_k/n in each fixed η derivative, uniformly on compact radius/parameter sets and all angles. The constant is proved to exist by compactness of the actual next derivative, then the MVT.

noncomputable def NavierStokes.RadialModulation.angularFamily (E : BaseProfile) (A : PrimitiveProfile) (z : FamilyPoint) :

Angular family, given by E z.2.1 z.2.2.1 * Real.exp (z.1 * A z.2).

Equations

NavierStokes.RadialModulation.angularFamily E A z = E z.2.1 z.2.2.1 * Real.exp (z.1 * A z.2)

Instances For

def NavierStokes.RadialModulation.axialFamily (U : BaseProfile) (B : PrimitiveProfile) (z : FamilyPoint) :

Axial family, given by U z.2.1 z.2.2.1 + z.1 * B z.2.

Equations

NavierStokes.RadialModulation.axialFamily U B z = U z.2.1 z.2.2.1 + z.1 * B z.2

Instances For

theorem NavierStokes.RadialModulation.uniform_modulatedE_eta_jets (E : BaseProfile) (A : PrimitiveProfile) (hE : ContDiff ℝ (↑⊤) (Function.uncurry E)) (hA : ContDiff ℝ (↑⊤) A) (hperiodic : ∀ (X η : ℝ), Function.Periodic (fun (θ : ℝ) => A (X, η, θ)) 1) (KX Kη : Set ℝ) (hKX : IsCompact KX) (hKη : IsCompact Kη) (k : ℕ) :

∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℝ), 1 ≤ n → ∀ X ∈ KX, ∀ η ∈ Kη, |iteratedDeriv k (modulatedE n E A X) η - iteratedDeriv k (E X) η| ≤ C / n

Uniform O(1/n) closeness in every fixed actual η derivative of E. Taking KX = [Xa,Xb] with 0 < Xa gives the manuscript's compact positive annulus.

theorem NavierStokes.RadialModulation.uniform_modulatedU_eta_jets (U : BaseProfile) (B : PrimitiveProfile) (hU : ContDiff ℝ (↑⊤) (Function.uncurry U)) (hB : ContDiff ℝ (↑⊤) B) (hperiodic : ∀ (X η : ℝ), Function.Periodic (fun (θ : ℝ) => B (X, η, θ)) 1) (KX Kη : Set ℝ) (hKX : IsCompact KX) (hKη : IsCompact Kη) (k : ℕ) :

∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℝ), 1 ≤ n → ∀ X ∈ KX, ∀ η ∈ Kη, |iteratedDeriv k (modulatedU n U B X) η - iteratedDeriv k (U X) η| ≤ C / n

Uniform O(1/n) closeness in every fixed actual η derivative of U.

noncomputable def NavierStokes.ParametricModulation.primitiveFamily {P : Type u_1} (q : P × ℝ → ℝ) (z : P × ℝ) :

Primitive family, given by RadialModulation.periodicPrimitive (fun θ => q (z.1, θ)) z.2.

Equations

NavierStokes.ParametricModulation.primitiveFamily q z = NavierStokes.RadialModulation.periodicPrimitive (fun (θ : ℝ) => q (z.1, θ)) z.2

Instances For

noncomputable def NavierStokes.ParametricModulation.normalizedPrimitiveFamily {P : Type u_1} (q : P × ℝ → ℝ) (z : P × ℝ) :

Normalized primitive family, given by RadialModulation.zeroMeanPrimitive (fun θ => q (z.1, θ)) z.2.

Equations

NavierStokes.ParametricModulation.normalizedPrimitiveFamily q z = NavierStokes.RadialModulation.zeroMeanPrimitive (fun (θ : ℝ) => q (z.1, θ)) z.2

Instances For

theorem NavierStokes.ParametricModulation.primitiveFamily_unit_interval {P : Type u_1} (q : P × ℝ → ℝ) (z : P × ℝ) :

primitiveFamily q z = z.2 * ∫ (s : ℝ) in 0..1, q (z.1, z.2 * s)

The variable-endpoint integral is an integral over the fixed unit interval.

theorem NavierStokes.ParametricModulation.primitiveFamily_contDiffOn {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (q : P × ℝ → ℝ) (U : Set P) (hU : IsOpen U) (hq : ContDiffOn ℝ (↑⊤) q (U ×ˢ Set.univ)) :

ContDiffOn ℝ (↑⊤) (primitiveFamily q) (U ×ˢ Set.univ)

Joint smoothness of the actual primitive; all domination comes from the compact integration interval, through SmoothParameterIntegral.

theorem NavierStokes.ParametricModulation.normalizedPrimitiveFamily_contDiffOn {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (q : P × ℝ → ℝ) (U : Set P) (hU : IsOpen U) (hq : ContDiffOn ℝ (↑⊤) q (U ×ˢ Set.univ)) :

ContDiffOn ℝ (↑⊤) (normalizedPrimitiveFamily q) (U ×ˢ Set.univ)

Subtracting the actual parameter-dependent mean preserves joint smoothness.

theorem NavierStokes.ParametricModulation.source_slice_contDiff {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (q : P × ℝ → ℝ) (U : Set P) (hq : ContDiffOn ℝ (↑⊤) q (U ×ˢ Set.univ)) (p : P) (hp : p ∈ U) :

ContDiff ℝ ↑⊤ fun (θ : ℝ) => q (p, θ)

theorem NavierStokes.ParametricModulation.normalizedPrimitiveFamily_hasDerivAt {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (q : P × ℝ → ℝ) (U : Set P) (hq : ContDiffOn ℝ (↑⊤) q (U ×ˢ Set.univ)) (p : P) (hp : p ∈ U) (θ : ℝ) :

HasDerivAt (fun (s : ℝ) => normalizedPrimitiveFamily q (p, s)) (q (p, θ)) θ

theorem NavierStokes.ParametricModulation.normalizedPrimitiveFamily_periodic {P : Type u_1} (q : P × ℝ → ℝ) (p : P) (hq : Continuous fun (θ : ℝ) => q (p, θ)) (hper : Function.Periodic (fun (θ : ℝ) => q (p, θ)) 1) (hmean : ∫ (θ : ℝ) in 0..1, q (p, θ) = 0) :

Function.Periodic (fun (θ : ℝ) => normalizedPrimitiveFamily q (p, θ)) 1

theorem NavierStokes.ParametricModulation.normalizedPrimitiveFamily_mean_zero {P : Type u_1} (q : P × ℝ → ℝ) (p : P) (hq : Continuous fun (θ : ℝ) => q (p, θ)) :

∫ (θ : ℝ) in 0..1, normalizedPrimitiveFamily q (p, θ) = 0

theorem NavierStokes.ParametricModulation.normalizedPrimitiveFamily_zero {P : Type u_1} (q : P × ℝ → ℝ) (p : P) (hq : ∀ (θ : ℝ), q (p, θ) = 0) (θ : ℝ) :

normalizedPrimitiveFamily q (p, θ) = 0

Exact vanishing, including the mean normalization, when the loop is nominal.

structure NavierStokes.ParametricModulation.CompactCutoff {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (K U : Set P) :

Type u_1

A cutoff which equals one around K and vanishes locally outside U.

value : P → ℝ
Value of CompactCutoff, of type P → ℝ.
smooth : ContDiff ℝ (↑⊤) self.value
neighborhood : Set P
Neighborhood of CompactCutoff, of type Set P.
open_neighborhood : IsOpen self.neighborhood
contains : K ⊆ self.neighborhood
subset_domain : self.neighborhood ⊆ U
one_on (p : P) : p ∈ self.neighborhood → self.value p = 1
zero_near (p : P) : p ∉ U → self.value =ᶠ[nhds p] fun (x : P) => 0

Instances For

theorem NavierStokes.ParametricModulation.exists_compactCutoff {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (K U : Set P) (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :

Nonempty (CompactCutoff K U)

A smooth plateau cutoff is constructed from a smooth function supported exactly on U and its positive minimum over K.

theorem NavierStokes.ParametricModulation.CompactCutoff.mul_contDiff {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {K U : Set P} (χ : CompactCutoff K U) (hU : IsOpen U) (f : P × ℝ → ℝ) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.univ)) :

ContDiff ℝ ↑⊤ fun (z : P × ℝ) => χ.value z.1 * f z

Multiplication by the constructed cutoff extends a locally smooth periodic profile to a globally smooth function, unchanged around K.

def NavierStokes.ParametricModulation.centeredSource {P : Type u_1} (f : P × ℝ → ℝ) (m c : P → ℝ) (z : P × ℝ) :

Centered source, given by c z.1 * (f z - m z.1).

Equations

NavierStokes.ParametricModulation.centeredSource f m c z = c z.1 * (f z - m z.1)

Instances For

noncomputable def NavierStokes.ParametricModulation.extendedPrimitive {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {K U : Set P} (χ : CompactCutoff K U) (f : P × ℝ → ℝ) (m c : P → ℝ) (z : P × ℝ) :

Extended primitive, given by χ.value z.1 * normalizedPrimitiveFamily (centeredSource f m c) z.

Equations

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

Instances For

theorem NavierStokes.ParametricModulation.centeredSource_contDiffOn {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (f : P × ℝ → ℝ) (m c : P → ℝ) (U : Set P) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.univ)) (hm : ContDiff ℝ (↑⊤) m) (hc : ContDiff ℝ (↑⊤) c) :

ContDiffOn ℝ (↑⊤) (centeredSource f m c) (U ×ˢ Set.univ)

theorem NavierStokes.ParametricModulation.centeredSource_periodic {P : Type u_1} (f : P × ℝ → ℝ) (m c : P → ℝ) (p : P) (hf : Function.Periodic (fun (θ : ℝ) => f (p, θ)) 1) :

Function.Periodic (fun (θ : ℝ) => centeredSource f m c (p, θ)) 1

theorem NavierStokes.ParametricModulation.centeredSource_mean_zero {P : Type u_1} (f : P × ℝ → ℝ) (m c : P → ℝ) (p : P) (hf : Continuous fun (θ : ℝ) => f (p, θ)) (hm : ∫ (θ : ℝ) in 0..1, f (p, θ) = m p) :

∫ (θ : ℝ) in 0..1, centeredSource f m c (p, θ) = 0

theorem NavierStokes.ParametricModulation.extendedPrimitive_contDiff {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {K U : Set P} (χ : CompactCutoff K U) (hU : IsOpen U) (f : P × ℝ → ℝ) (m c : P → ℝ) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.univ)) (hm : ContDiff ℝ (↑⊤) m) (hc : ContDiff ℝ (↑⊤) c) :

ContDiff ℝ (↑⊤) (extendedPrimitive χ f m c)

theorem NavierStokes.ParametricModulation.extendedPrimitive_periodic {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {K U : Set P} (χ : CompactCutoff K U) (f : P × ℝ → ℝ) (m c : P → ℝ) (hf : ∀ p ∈ U, Continuous fun (θ : ℝ) => f (p, θ)) (hper : ∀ p ∈ U, Function.Periodic (fun (θ : ℝ) => f (p, θ)) 1) (hm : ∀ p ∈ U, ∫ (θ : ℝ) in 0..1, f (p, θ) = m p) (p : P) :

Function.Periodic (fun (θ : ℝ) => extendedPrimitive χ f m c (p, θ)) 1

theorem NavierStokes.ParametricModulation.extendedPrimitive_mean_zero {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {K U : Set P} (χ : CompactCutoff K U) (f : P × ℝ → ℝ) (m c : P → ℝ) (hf : ∀ p ∈ U, Continuous fun (θ : ℝ) => f (p, θ)) (p : P) :

∫ (θ : ℝ) in 0..1, extendedPrimitive χ f m c (p, θ) = 0

theorem NavierStokes.ParametricModulation.extendedPrimitive_hasDerivAt {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {K U : Set P} (χ : CompactCutoff K U) (f : P × ℝ → ℝ) (m c : P → ℝ) (hf : ∀ p ∈ U, Continuous fun (θ : ℝ) => f (p, θ)) (p : P) (hp : p ∈ K) (θ : ℝ) :

HasDerivAt (fun (s : ℝ) => extendedPrimitive χ f m c (p, s)) (c p * (f (p, θ) - m p)) θ

theorem NavierStokes.ParametricModulation.extendedPrimitive_zero {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {K U : Set P} (χ : CompactCutoff K U) (f : P × ℝ → ℝ) (m c : P → ℝ) (p : P) (hf : ∀ (θ : ℝ), f (p, θ) = m p) (θ : ℝ) :

extendedPrimitive χ f m c (p, θ) = 0

structure NavierStokes.ParametricModulation.TrueConeRealization {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (a m p₁ p₂ : P → ℝ) (K B : Set P) :

Type u_1

The only choice data are the already constructed true-cone loop parameters and an actual smooth compact-set cutoff. Primitives below are defined by integrals.

choices : TrueConeLoop.FamilyChoices a m p₁ p₂ K B
Choices of TrueConeRealization, of type TrueConeLoop.FamilyChoices a m p₁ p₂ K B.
cutoff : CompactCutoff K {p : P | 0 < a p}
Cutoff of TrueConeRealization, of type CompactCutoff K {p | 0 < a p}.

Instances For

theorem NavierStokes.ParametricModulation.exists_trueConeRealization {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (a m p₁ p₂ : P → ℝ) (K B : Set P) (hK : IsCompact K) (hB : IsCompact B) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₁ : ContDiff ℝ (↑⊤) p₁) (hp₂ : ContDiff ℝ (↑⊤) p₂) (haK : ∀ p ∈ K, 0 < a p) (hPK : ∀ p ∈ K, 2 < p₁ p + p₂ p * m p) (htrueB : ∀ p ∈ B, 2 < TrueConeLoop.nominalSpeed (a p) (m p)) :

Nonempty (TrueConeRealization a m p₁ p₂ K B)

noncomputable def NavierStokes.ParametricModulation.TrueConeRealization.angularLoop {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) :

P × ℝ → ℝ

Angular loop, given by TrueConeLoop.familyA a m p₂ r.choices.d r.choices.delta (ne_of_gt r.choices.d_pos) r.choices.delta_pos.

Equations

r.angularLoop = NavierStokes.TrueConeLoop.familyA a m p₂ r.choices.d r.choices.delta ⋯ ⋯

Instances For

noncomputable def NavierStokes.ParametricModulation.TrueConeRealization.signedAxialLoop {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) :

P × ℝ → ℝ

This is the signed loop coordinate -b_L, in the convention of TrueConeLoop.

Equations

r.signedAxialLoop = NavierStokes.TrueConeLoop.familyC a m p₂ r.choices.d r.choices.delta ⋯ ⋯

Instances For

noncomputable def NavierStokes.ParametricModulation.TrueConeRealization.angularPrimitive {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) :

P × ℝ → ℝ

Angular primitive, given by extendedPrimitive r.cutoff r.angularLoop a (fun _ => -1 / 2).

Equations

r.angularPrimitive = NavierStokes.ParametricModulation.extendedPrimitive r.cutoff r.angularLoop a fun (x : P) => -1 / 2

Instances For

noncomputable def NavierStokes.ParametricModulation.TrueConeRealization.axialPrimitive {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) (E : P → ℝ) :

P × ℝ → ℝ

Axial primitive, given by extendedPrimitive r.cutoff r.signedAxialLoop (fun p => a p * m p) (fun p => -E p / 2).

Equations

r.axialPrimitive E = NavierStokes.ParametricModulation.extendedPrimitive r.cutoff r.signedAxialLoop (fun (p : P) => a p * m p) fun (p : P) => -E p / 2

Instances For

theorem NavierStokes.ParametricModulation.TrueConeRealization.loop_smooth {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) :

ContDiffOn ℝ (↑⊤) r.angularLoop ({p : P | 0 < a p} ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) r.signedAxialLoop ({p : P | 0 < a p} ×ˢ Set.univ)

theorem NavierStokes.ParametricModulation.TrueConeRealization.loop_periods_means {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) (p : P) (hp : 0 < a p) :

Function.Periodic (fun (θ : ℝ) => r.angularLoop (p, θ)) 1 ∧ Function.Periodic (fun (θ : ℝ) => r.signedAxialLoop (p, θ)) 1 ∧ ∫ (θ : ℝ) in 0..1, r.angularLoop (p, θ) = a p ∧ ∫ (θ : ℝ) in 0..1, r.signedAxialLoop (p, θ) = a p * m p

theorem NavierStokes.ParametricModulation.TrueConeRealization.primitives_smooth {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) (E : P → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) :

ContDiff ℝ (↑⊤) r.angularPrimitive ∧ ContDiff ℝ (↑⊤) (r.axialPrimitive E)

theorem NavierStokes.ParametricModulation.TrueConeRealization.primitives_periodic {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) (E : P → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (p : P) :

Function.Periodic (fun (θ : ℝ) => r.angularPrimitive (p, θ)) 1 ∧ Function.Periodic (fun (θ : ℝ) => r.axialPrimitive E (p, θ)) 1

theorem NavierStokes.ParametricModulation.TrueConeRealization.primitives_mean_zero {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) (E : P → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (p : P) :

∫ (θ : ℝ) in 0..1, r.angularPrimitive (p, θ) = 0 ∧ ∫ (θ : ℝ) in 0..1, r.axialPrimitive E (p, θ) = 0

theorem NavierStokes.ParametricModulation.TrueConeRealization.primitive_derivatives {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) (E : P → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (p : P) (hp : p ∈ K) (θ : ℝ) :

HasDerivAt (fun (s : ℝ) => r.angularPrimitive (p, s)) (-(r.angularLoop (p, θ) - a p) / 2) θ ∧ HasDerivAt (fun (s : ℝ) => r.axialPrimitive E (p, s)) (E p * (-r.signedAxialLoop (p, θ) + a p * m p) / 2) θ

theorem NavierStokes.ParametricModulation.TrueConeRealization.boundary_vanishing {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) (E : P → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hBK : B ⊆ K) :

∃ (N : Set P), IsOpen N ∧ B ⊆ N ∧ ∀ p ∈ N, ∀ (θ : ℝ), r.angularPrimitive (p, θ) = 0 ∧ r.axialPrimitive E (p, θ) = 0

theorem NavierStokes.ParametricModulation.TrueConeRealization.loop_trueCone {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {a m p₁ p₂ : P → ℝ} {K B : Set P} (r : TrueConeRealization a m p₁ p₂ K B) (hrelaxed : ∀ p ∈ K, TrueConeLoop.nominalSpeed (a p) (m p) < ConeAlgebra.coneBound (p₁ p + p₂ p * m p) (p₂ p - p₁ p * m p)) (p : P) :

p ∈ K → ∀ (θ : ℝ), TrueConeLoop.InTrueCone (p₁ p) (p₂ p) (r.angularLoop (p, θ)) (r.signedAxialLoop (p, θ))

@[reducible, inline]

abbrev NavierStokes.ParametricModulation.RadialParameter :

Radial parameter: an abbreviation for ℝ × ℝ.

Equations

NavierStokes.ParametricModulation.RadialParameter = (ℝ × ℝ)

Instances For

def NavierStokes.ParametricModulation.asRadialPrimitive (Q : RadialParameter × ℝ → ℝ) :

RadialModulation.PrimitiveProfile

Reassociation between slow-parameter/angle coordinates and the radial modulation module's (X,η,θ) coordinates.

Equations

NavierStokes.ParametricModulation.asRadialPrimitive Q z = Q ((z.1, z.2.1), z.2.2)

Instances For

theorem NavierStokes.ParametricModulation.asRadialPrimitive_contDiff (Q : RadialParameter × ℝ → ℝ) (hQ : ContDiff ℝ (↑⊤) Q) :

ContDiff ℝ (↑⊤) (asRadialPrimitive Q)

noncomputable def NavierStokes.ParametricModulation.realizedE {a m p₁ p₂ : RadialParameter → ℝ} {K B : Set RadialParameter} (r : TrueConeRealization a m p₁ p₂ K B) (E : RadialParameter → ℝ) (n X η : ℝ) :

Realized E, given by RadialModulation.modulatedE n (fun X η => E (X, η)) (asRadialPrimitive r.angularPrimitive) X η.

Equations

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

Instances For

noncomputable def NavierStokes.ParametricModulation.realizedU {a m p₁ p₂ : RadialParameter → ℝ} {K B : Set RadialParameter} (r : TrueConeRealization a m p₁ p₂ K B) (E U : RadialParameter → ℝ) (n X η : ℝ) :

Realized U, given by RadialModulation.modulatedU n (fun X η => U (X, η)) (asRadialPrimitive (r.axialPrimitive E)) X η.

Equations

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

Instances For

theorem NavierStokes.ParametricModulation.realized_profiles_contDiffAt {a m p₁ p₂ : RadialParameter → ℝ} {K B : Set RadialParameter} (r : TrueConeRealization a m p₁ p₂ K B) (E U : RadialParameter → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (n X η : ℝ) (hX : X ≠ 0) :

ContDiffAt ℝ (↑⊤) (Function.uncurry (realizedE r E n)) (X, η) ∧ ContDiffAt ℝ (↑⊤) (Function.uncurry (realizedU r E U n)) (X, η)

Smoothness of the realized profiles follows from the constructed integral primitives, without any primitive-smoothness assumption.

theorem NavierStokes.ParametricModulation.realized_profiles_uniform_eta_jets {a m p₁ p₂ : RadialParameter → ℝ} {K B : Set RadialParameter} (r : TrueConeRealization a m p₁ p₂ K B) (E U : RadialParameter → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (KX Kη : Set ℝ) (hKX : IsCompact KX) (hKη : IsCompact Kη) (k : ℕ) :

∃ (CE : ℝ) (CU : ℝ), 0 ≤ CE ∧ 0 ≤ CU ∧ ∀ (n : ℝ), 1 ≤ n → ∀ X ∈ KX, ∀ η ∈ Kη, |iteratedDeriv k (realizedE r E n X) η - iteratedDeriv k (fun (e : ℝ) => E (X, e)) η| ≤ CE / n ∧ |iteratedDeriv k (realizedU r E U n X) η - iteratedDeriv k (fun (e : ℝ) => U (X, e)) η| ≤ CU / n

Every fixed actual η jet is O(1/n), now for the primitives constructed from the actual TrueConeLoop family, uniformly on arbitrary compact sets.

theorem NavierStokes.ParametricModulation.realized_profiles_boundary_match {a m p₁ p₂ : RadialParameter → ℝ} {K B : Set RadialParameter} (r : TrueConeRealization a m p₁ p₂ K B) (E U : RadialParameter → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hBK : B ⊆ K) :

∃ (N : Set RadialParameter), IsOpen N ∧ B ⊆ N ∧ ∀ (n X η : ℝ), (X, η) ∈ N → realizedE r E n X η = E (X, η) ∧ realizedU r E U n X η = U (X, η)

The constructed profiles agree exactly with the nominal profiles on one open neighborhood of the prescribed boundary set, for every frequency.

theorem NavierStokes.ParametricModulation.theta_derivative_asRadialPrimitive (Q : RadialParameter × ℝ → ℝ) (hQ : ContDiff ℝ (↑⊤) Q) (X η θ : ℝ) :

HasDerivAt (fun (s : ℝ) => Q ((X, η), s)) (RadialModulation.partialTheta (asRadialPrimitive Q) (X, η, θ)) θ

theorem NavierStokes.ParametricModulation.realized_primitive_theta {a m p₁ p₂ : RadialParameter → ℝ} {K B : Set RadialParameter} (r : TrueConeRealization a m p₁ p₂ K B) (E : RadialParameter → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) (X η θ : ℝ) (hp : (X, η) ∈ K) :

RadialModulation.partialTheta (asRadialPrimitive r.angularPrimitive) (X, η, θ) = -(r.angularLoop ((X, η), θ) - a (X, η)) / 2 ∧ RadialModulation.partialTheta (asRadialPrimitive (r.axialPrimitive E)) (X, η, θ) = E (X, η) * (-r.signedAxialLoop ((X, η), θ) + a (X, η) * m (X, η)) / 2

The prescribed loop derivatives are established for the constructed primitives, including the sign change from C = -b_L.

theorem NavierStokes.ParametricModulation.realized_shears_exact {a m p₁ p₂ : RadialParameter → ℝ} {K B : Set RadialParameter} (r : TrueConeRealization a m p₁ p₂ K B) (E U : RadialParameter → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (n X η : ℝ) (hn : n ≠ 0) (hX : X ≠ 0) (hE0 : E (X, η) ≠ 0) (hp : (X, η) ∈ K) (haNom : a (X, η) = 1 - 2 * X * deriv (fun (x : ℝ) => E (x, η)) X / E (X, η)) (hbNom : -a (X, η) * m (X, η) = 2 * X * deriv (fun (x : ℝ) => U (x, η)) X / E (X, η)) :

1 - 2 * X * deriv (fun (x : ℝ) => realizedE r E n x η) X / realizedE r E n X η = r.angularLoop ((X, η), n * Real.log X) - 2 * X * RadialModulation.partialX (asRadialPrimitive r.angularPrimitive) (X, η, n * Real.log X) / n ∧ 2 * X * deriv (fun (x : ℝ) => realizedU r E U n x η) X / realizedE r E n X η = (-r.signedAxialLoop ((X, η), n * Real.log X) + 2 * X * RadialModulation.partialX (asRadialPrimitive (r.axialPrimitive E)) (X, η, n * Real.log X) / (n * E (X, η))) / Real.exp (r.angularPrimitive ((X, η), n * Real.log X) / n)

Exact shear identities after composition of the constructed true-cone loop, its actual integral primitives, and radial modulation.

theorem NavierStokes.ParametricModulation.exists_modulated_trueCone_profiles (a m p₁ p₂ E U : RadialParameter → ℝ) (KX Kη : Set ℝ) (B : Set RadialParameter) (hKX : IsCompact KX) (hKη : IsCompact Kη) (hB : IsCompact B) (hBK : B ⊆ KX ×ˢ Kη) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₁ : ContDiff ℝ (↑⊤) p₁) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (haK : ∀ p ∈ KX ×ˢ Kη, 0 < a p) (hPK : ∀ p ∈ KX ×ˢ Kη, 2 < p₁ p + p₂ p * m p) (hrelaxed : ∀ p ∈ KX ×ˢ Kη, TrueConeLoop.nominalSpeed (a p) (m p) < ConeAlgebra.coneBound (p₁ p + p₂ p * m p) (p₂ p - p₁ p * m p)) (htrueB : ∀ p ∈ B, 2 < TrueConeLoop.nominalSpeed (a p) (m p)) :

∃ (r : TrueConeRealization a m p₁ p₂ (KX ×ˢ Kη) B), (∀ p ∈ KX ×ˢ Kη, ∀ (θ : ℝ), TrueConeLoop.InTrueCone (p₁ p) (p₂ p) (r.angularLoop (p, θ)) (r.signedAxialLoop (p, θ))) ∧ (∀ (n X η : ℝ), X ≠ 0 → ContDiffAt ℝ (↑⊤) (Function.uncurry (realizedE r E n)) (X, η) ∧ ContDiffAt ℝ (↑⊤) (Function.uncurry (realizedU r E U n)) (X, η)) ∧ (∀ (k : ℕ), ∃ (CE : ℝ) (CU : ℝ), 0 ≤ CE ∧ 0 ≤ CU ∧ ∀ (n : ℝ), 1 ≤ n → ∀ X ∈ KX, ∀ η ∈ Kη, |iteratedDeriv k (realizedE r E n X) η - iteratedDeriv k (fun (e : ℝ) => E (X, e)) η| ≤ CE / n ∧ |iteratedDeriv k (realizedU r E U n X) η - iteratedDeriv k (fun (e : ℝ) => U (X, e)) η| ≤ CU / n) ∧ ∃ (N : Set RadialParameter), IsOpen N ∧ B ⊆ N ∧ ∀ (n X η : ℝ), (X, η) ∈ N → realizedE r E n X η = E (X, η) ∧ realizedU r E U n X η = U (X, η)

End-to-end existence from nominal scalar data: construct the actual TrueConeLoop family, its normalized integral primitives, and modulated profiles. All smoothness and finite-jet conclusions are proved for these constructions.