Actual natural profiles in the original radial variable

This module reconstructs the unscaled natural profiles from the actual smooth solutions of the coefficient-space problem. Derivative identities refer to ordinary derivatives of the reconstructed real functions.

The actual fixed coefficients of the natural-axis problem

The pressure comes from its proved holomorphic integral extension. A common complex neighborhood is chosen by compactness and nonvanishing of the two actual denominators. Every fixed field is then embedded in the same complete space of compatible coefficient functions.

The fixed real natural-axis data

The small parameters are quantitative. The unique zero of H is proved, not postulated. The pressure is an input with explicit real smoothness, negativity, and derivative-sign hypotheses; its construction and complex analytic estimates are separate results.

The pressure datum from a nonnegative weighted schedule

The clock weights and bounded exponents are fixed input functions. Regularity of the pressure is deduced from the integral, not assumed as an input.

noncomputable def NavierStokes.PressureDatum.kernel (a η : ℝ) : ℝ

Real form of (1 + η²)^(-2a).

Equations

• NavierStokes.PressureDatum.kernel a η = Real.exp (-2 * a * Real.log (1 + η ^ 2))

noncomputable def NavierStokes.PressureDatum.pressure (g a : ℝ → ℝ) (η : ℝ) : ℝ

Pressure, given by -(1 / 2 : ℝ) * ∫ y, g y * kernel (a y) η.

Equations

• NavierStokes.PressureDatum.pressure g a η = -(1 / 2) * ∫ (y : ℝ), g y * NavierStokes.PressureDatum.kernel (a y) η

structure NavierStokes.PressureDatum.Admissible (g a : ℝ → ℝ) (A : ℝ) : Prop

Sufficient hypotheses on the fixed clock data. No pressure derivatives occur here.

• cap_nonneg : 0 ≤ A
• integrable : MeasureTheory.Integrable g MeasureTheory.volume
• nonneg (y : ℝ) : 0 ≤ g y
• measurable : Measurable a
• exponent_nonneg (y : ℝ) : 0 ≤ a y
• exponent_le (y : ℝ) : a y ≤ A

theorem NavierStokes.PressureDatum.kernel_eq_rpow (a η : ℝ) : kernel a η = (1 + η ^ 2) ^ (-2 * a)

theorem NavierStokes.PressureDatum.kernel_pos (a η : ℝ) : 0 < kernel a η

theorem NavierStokes.PressureDatum.kernel_le_one {a : ℝ} (ha : 0 ≤ a) (η : ℝ) : kernel a η ≤ 1

theorem NavierStokes.PressureDatum.kernel_antitone {a b : ℝ} (hab : a ≤ b) (η : ℝ) : kernel b η ≤ kernel a η

@[simp]

theorem NavierStokes.PressureDatum.kernel_neg (a η : ℝ) : kernel a (-η) = kernel a η

@[simp]

theorem NavierStokes.PressureDatum.pressure_neg (g a : ℝ → ℝ) (η : ℝ) : pressure g a (-η) = pressure g a η

theorem NavierStokes.PressureDatum.kernel_measurable {a : ℝ → ℝ} (ha : Measurable a) (η : ℝ) : Measurable fun (y : ℝ) => kernel (a y) η

theorem NavierStokes.PressureDatum.integrable_kernel {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (η : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => g y * kernel (a y) η) MeasureTheory.volume

theorem NavierStokes.PressureDatum.pressure_nonpos {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (η : ℝ) : pressure g a η ≤ 0

theorem NavierStokes.PressureDatum.pressure_le_mass {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (η : ℝ) : pressure g a η ≤ -(1 / 2) * kernel A η * ∫ (y : ℝ), g y

theorem NavierStokes.PressureDatum.pressure_translate (g a : ℝ → ℝ) (c η : ℝ) : pressure (fun (y : ℝ) => g (y + c)) (fun (y : ℝ) => a (y + c)) η = pressure g a η

Shifting the logarithmic clock leaves the datum unchanged.

def NavierStokes.PressureDatum.strip : Set ℂ

A strip containing the complete real axis and therefore [-1,1].

Equations

• NavierStokes.PressureDatum.strip = {z : ℂ | |z.im| < 1 / 2}

theorem NavierStokes.PressureDatum.strip_open : IsOpen strip

@[simp]

theorem NavierStokes.PressureDatum.real_mem_strip (η : ℝ) : ↑η ∈ strip

theorem NavierStokes.PressureDatum.base_mem_slitPlane {z : ℂ} (hz : z ∈ strip) : 1 + z ^ 2 ∈ Complex.slitPlane

noncomputable def NavierStokes.PressureDatum.complexKernel (a : ℝ) (z : ℂ) : ℂ

Complex kernel, given by Complex.exp ((-2 * (a : ℂ)) * Complex.log (1 + z ^ 2)).

Equations

• NavierStokes.PressureDatum.complexKernel a z = Complex.exp (-2 * ↑a * Complex.log (1 + z ^ 2))

noncomputable def NavierStokes.PressureDatum.complexKernelDeriv (a : ℝ) (z : ℂ) : ℂ

Complex kernel derivative, given by complexKernel a z * ((-2 * (a : ℂ)) * ((1 + z ^ 2)⁻¹ * (2 * z))).

Equations

• NavierStokes.PressureDatum.complexKernelDeriv a z = NavierStokes.PressureDatum.complexKernel a z * (-2 * ↑a * ((1 + z ^ 2)⁻¹ * (2 * z)))

theorem NavierStokes.PressureDatum.hasDerivAt_complexKernel (a : ℝ) {z : ℂ} (hz : z ∈ strip) : HasDerivAt (complexKernel a) (complexKernelDeriv a z) z

theorem NavierStokes.PressureDatum.continuous_complexKernel_parameter (z : ℂ) : Continuous fun (b : ℝ) => complexKernel b z

theorem NavierStokes.PressureDatum.continuous_complexKernelDeriv_parameter (z : ℂ) : Continuous fun (b : ℝ) => complexKernelDeriv b z

theorem NavierStokes.PressureDatum.continuousOn_complexKernel {s : Set (ℝ × ℂ)} (hs : ∀ p ∈ s, p.2 ∈ strip) : ContinuousOn (fun (p : ℝ × ℂ) => complexKernel p.1 p.2) s

theorem NavierStokes.PressureDatum.continuousOn_complexKernelDeriv {s : Set (ℝ × ℂ)} (hs : ∀ p ∈ s, p.2 ∈ strip) : ContinuousOn (fun (p : ℝ × ℂ) => complexKernelDeriv p.1 p.2) s

theorem NavierStokes.PressureDatum.measurable_weighted_parameter {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) {k : ℝ → ℂ} (hk : Continuous k) : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => ↑(g y) * k (a y)) MeasureTheory.volume

theorem NavierStokes.PressureDatum.integrable_weighted_parameter {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) {k : ℝ → ℂ} (hk : Continuous k) : MeasureTheory.Integrable (fun (y : ℝ) => ↑(g y) * k (a y)) MeasureTheory.volume

Compactness of the bounded exponent interval supplies the dominating constant.

noncomputable def NavierStokes.PressureDatum.complexPressure (g a : ℝ → ℝ) (z : ℂ) : ℂ

Complex pressure, given by -(1 / 2 : ℂ) * ∫ y, (g y : ℂ) * complexKernel (a y) z.

Equations

• NavierStokes.PressureDatum.complexPressure g a z = -(1 / 2) * ∫ (y : ℝ), ↑(g y) * NavierStokes.PressureDatum.complexKernel (a y) z

theorem NavierStokes.PressureDatum.integrable_complexKernel {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (z : ℂ) : MeasureTheory.Integrable (fun (y : ℝ) => ↑(g y) * complexKernel (a y) z) MeasureTheory.volume

theorem NavierStokes.PressureDatum.hasDerivAt_complexPressure {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) {z : ℂ} (hz : z ∈ strip) : HasDerivAt (complexPressure g a) (-(1 / 2) * ∫ (y : ℝ), ↑(g y) * complexKernelDeriv (a y) z) z

theorem NavierStokes.PressureDatum.complexPressure_analytic {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) : AnalyticOnNhd ℂ (complexPressure g a) strip

Holomorphic extension is proved by dominated differentiation on the strip.

@[simp]

theorem NavierStokes.PressureDatum.complexKernel_ofReal (a η : ℝ) : complexKernel a ↑η = ↑(kernel a η)

@[simp]

theorem NavierStokes.PressureDatum.complexPressure_ofReal (g a : ℝ → ℝ) (η : ℝ) : complexPressure g a ↑η = ↑(pressure g a η)

theorem NavierStokes.PressureDatum.pressure_contDiff {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) : ContDiff ℝ (↑⊤) (pressure g a)

Smoothness follows from the proved complex extension, for every finite order at once.

theorem NavierStokes.PressureDatum.complexPressure_bounded_on_compact {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) {s : Set ℂ} (hs : IsCompact s) (hss : s ⊆ strip) : ∃ (M : ℝ), ∀ z ∈ s, ‖complexPressure g a z‖ ≤ M

theorem NavierStokes.PressureDatum.integrable_exponent_weight {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) : MeasureTheory.Integrable (fun (y : ℝ) => g y * a y) MeasureTheory.volume

theorem NavierStokes.PressureDatum.exponent_weight_admissible {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) : Admissible (fun (y : ℝ) => g y * a y) a A

theorem NavierStokes.PressureDatum.exponent_mass_pos_of_active {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (hactive : 0 < MeasureTheory.volume {y : ℝ | 0 < g y ∧ 0 < a y}) : 0 < ∫ (y : ℝ), g y * a y

theorem NavierStokes.PressureDatum.complexKernelDeriv_ofReal (a η : ℝ) : complexKernelDeriv a ↑η = ↑(kernel a η * (-4 * a * η / (1 + η ^ 2)))

theorem NavierStokes.PressureDatum.hasDerivAt_pressure {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (η : ℝ) : HasDerivAt (pressure g a) (2 * η / (1 + η ^ 2) * ∫ (y : ℝ), g y * a y * kernel (a y) η) η

The derivative is the positive radial factor times the weighted positive-exponent mass.

theorem NavierStokes.PressureDatum.deriv_pressure {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (η : ℝ) : deriv (pressure g a) η = 2 * η / (1 + η ^ 2) * ∫ (y : ℝ), g y * a y * kernel (a y) η

theorem NavierStokes.PressureDatum.weighted_kernel_pos {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (hmass : 0 < ∫ (y : ℝ), g y * a y) (η : ℝ) : 0 < ∫ (y : ℝ), g y * a y * kernel (a y) η

theorem NavierStokes.PressureDatum.deriv_pressure_pos {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (hmass : 0 < ∫ (y : ℝ), g y * a y) {η : ℝ} (hη : 0 < η) : 0 < deriv (pressure g a) η

theorem NavierStokes.PressureDatum.deriv_pressure_pos_of_active {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (hactive : 0 < MeasureTheory.volume {y : ℝ | 0 < g y ∧ 0 < a y}) {η : ℝ} (hη : 0 < η) : 0 < deriv (pressure g a) η

theorem NavierStokes.PressureDatum.deriv_pressure_neg {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) (hmass : 0 < ∫ (y : ℝ), g y * a y) {η : ℝ} (hη : η < 0) : deriv (pressure g a) η < 0

theorem NavierStokes.PressureDatum.deriv_pressure_zero {g a : ℝ → ℝ} {A : ℝ} (h : Admissible g a A) : deriv (pressure g a) 0 = 0

theorem NavierStokes.PressureDatum.pressure_le_prefix {g a : ℝ → ℝ} {A b : ℝ} (h : Admissible g a A) {s : Set ℝ} (hs : MeasurableSet s) (ha : ∀ y ∈ s, a y = b) (η : ℝ) : pressure g a η ≤ -(1 / 2) * kernel b η * ∫ (y : ℝ) in s, g y

An arbitrary measurable positive prefix contributes its exact constant-exponent mass.

theorem NavierStokes.PressureDatum.pressure_le_prefix_mass {g a : ℝ → ℝ} {A b m : ℝ} (h : Admissible g a A) {s : Set ℝ} (hs : MeasurableSet s) (ha : ∀ y ∈ s, a y = b) (hm : m ≤ ∫ (y : ℝ) in s, g y) (η : ℝ) : pressure g a η ≤ -(1 / 2) * m * kernel b η

theorem NavierStokes.PressureDatum.kernel_one (η : ℝ) : kernel 1 η = (1 + η ^ 2)⁻¹ ^ 2

theorem NavierStokes.PressureDatum.manuscript_prefix_bound {g a : ℝ → ℝ} {A P : ℝ} (h : Admissible g a A) {s : Set ℝ} (hs : MeasurableSet s) (ha : ∀ y ∈ s, a y = 1) (hm : 5 * P ^ 2 ≤ ∫ (y : ℝ) in s, g y) (η : ℝ) : pressure g a η ≤ -(5 / 2) * P ^ 2 * (1 + η ^ 2)⁻¹ ^ 2

The manuscript's ideal prefix has exponent one and mass 5 P².

theorem NavierStokes.PressureDatum.ideal_prefix_mass (P : ℝ) : ∫ (y : ℝ) in Set.Iic 0, P ^ 2 * Real.exp (1 / 5 * y) = 5 * P ^ 2

Exact integral of the ideal clock prefix P² exp(y/5).

theorem NavierStokes.PressureDatum.prefix_mass_eq {g : ℝ → ℝ} {P : ℝ} (hg : ∀ y ≤ 0, g y = P ^ 2 * Real.exp (1 / 5 * y)) : ∫ (y : ℝ) in Set.Iic 0, g y = 5 * P ^ 2

theorem NavierStokes.PressureDatum.pressure_le_of_ideal_prefix {g a : ℝ → ℝ} {A P : ℝ} (h : Admissible g a A) (hg : ∀ y ≤ 0, g y = P ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) (η : ℝ) : pressure g a η ≤ -(5 / 2) * P ^ 2 * (1 + η ^ 2)⁻¹ ^ 2

The exact manuscript lower bound, with the prefix integral evaluated.

theorem NavierStokes.PressureDatum.exponent_mass_pos_of_ideal_prefix {g a : ℝ → ℝ} {A P : ℝ} (h : Admissible g a A) (hP : 0 < P) (hg : ∀ y ≤ 0, g y = P ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) : 0 < ∫ (y : ℝ), g y * a y

theorem NavierStokes.PressureDatum.pressure_neg_of_ideal_prefix {g a : ℝ → ℝ} {A P : ℝ} (h : Admissible g a A) (hP : 0 < P) (hg : ∀ y ≤ 0, g y = P ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) (η : ℝ) : pressure g a η < 0

noncomputable def NavierStokes.NaturalAxisData.D (h : ℝ) : ℝ

D, given by 1 / 2 - h.

Equations

• NavierStokes.NaturalAxisData.D h = 1 / 2 - h

noncomputable def NavierStokes.NaturalAxisData.A (h : ℝ) : ℝ

A, given by 1 / 2 + h.

Equations

• NavierStokes.NaturalAxisData.A h = 1 / 2 + h

def NavierStokes.NaturalAxisData.d (η : ℝ) : ℝ

D, given by 1 - η ^ 2.

Equations

• NavierStokes.NaturalAxisData.d η = 1 - η ^ 2

def NavierStokes.NaturalAxisData.L (h η : ℝ) : ℝ

L, given by 1 - 2 * h * η ^ 2.

Equations

• NavierStokes.NaturalAxisData.L h η = 1 - 2 * h * η ^ 2

def NavierStokes.NaturalAxisData.U (j η : ℝ) : ℝ

U, given by 4 * η + j.

Equations

• NavierStokes.NaturalAxisData.U j η = 4 * η + j

noncomputable def NavierStokes.NaturalAxisData.H (h j η : ℝ) : ℝ

H, given by D h * η + d η * U j η.

Equations

• NavierStokes.NaturalAxisData.H h j η = NavierStokes.NaturalAxisData.D h * η + NavierStokes.NaturalAxisData.d η * NavierStokes.NaturalAxisData.U j η

noncomputable def NavierStokes.NaturalAxisData.W (h j η : ℝ) : ℝ

W, given by 1 - 4 * d η - 2 * D h * η * U j η.

Equations

• NavierStokes.NaturalAxisData.W h j η = 1 - 4 * NavierStokes.NaturalAxisData.d η - 2 * NavierStokes.NaturalAxisData.D h * η * NavierStokes.NaturalAxisData.U j η

noncomputable def NavierStokes.NaturalAxisData.Z (h j : ℝ) (P : ℝ → ℝ) (η : ℝ) : ℝ

Z, given by -A h * (1 - 2 * η * U j η) * U j η - H h j η * 4 - d η * deriv P η + 4 * A h * η * P η.

Equations

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

noncomputable def NavierStokes.NaturalAxisData.chi (h j σ η : ℝ) : ℝ

Chi, given by (H h j η) ^ 2 / ((H h j η) ^ 2 + σ ^ 2).

Equations

• NavierStokes.NaturalAxisData.chi h j σ η = NavierStokes.NaturalAxisData.H h j η ^ 2 / (NavierStokes.NaturalAxisData.H h j η ^ 2 + σ ^ 2)

structure NavierStokes.NaturalAxisData.SmallParameters (h j : ℝ) : Prop

A concrete range of choices permitted by the manuscript's smallness order.

• h_pos : 0 < h
• h_le : h ≤ 1 / 1000
• j_pos : 0 < j
• j_le : j ≤ 1 / 1000

theorem NavierStokes.NaturalAxisData.D_bounds {h j : ℝ} (p : SmallParameters h j) : 499 / 1000 ≤ D h ∧ D h < 1 / 2

theorem NavierStokes.NaturalAxisData.D_pos {h j : ℝ} (p : SmallParameters h j) : 0 < D h

theorem NavierStokes.NaturalAxisData.A_bounds {h j : ℝ} (p : SmallParameters h j) : 1 / 2 < A h ∧ A h ≤ 501 / 1000

theorem NavierStokes.NaturalAxisData.A_pos {h j : ℝ} (p : SmallParameters h j) : 0 < A h

theorem NavierStokes.NaturalAxisData.d_nonneg {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : 0 ≤ d η

theorem NavierStokes.NaturalAxisData.L_lower_bound {h j η : ℝ} (p : SmallParameters h j) (hη : η ∈ Set.Icc (-1) 1) : 499 / 500 ≤ L h η

theorem NavierStokes.NaturalAxisData.L_pos {h j η : ℝ} (p : SmallParameters h j) (hη : η ∈ Set.Icc (-1) 1) : 0 < L h η

theorem NavierStokes.NaturalAxisData.neg_W_formula (h j η : ℝ) : -W h j η = 3 - 8 * h * η ^ 2 + 2 * D h * j * η

theorem NavierStokes.NaturalAxisData.neg_W_lower_bound {h j η : ℝ} (p : SmallParameters h j) (hη : η ∈ Set.Icc (-1) 1) : 2991 / 1000 ≤ -W h j η

The proof gives 2.991, stronger than the manuscript's 2.8.

theorem NavierStokes.NaturalAxisData.neg_W_gt {h j η : ℝ} (p : SmallParameters h j) (hη : η ∈ Set.Icc (-1) 1) : 14 / 5 < -W h j η

theorem NavierStokes.NaturalAxisData.H_contDiff (h j : ℝ) : ContDiff ℝ (↑⊤) (H h j)

theorem NavierStokes.NaturalAxisData.H_at_left (h j : ℝ) : H h j (-j / 4) = -(D h * j) / 4

theorem NavierStokes.NaturalAxisData.H_at_right (h j : ℝ) : H h j (-j / 5) = j / 5 * (1 - D h - j ^ 2 / 25)

theorem NavierStokes.NaturalAxisData.H_left_neg {h j : ℝ} (p : SmallParameters h j) : H h j (-j / 4) < 0

theorem NavierStokes.NaturalAxisData.H_right_pos {h j : ℝ} (p : SmallParameters h j) : 0 < H h j (-j / 5)

theorem NavierStokes.NaturalAxisData.H_pos_of_nonneg {h j η : ℝ} (p : SmallParameters h j) (hη : η ∈ Set.Icc (-1) 1) (hη0 : 0 ≤ η) : 0 < H h j η

theorem NavierStokes.NaturalAxisData.H_neg_of_le_left {h j η : ℝ} (p : SmallParameters h j) (hη : η ∈ Set.Icc (-1) 1) (hleft : η ≤ -j / 4) : H h j η < 0

theorem NavierStokes.NaturalAxisData.root_negative {h j η : ℝ} (p : SmallParameters h j) (hη : η ∈ Set.Icc (-1) 1) (hzero : H h j η = 0) : η < 0

theorem NavierStokes.NaturalAxisData.cross_identity (h j x y : ℝ) : H h j x * d y - H h j y * d x = (x - y) * (D h * (1 + x * y) + 4 * d x * d y)

theorem NavierStokes.NaturalAxisData.root_unique {h j x y : ℝ} (p : SmallParameters h j) (hx : x ∈ Set.Icc (-1) 1) (hy : y ∈ Set.Icc (-1) 1) (hx0 : H h j x = 0) (hy0 : H h j y = 0) : x = y

Uniqueness is proved algebraically from the actual polynomial.

theorem NavierStokes.NaturalAxisData.exists_unique_root {h j : ℝ} (p : SmallParameters h j) : ∃ η₀ ∈ Set.Ioo (-j / 4) (-j / 5), H h j η₀ = 0 ∧ ∀ η ∈ Set.Icc (-1) 1, H h j η = 0 → η = η₀

The unique zero lies strictly between -j/4 and -j/5.

structure NavierStokes.NaturalAxisData.PressureData (P : ℝ → ℝ) : Prop

Real pressure hypotheses provided by the separately constructed datum. The derivative-sign condition is weak, so zero derivative is permitted.

• smooth : ContDiff ℝ (↑⊤) P
• negative (η : ℝ) : η ∈ Set.Icc (-1) 1 → P η ≤ -1
• derivative_sign (η : ℝ) : η ∈ Set.Icc (-1) 1 → 0 ≤ η * deriv P η

theorem NavierStokes.NaturalAxisData.PressureData.deriv_nonpos {P : ℝ → ℝ} (pP : PressureData P) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) (hn : η < 0) : deriv P η ≤ 0

theorem NavierStokes.NaturalAxisData.Z_at_root_lower {h j η : ℝ} {P : ℝ → ℝ} (p : SmallParameters h j) (hη : η ∈ Set.Ioo (-j / 4) (-j / 5)) (hz : H h j η = 0) (hP : P η ≤ -1) (hP' : deriv P η ≤ 0) : j / 5 < Z h j P η

A quantitative version of the crucial nonzero-root assertion: pressure at most minus one is already sufficient.

theorem NavierStokes.NaturalAxisData.Z_continuous (h j : ℝ) {P : ℝ → ℝ} (hP : ContDiff ℝ (↑⊤) P) : Continuous (Z h j P)

theorem NavierStokes.NaturalAxisData.exists_root_with_positive_Z {h j : ℝ} {P : ℝ → ℝ} (p : SmallParameters h j) (pP : PressureData P) : ∃ η₀ ∈ Set.Ioo (-j / 4) (-j / 5), H h j η₀ = 0 ∧ j / 5 < Z h j P η₀ ∧ ∀ η ∈ Set.Icc (-1) 1, H h j η = 0 → η = η₀

The true fixed data have a unique negative root at which Z is bounded strictly away from zero. No root property is an input hypothesis.

theorem NavierStokes.NaturalAxisData.low_Z_has_H_margin {h j : ℝ} {P : ℝ → ℝ} (p : SmallParameters h j) (pP : PressureData P) : ∃ (m : ℝ), 0 < m ∧ ∀ η ∈ Set.Icc (-1) 1, |Z h j P η| ≤ j / 10 → m ≤ H h j η ^ 2

On the actual compact low-Z set, H² has a strictly positive uniform minimum. The threshold is the explicit choice δ_* = j/10.

theorem NavierStokes.NaturalAxisData.chi_contDiff (h j : ℝ) {σ : ℝ} (hσ : 0 < σ) : ContDiff ℝ (↑⊤) (chi h j σ)

theorem NavierStokes.NaturalAxisData.chi_bounds (h j : ℝ) {σ : ℝ} (hσ : 0 < σ) (η : ℝ) : 0 ≤ chi h j σ η ∧ chi h j σ η < 1

theorem NavierStokes.NaturalAxisData.exists_sigma {h j : ℝ} {P : ℝ → ℝ} (p : SmallParameters h j) (pP : PressureData P) : ∃ (σ : ℝ), 0 < σ ∧ ∀ η ∈ Set.Icc (-1) 1, |Z h j P η| ≤ j / 10 → 99 / 100 < chi h j σ η

Construct the cutoff scale after the root-separation proof. The proof chooses σ_* = sqrt(m)/20 from the actual compact minimum bound.

theorem NavierStokes.NaturalAxisData.exists_cutoff_parameters {h j : ℝ} {P : ℝ → ℝ} (p : SmallParameters h j) (pP : PressureData P) : ∃ (δ : ℝ) (σ : ℝ), 0 < δ ∧ 0 < σ ∧ (∀ η ∈ Set.Icc (-1) 1, |Z h j P η| ≤ δ → 99 / 100 < chi h j σ η) ∧ ContDiff ℝ (↑⊤) (chi h j σ)

The requested fixed positive choices, with no input separation premise.

theorem NavierStokes.NaturalAxisData.pressureData_of_ideal_prefix {g a : ℝ → ℝ} {cap B : ℝ} (hp : PressureDatum.Admissible g a cap) (hB : 2 ≤ B) (hg : ∀ y ≤ 0, g y = B ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) : PressureData (PressureDatum.pressure g a)

The actual integral pressure datum satisfies the real axis hypotheses. The ideal-prefix amplitude B ≥ 2 suffices uniformly on [-1,1].

theorem NavierStokes.NaturalAxisData.ideal_prefix_cutoff_parameters {h j : ℝ} (p : SmallParameters h j) {g a : ℝ → ℝ} {cap B : ℝ} (hp : PressureDatum.Admissible g a cap) (hB : 2 ≤ B) (hg : ∀ y ≤ 0, g y = B ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) : ∃ (δ : ℝ) (σ : ℝ), 0 < δ ∧ 0 < σ ∧ (∀ η ∈ Set.Icc (-1) 1, |Z h j (PressureDatum.pressure g a) η| ≤ δ → 99 / 100 < chi h j σ η) ∧ ContDiff ℝ (↑⊤) (chi h j σ)

End-to-end real cutoff construction from the actual weighted pressure integral and its ideal prefix, rather than assumed pressure conclusions.

theorem NavierStokes.NaturalAxisData.ideal_prefix_root_positive {h j : ℝ} (p : SmallParameters h j) {g a : ℝ → ℝ} {cap B : ℝ} (hp : PressureDatum.Admissible g a cap) (hB : 2 ≤ B) (hg : ∀ y ≤ 0, g y = B ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) : ∃ η₀ ∈ Set.Ioo (-j / 4) (-j / 5), H h j η₀ = 0 ∧ j / 5 < Z h j (PressureDatum.pressure g a) η₀ ∧ ∀ η ∈ Set.Icc (-1) 1, H h j η = 0 → η = η₀

Uniform analytic input for the natural-axis coefficient space

The hypotheses concern one common complex neighborhood of the entire real parameter interval. Cauchy's integral formula supplies bounds on actual derivatives; the derivative bounds are not hypotheses of the construction.

def NavierStokes.AnalyticCoefficientBounds.closedTube (I : AxisCoefficientSpace.Window) (ρ : ℝ) : Set ℂ

The closed radius-ρ neighborhood of the real parameter interval.

Equations

• NavierStokes.AnalyticCoefficientBounds.closedTube I ρ = {z : ℂ | ∃ x ∈ I.interval, dist z ↑x ≤ ρ}

theorem NavierStokes.AnalyticCoefficientBounds.closedBall_subset_closedTube (I : AxisCoefficientSpace.Window) (ρ : ℝ) {x : ℝ} (hx : x ∈ I.interval) : Metric.closedBall (↑x) ρ ⊆ closedTube I ρ

theorem NavierStokes.AnalyticCoefficientBounds.real_mem_closedTube (I : AxisCoefficientSpace.Window) {ρ : ℝ} (hρ : 0 ≤ ρ) {x : ℝ} (hx : x ∈ I.interval) : ↑x ∈ closedTube I ρ

structure NavierStokes.AnalyticCoefficientBounds.UnitHolomorphic (I : AxisCoefficientSpace.Window) (ρ : ℝ) (f : ℂ → ℂ) : Prop

A uniform complex value bound, with holomorphy on a neighborhood of the same closed tube. No derivative estimates occur in this predicate.

• analytic : AnalyticOnNhd ℂ f (closedTube I ρ)
• norm_le_one (z : ℂ) : z ∈ closedTube I ρ → ‖f z‖ ≤ 1

theorem NavierStokes.AnalyticCoefficientBounds.norm_cauchyCoefficient_le {f : ℂ → ℂ} {c : ℂ} {ρ : ℝ} (hρ : 0 < ρ) (hb : ∀ z ∈ Metric.sphere c ρ, ‖f z‖ ≤ 1) (m : ℕ) : ‖(cauchyPowerSeries f c ρ m) fun (x : Fin m) => 1‖ ≤ ρ⁻¹ ^ m

Bound one Cauchy coefficient directly by its circle integral.

theorem NavierStokes.AnalyticCoefficientBounds.norm_iteratedDeriv_le {f : ℂ → ℂ} {c : ℂ} {ρ : ℝ} (hρ : 0 < ρ) (hf : DifferentiableOn ℂ f (Metric.closedBall c ρ)) (hb : ∀ z ∈ Metric.sphere c ρ, ‖f z‖ ≤ 1) (m : ℕ) : ‖iteratedDeriv m f c‖ ≤ ↑m.factorial * ρ⁻¹ ^ m

Cauchy's estimate for every genuine complex derivative, derived from the circle-integral coefficients and the factorial derivative identity.

noncomputable def NavierStokes.AnalyticCoefficientBounds.realJet (f : ℂ → ℂ) (m : ℕ) (x : ℝ) : ℝ

The real part of a genuine complex jet, evaluated on the real axis.

Equations

• NavierStokes.AnalyticCoefficientBounds.realJet f m x = (iteratedDeriv m f ↑x).re

theorem NavierStokes.AnalyticCoefficientBounds.hasDerivAt_realJet {f : ℂ → ℂ} {x : ℝ} (hf : AnalyticAt ℂ f ↑x) (m : ℕ) : HasDerivAt (realJet f m) (realJet f (m + 1) x) x

theorem NavierStokes.AnalyticCoefficientBounds.iteratedDeriv_realPart {f : ℂ → ℂ} {x : ℝ} (hf : AnalyticAt ℂ f ↑x) (m : ℕ) : iteratedDeriv m (fun (t : ℝ) => (f ↑t).re) x = realJet f m x

The real-axis jets really are the ordinary iterated real derivatives.

theorem NavierStokes.AnalyticCoefficientBounds.UnitHolomorphic.abs_realJet_le {I : AxisCoefficientSpace.Window} {ρ : ℝ} {f : ℂ → ℂ} (hf : UnitHolomorphic I ρ f) (hρ : 0 < ρ) (m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : |realJet f m x| ≤ ↑m.factorial * ρ⁻¹ ^ m

theorem NavierStokes.AnalyticCoefficientBounds.UnitHolomorphic.abs_iteratedDeriv_le {I : AxisCoefficientSpace.Window} {ρ : ℝ} {f : ℂ → ℂ} (hf : UnitHolomorphic I ρ f) (hρ : 0 < ρ) (m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : |iteratedDeriv m (fun (t : ℝ) => (f ↑t).re) x| ≤ ↑m.factorial * ρ⁻¹ ^ m

noncomputable def NavierStokes.AnalyticCoefficientBounds.radiusLoss (q : ℝ) : ℝ

The loss in passing from a complex radius to the coefficient radius.

Equations

• NavierStokes.AnalyticCoefficientBounds.radiusLoss q = ∑' (m : ℕ), (↑m + 1) ^ 2 * q ^ m

theorem NavierStokes.AnalyticCoefficientBounds.summable_radiusLoss {q : ℝ} (hq : 0 ≤ q) (hq1 : q < 1) : Summable fun (m : ℕ) => (↑m + 1) ^ 2 * q ^ m

theorem NavierStokes.AnalyticCoefficientBounds.radiusLoss_nonneg {q : ℝ} (hq : 0 ≤ q) : 0 ≤ radiusLoss q

theorem NavierStokes.AnalyticCoefficientBounds.term_le_radiusLoss {q : ℝ} (hq : 0 ≤ q) (hq1 : q < 1) (m : ℕ) : (↑m + 1) ^ 2 * q ^ m ≤ radiusLoss q

theorem NavierStokes.AnalyticCoefficientBounds.cauchy_bound_le_weight {ε ρ : ℝ} (hε : 0 < ε) (hερ : ε < ρ) (m : ℕ) : ↑m.factorial * ρ⁻¹ ^ m ≤ radiusLoss (ε / ρ) * AxisWeightEstimates.weight ε 0 m

The Cauchy bound fits the exact degree-zero manuscript weight.

noncomputable def NavierStokes.AnalyticCoefficientBounds.degreeZeroJet (f : ℂ → ℂ) (n m : ℕ) (x : ℝ) : ℝ

A coefficient family concentrated at radial degree zero.

Equations

• NavierStokes.AnalyticCoefficientBounds.degreeZeroJet f n m x = if n = 0 then NavierStokes.AnalyticCoefficientBounds.realJet f m x else 0

theorem NavierStokes.AnalyticCoefficientBounds.UnitHolomorphic.degreeZeroJet_continuous {I : AxisCoefficientSpace.Window} {ρ : ℝ} {f : ℂ → ℂ} (hf : UnitHolomorphic I ρ f) (hρ : 0 < ρ) (n m : ℕ) : ContinuousOn (degreeZeroJet f n m) I.interval

theorem NavierStokes.AnalyticCoefficientBounds.UnitHolomorphic.degreeZeroJet_hasDerivWithinAt {I : AxisCoefficientSpace.Window} {ρ : ℝ} {f : ℂ → ℂ} (hf : UnitHolomorphic I ρ f) (hρ : 0 < ρ) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : HasDerivWithinAt (degreeZeroJet f n m) (degreeZeroJet f n (m + 1) x) I.interval x

theorem NavierStokes.AnalyticCoefficientBounds.UnitHolomorphic.degreeZeroJet_bound {I : AxisCoefficientSpace.Window} {ε ρ : ℝ} {f : ℂ → ℂ} (hf : UnitHolomorphic I ρ f) (hε : 0 < ε) (hερ : ε < ρ) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : |degreeZeroJet f n m x| ≤ radiusLoss (ε / ρ) * AxisWeightEstimates.weight ε n m

noncomputable def NavierStokes.AnalyticCoefficientBounds.UnitHolomorphic.toAxisSpace {I : AxisCoefficientSpace.Window} {ε ρ : ℝ} {f : ℂ → ℂ} (hf : UnitHolomorphic I ρ f) (hε : 0 < ε) (hερ : ε < ρ) : ↥(AxisCoefficientSpace.AxisSpace I ε)

A bounded holomorphic function supplies an actual degree-zero element of the compatible coefficient Banach space.

Equations

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

theorem NavierStokes.AnalyticCoefficientBounds.UnitHolomorphic.norm_toAxisSpace_le {I : AxisCoefficientSpace.Window} {ε ρ : ℝ} {f : ℂ → ℂ} (hf : UnitHolomorphic I ρ f) (hε : 0 < ε) (hερ : ε < ρ) : ‖hf.toAxisSpace hε hερ‖ ≤ radiusLoss (ε / ρ)

theorem NavierStokes.AnalyticCoefficientBounds.UnitHolomorphic.coefficient_toAxisSpace {I : AxisCoefficientSpace.Window} {ε ρ : ℝ} {f : ℂ → ℂ} (hf : UnitHolomorphic I ρ f) (hε : 0 < ε) (hερ : ε < ρ) (n : ℕ) {x : ℝ} (hx : x ∈ I.interval) : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) (hf.toAxisSpace hε hερ) n x = if n = 0 then (f ↑x).re else 0

theorem NavierStokes.AnalyticCoefficientBounds.UnitHolomorphic.jet_toAxisSpace {I : AxisCoefficientSpace.Window} {ε ρ : ℝ} {f : ℂ → ℂ} (hf : UnitHolomorphic I ρ f) (hε : 0 < ε) (hερ : ε < ρ) (n m : ℕ) {x : ℝ} (hx : x ∈ I.interval) : AxisCoefficientSpace.jet I (AxisWeightEstimates.weight ε) (↑(hf.toAxisSpace hε hερ)) n m x = if n = 0 then iteratedDeriv m (fun (t : ℝ) => (f ↑t).re) x else 0

noncomputable def NavierStokes.AnalyticCoefficientBounds.normalizedExp (F : ℂ → ℂ) (Λ C : ℝ) (z : ℂ) : ℂ

The normalized axis exponential, defined on the whole complex plane but bounded using the common complex neighborhood.

Equations

• NavierStokes.AnalyticCoefficientBounds.normalizedExp F Λ C z = Complex.exp (↑Λ * F z) / ↑C

theorem NavierStokes.AnalyticCoefficientBounds.normalizedExp_unitHolomorphic {I : AxisCoefficientSpace.Window} {ρ Λ C M : ℝ} {F : ℂ → ℂ} (hF : AnalyticOnNhd ℂ F (closedTube I ρ)) (hM : ∀ z ∈ closedTube I ρ, (F z).re ≤ M) (hΛ : 0 ≤ Λ) (hC : Real.exp (Λ * M) ≤ C) : UnitHolomorphic I ρ (normalizedExp F Λ C)

One lower bound on C supplies all derivative bounds simultaneously. The upper bound on Re F is imposed on the complex tube, not just its real axis.

noncomputable def NavierStokes.AnalyticCoefficientBounds.realPartSup (F : ℂ → ℂ) (K : Set ℂ) : ℝ

Supremum over a fixed compact complex set, used for the literal normalization threshold exp(Λ sup Re F).

Equations

• NavierStokes.AnalyticCoefficientBounds.realPartSup F K = sSup ((fun (z : ℂ) => (F z).re) '' K)

theorem NavierStokes.AnalyticCoefficientBounds.re_le_realPartSup {F : ℂ → ℂ} {K : Set ℂ} (hK : IsCompact K) (hF : ContinuousOn F K) {z : ℂ} (hz : z ∈ K) : (F z).re ≤ realPartSup F K

theorem NavierStokes.AnalyticCoefficientBounds.normalizedExp_unitHolomorphic_of_compact {I : AxisCoefficientSpace.Window} {ρ Λ C : ℝ} {F : ℂ → ℂ} {K : Set ℂ} (hK : IsCompact K) (hF : AnalyticOnNhd ℂ F K) (hcover : ∀ x ∈ I.interval, Metric.closedBall (↑x) ρ ⊆ K) (hΛ : 0 ≤ Λ) (hC : Real.exp (Λ * realPartSup F K) ≤ C) : UnitHolomorphic I ρ (normalizedExp F Λ C)

A compact wider complex neighborhood is enough: every radius-ρ closed disc about a real parameter must lie inside it.

theorem NavierStokes.AnalyticCoefficientBounds.normalizedExp_re_of_real {F : ℂ → ℂ} {Λ C x : ℝ} (hreal : (F ↑x).im = 0) : (normalizedExp F Λ C ↑x).re = Real.exp (Λ * (F ↑x).re) / C

theorem NavierStokes.AnalyticCoefficientBounds.uniform_normalizedExp_axisData {I : AxisCoefficientSpace.Window} {ε ρ M : ℝ} {F : ℂ → ℂ} (hε : 0 < ε) (hερ : ε < ρ) (hF : AnalyticOnNhd ℂ F (closedTube I ρ)) (hM : ∀ z ∈ closedTube I ρ, (F z).re ≤ M) (hreal : ∀ x ∈ I.interval, (F ↑x).im = 0) (Λ : ℝ) : 0 ≤ Λ → ∀ (C : ℝ), Real.exp (Λ * M) ≤ C → ∃ (a : ↥(AxisCoefficientSpace.AxisSpace I ε)), ‖a‖ ≤ radiusLoss (ε / ρ) ∧ (∀ x ∈ I.interval, AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) a 0 x = Real.exp (Λ * (F ↑x).re) / C) ∧ ∀ (n : ℕ), n ≠ 0 → ∀ x ∈ I.interval, AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) a n x = 0

Uniform degree-zero data for every admissible pair (Λ,C). The element is constructed from compatible actual derivatives, and its norm bound depends only on the two radii.

theorem NavierStokes.AnalyticCoefficientBounds.uniform_normalizedExp_axisData_of_compact {I : AxisCoefficientSpace.Window} {ε ρ : ℝ} {F : ℂ → ℂ} {K : Set ℂ} (hε : 0 < ε) (hερ : ε < ρ) (hK : IsCompact K) (hF : AnalyticOnNhd ℂ F K) (hcover : ∀ x ∈ I.interval, Metric.closedBall (↑x) ρ ⊆ K) (hreal : ∀ x ∈ I.interval, (F ↑x).im = 0) (Λ : ℝ) : 0 ≤ Λ → ∀ (C : ℝ), Real.exp (Λ * realPartSup F K) ≤ C → ∃ (a : ↥(AxisCoefficientSpace.AxisSpace I ε)), ‖a‖ ≤ radiusLoss (ε / ρ) ∧ (∀ x ∈ I.interval, AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) a 0 x = Real.exp (Λ * (F ↑x).re) / C) ∧ ∀ (n : ℕ), n ≠ 0 → ∀ x ∈ I.interval, AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) a n x = 0

The compact-neighborhood form uses exactly C ≥ exp(Λ sup Re F). The order is: fix I, ε, ρ, K, F, then choose Λ and any sufficiently large C; the coefficient norm threshold remains the same.

An actual holomorphic primitive on a convex open set

The primitive is the radial segment integral. Its derivative is proved by differentiating under a uniformly dominated integral on a compact local product, then applying the real fundamental theorem of calculus along the segment. No disk containing the entire domain and no assumed primitive are required.

noncomputable def NavierStokes.AnalyticPrimitive.primitive (g : ℂ → ℂ) (z : ℂ) : ℂ

Integration along the straight segment from zero to z.

Equations

• NavierStokes.AnalyticPrimitive.primitive g z = z * ∫ (t : ℝ) in 0..1, g (↑t * z)

@[simp]

theorem NavierStokes.AnalyticPrimitive.primitive_zero (g : ℂ → ℂ) : primitive g 0 = 0

theorem NavierStokes.AnalyticPrimitive.primitive_eq_integral (g : ℂ → ℂ) (z : ℂ) : primitive g z = ∫ (t : ℝ) in 0..1, z * g (↑t * z)

theorem NavierStokes.AnalyticPrimitive.segment_mem {U : Set ℂ} (hU : Convex ℝ U) (h0 : 0 ∈ U) {z : ℂ} (hz : z ∈ U) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ↑t * z ∈ U

theorem NavierStokes.AnalyticPrimitive.continuousOn_segment {U : Set ℂ} (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : ContinuousOn g U) {z : ℂ} (hz : z ∈ U) : ContinuousOn (fun (t : ℝ) => g (↑t * z)) (Set.Icc 0 1)

noncomputable def NavierStokes.AnalyticPrimitive.integrandDerivative (g : ℂ → ℂ) (z : ℂ) (t : ℝ) : ℂ

The complex derivative of the parameter-dependent integrand.

Equations

• NavierStokes.AnalyticPrimitive.integrandDerivative g z t = g (↑t * z) + ↑t * z * deriv g (↑t * z)

theorem NavierStokes.AnalyticPrimitive.integrand_hasDerivAt {U : Set ℂ} (ho : IsOpen U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) {z : ℂ} {t : ℝ} (htz : ↑t * z ∈ U) : HasDerivAt (fun (w : ℂ) => w * g (↑t * w)) (integrandDerivative g z t) z

theorem NavierStokes.AnalyticPrimitive.integrandDerivative_continuousOn_segment {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) {z : ℂ} (hz : z ∈ U) : ContinuousOn (integrandDerivative g z) (Set.Icc 0 1)

theorem NavierStokes.AnalyticPrimitive.segment_product_hasDerivAt {U : Set ℂ} (ho : IsOpen U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) {z : ℂ} {t : ℝ} (htz : ↑t * z ∈ U) : HasDerivAt (fun (s : ℝ) => ↑s * g (↑s * z)) (integrandDerivative g z t) t

The same derivative integrand is the real derivative of t*g(t*z).

theorem NavierStokes.AnalyticPrimitive.integral_integrandDerivative {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) {z : ℂ} (hz : z ∈ U) : ∫ (t : ℝ) in 0..1, integrandDerivative g z t = g z

theorem NavierStokes.AnalyticPrimitive.hasDerivAt_primitive {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) {z : ℂ} (hz : z ∈ U) : HasDerivAt (primitive g) (g z) z

An actual holomorphic primitive on any convex open neighborhood of zero.

theorem NavierStokes.AnalyticPrimitive.differentiableOn_primitive {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) : DifferentiableOn ℂ (primitive g) U

theorem NavierStokes.AnalyticPrimitive.analyticOnNhd_primitive {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) : AnalyticOnNhd ℂ (primitive g) U

theorem NavierStokes.AnalyticPrimitive.primitive_im_eq_zero {U : Set ℂ} (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hreal : ∀ (x : ℝ), ↑x ∈ U → (g ↑x).im = 0) {x : ℝ} (hx : ↑x ∈ U) : (primitive g ↑x).im = 0

Reality is local to the real points of the given convex domain.

theorem NavierStokes.AnalyticPrimitive.primitive_ofReal (g : ℂ → ℂ) (f : ℝ → ℝ) (hreal : ∀ (x : ℝ), g ↑x = ↑(f x)) (x : ℝ) : primitive g ↑x = ↑(x * ∫ (t : ℝ) in 0..1, f (t * x))

If the integrand extends a real function, its segment primitive extends the corresponding real segment integral exactly.

theorem NavierStokes.AnalyticPrimitive.hasDerivAt_real_primitive {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) {x : ℝ} (hx : ↑x ∈ U) : HasDerivAt (fun (y : ℝ) => (primitive g ↑y).re) (g ↑x).re x

noncomputable def NavierStokes.AnalyticPrimitive.amplitude (g : ℂ → ℂ) (Λ C z : ℂ) : ℂ

The normalized exponential built from the actual segment primitive.

Equations

• NavierStokes.AnalyticPrimitive.amplitude g Λ C z = Complex.exp (Λ * NavierStokes.AnalyticPrimitive.primitive g z) / C

@[simp]

theorem NavierStokes.AnalyticPrimitive.amplitude_zero (g : ℂ → ℂ) (Λ C : ℂ) : amplitude g Λ C 0 = 1 / C

theorem NavierStokes.AnalyticPrimitive.amplitude_ne_zero (g : ℂ → ℂ) (Λ : ℂ) {C : ℂ} (hC : C ≠ 0) (z : ℂ) : amplitude g Λ C z ≠ 0

theorem NavierStokes.AnalyticPrimitive.hasDerivAt_amplitude {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) (Λ C : ℂ) {z : ℂ} (hz : z ∈ U) : HasDerivAt (amplitude g Λ C) (Λ * g z * amplitude g Λ C z) z

Normalization is constant in the spatial variable, so the differential equation is valid for any normalization scalar.

theorem NavierStokes.AnalyticPrimitive.analyticOnNhd_amplitude {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) (Λ C : ℂ) : AnalyticOnNhd ℂ (amplitude g Λ C) U

theorem NavierStokes.AnalyticPrimitive.amplitude_log_derivative {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) (Λ : ℂ) {C : ℂ} (hC : C ≠ 0) {z : ℂ} (hz : z ∈ U) : deriv (amplitude g Λ C) z / amplitude g Λ C z = Λ * g z

The actual logarithmic derivative of the nonvanishing normalized exponential is the prescribed scaled holomorphic gradient.

theorem NavierStokes.AnalyticPrimitive.amplitude_ofReal (g : ℂ → ℂ) (f : ℝ → ℝ) (hreal : ∀ (x : ℝ), g ↑x = ↑(f x)) (Λ C x : ℝ) : amplitude g ↑Λ ↑C ↑x = ↑(Real.exp (Λ * (x * ∫ (t : ℝ) in 0..1, f (t * x))) / C)

theorem NavierStokes.AnalyticPrimitive.amplitude_real_pos (g : ℂ → ℂ) (f : ℝ → ℝ) (hreal : ∀ (x : ℝ), g ↑x = ↑(f x)) (Λ : ℝ) {C : ℝ} (hC : 0 < C) (x : ℝ) : 0 < (amplitude g ↑Λ ↑C ↑x).re

theorem NavierStokes.AnalyticPrimitive.hasDerivAt_real_amplitude {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) (f : ℝ → ℝ) (hreal : ∀ (x : ℝ), g ↑x = ↑(f x)) (Λ C : ℝ) {x : ℝ} (hx : ↑x ∈ U) : HasDerivAt (fun (y : ℝ) => (amplitude g ↑Λ ↑C ↑y).re) (Λ * f x * (amplitude g ↑Λ ↑C ↑x).re) x

theorem NavierStokes.AnalyticPrimitive.real_amplitude_log_derivative {U : Set ℂ} (ho : IsOpen U) (hU : Convex ℝ U) (h0 : 0 ∈ U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) (f : ℝ → ℝ) (hreal : ∀ (x : ℝ), g ↑x = ↑(f x)) (Λ : ℝ) {C : ℝ} (hC : 0 < C) {x : ℝ} (hx : ↑x ∈ U) : deriv (fun (y : ℝ) => (amplitude g ↑Λ ↑C ↑y).re) x / (amplitude g ↑Λ ↑C ↑x).re = Λ * f x

noncomputable def NavierStokes.NaturalAxisCoefficients.window : AxisCoefficientSpace.Window

A fixed, slightly enlarged real parameter interval.

Equations

• NavierStokes.NaturalAxisCoefficients.window = { left := -11 / 10, right := 11 / 10, nondegenerate := NavierStokes.NaturalAxisCoefficients.window._proof_1 }

theorem NavierStokes.NaturalAxisCoefficients.original_interval_interior : Set.Icc (-1) 1 ⊆ Set.Ioo window.left window.right

def NavierStokes.NaturalAxisCoefficients.complexD (z : ℂ) : ℂ

Complex D, given by 1 - z ^ 2.

Equations

• NavierStokes.NaturalAxisCoefficients.complexD z = 1 - z ^ 2

def NavierStokes.NaturalAxisCoefficients.complexL (h : ℝ) (z : ℂ) : ℂ

Complex L, given by 1 - 2 * (h : ℂ) * z ^ 2.

Equations

• NavierStokes.NaturalAxisCoefficients.complexL h z = 1 - 2 * ↑h * z ^ 2

def NavierStokes.NaturalAxisCoefficients.complexU (j : ℝ) (z : ℂ) : ℂ

Complex U, given by 4 * z + (j : ℂ).

Equations

• NavierStokes.NaturalAxisCoefficients.complexU j z = 4 * z + ↑j

noncomputable def NavierStokes.NaturalAxisCoefficients.complexH (h j : ℝ) (z : ℂ) : ℂ

Complex H, given by (NaturalAxisData.D h : ℂ) * z + complexD z * complexU j z.

Equations

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

noncomputable def NavierStokes.NaturalAxisCoefficients.complexW (h j : ℝ) (z : ℂ) : ℂ

Complex W, given by 1 - 4 * complexD z - 2 * (NaturalAxisData.D h : ℂ) * z * complexU j z.

Equations

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

noncomputable def NavierStokes.NaturalAxisCoefficients.denominator (h j σ : ℝ) (z : ℂ) : ℂ

Denominator, given by complexH h j z ^ 2 + (σ : ℂ) ^ 2.

Equations

• NavierStokes.NaturalAxisCoefficients.denominator h j σ z = NavierStokes.NaturalAxisCoefficients.complexH h j z ^ 2 + ↑σ ^ 2

noncomputable def NavierStokes.NaturalAxisCoefficients.complexZ (h j : ℝ) (P : ℂ → ℂ) (z : ℂ) : ℂ

Complex Z as an element of ℂ.

Equations

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

noncomputable def NavierStokes.NaturalAxisCoefficients.complexChi (h j σ : ℝ) (z : ℂ) : ℂ

Complex chi, given by complexH h j z ^ 2 / denominator h j σ z.

Equations

• NavierStokes.NaturalAxisCoefficients.complexChi h j σ z = NavierStokes.NaturalAxisCoefficients.complexH h j z ^ 2 / NavierStokes.NaturalAxisCoefficients.denominator h j σ z

noncomputable def NavierStokes.NaturalAxisCoefficients.complexGradient (h j σ : ℝ) (z : ℂ) : ℂ

Complex gradient, given by -complexL h z * complexH h j z / denominator h j σ z.

Equations

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

noncomputable def NavierStokes.NaturalAxisCoefficients.realGradient (h j σ x : ℝ) : ℝ

Real gradient, given by -NaturalAxisData.L h x * NaturalAxisData.H h j x / (NaturalAxisData.H h j x ^ 2 + σ ^ 2).

Equations

• NavierStokes.NaturalAxisCoefficients.realGradient h j σ x = -NavierStokes.NaturalAxisData.L h x * NavierStokes.NaturalAxisData.H h j x / (NavierStokes.NaturalAxisData.H h j x ^ 2 + σ ^ 2)

@[simp]

theorem NavierStokes.NaturalAxisCoefficients.complexL_ofReal (h x : ℝ) : complexL h ↑x = ↑(NaturalAxisData.L h x)

@[simp]

theorem NavierStokes.NaturalAxisCoefficients.complexH_ofReal (h j x : ℝ) : complexH h j ↑x = ↑(NaturalAxisData.H h j x)

@[simp]

theorem NavierStokes.NaturalAxisCoefficients.denominator_ofReal (h j σ x : ℝ) : denominator h j σ ↑x = ↑(NaturalAxisData.H h j x ^ 2 + σ ^ 2)

@[simp]

theorem NavierStokes.NaturalAxisCoefficients.complexGradient_ofReal (h j σ x : ℝ) : complexGradient h j σ ↑x = ↑(realGradient h j σ x)

theorem NavierStokes.NaturalAxisCoefficients.L_pos_on_window {h j : ℝ} (hp : NaturalAxisData.SmallParameters h j) {x : ℝ} (hx : x ∈ window.interval) : 0 < NaturalAxisData.L h x

theorem NavierStokes.NaturalAxisCoefficients.denominator_ne_zero_on_real (h j : ℝ) {σ : ℝ} (hσ : 0 < σ) (x : ℝ) : denominator h j σ ↑x ≠ 0

def NavierStokes.NaturalAxisCoefficients.regularSet (h j σ : ℝ) : Set ℂ

The open region where all fixed rational expressions and pressure are analytic.

Equations

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

theorem NavierStokes.NaturalAxisCoefficients.regularSet_open (h j σ : ℝ) : IsOpen (regularSet h j σ)

theorem NavierStokes.NaturalAxisCoefficients.real_mem_regularSet {h j σ : ℝ} (hp : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {x : ℝ} (hx : x ∈ window.interval) : ↑x ∈ regularSet h j σ

theorem NavierStokes.NaturalAxisCoefficients.complexGradient_analytic (h j σ : ℝ) : AnalyticOnNhd ℂ (complexGradient h j σ) (regularSet h j σ)

inductive NavierStokes.NaturalAxisCoefficients.Field : Type

Field data for natural axis coefficients.

• one : Field
• eta : Field
• d : Field
• inverseL : Field
• uStar : Field
• uStarEta : Field
• wStar : Field
• hStar : Field
• zStar : Field
• chi : Field
• gradient : Field

@[instance_reducible]

instance NavierStokes.NaturalAxisCoefficients.instDecidableEqField : DecidableEq Field

Equations

• NavierStokes.NaturalAxisCoefficients.instDecidableEqField x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance NavierStokes.NaturalAxisCoefficients.instFintypeField : Fintype Field

Equations

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

noncomputable def NavierStokes.NaturalAxisCoefficients.complexField (h j σ : ℝ) (P : ℂ → ℂ) : Field → ℂ → ℂ

Complex field used in natural axis coefficients.

Equations

• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.one = fun (x : ℂ) => 1
• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.eta = fun (z : ℂ) => z
• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.d = NavierStokes.NaturalAxisCoefficients.complexD
• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.inverseL = fun (z : ℂ) => (NavierStokes.NaturalAxisCoefficients.complexL h z)⁻¹
• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.uStar = NavierStokes.NaturalAxisCoefficients.complexU j
• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.uStarEta = fun (x : ℂ) => 4
• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.wStar = NavierStokes.NaturalAxisCoefficients.complexW h j
• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.hStar = NavierStokes.NaturalAxisCoefficients.complexH h j
• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.zStar = NavierStokes.NaturalAxisCoefficients.complexZ h j P
• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.chi = NavierStokes.NaturalAxisCoefficients.complexChi h j σ
• NavierStokes.NaturalAxisCoefficients.complexField h j σ P NavierStokes.NaturalAxisCoefficients.Field.gradient = NavierStokes.NaturalAxisCoefficients.complexGradient h j σ

noncomputable def NavierStokes.NaturalAxisCoefficients.realField (h j σ : ℝ) (P : ℝ → ℝ) : Field → ℝ → ℝ

Real field used in natural axis coefficients.

Equations

• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.one = fun (x : ℝ) => 1
• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.eta = fun (x : ℝ) => x
• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.d = NavierStokes.NaturalAxisData.d
• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.inverseL = fun (x : ℝ) => (NavierStokes.NaturalAxisData.L h x)⁻¹
• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.uStar = NavierStokes.NaturalAxisData.U j
• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.uStarEta = fun (x : ℝ) => 4
• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.wStar = NavierStokes.NaturalAxisData.W h j
• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.hStar = NavierStokes.NaturalAxisData.H h j
• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.zStar = NavierStokes.NaturalAxisData.Z h j P
• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.chi = NavierStokes.NaturalAxisData.chi h j σ
• NavierStokes.NaturalAxisCoefficients.realField h j σ P NavierStokes.NaturalAxisCoefficients.Field.gradient = NavierStokes.NaturalAxisCoefficients.realGradient h j σ

theorem NavierStokes.NaturalAxisCoefficients.deriv_complexPressure_ofReal {g a : ℝ → ℝ} {cap : ℝ} (hp : PressureDatum.Admissible g a cap) (x : ℝ) : deriv (PressureDatum.complexPressure g a) ↑x = ↑(deriv (PressureDatum.pressure g a) x)

theorem NavierStokes.NaturalAxisCoefficients.complexField_ofReal {g a : ℝ → ℝ} {cap : ℝ} (hp : PressureDatum.Admissible g a cap) (h j σ : ℝ) (k : Field) (x : ℝ) : complexField h j σ (PressureDatum.complexPressure g a) k ↑x = ↑(realField h j σ (PressureDatum.pressure g a) k x)

theorem NavierStokes.NaturalAxisCoefficients.complexField_analytic {g a : ℝ → ℝ} {cap : ℝ} (hp : PressureDatum.Admissible g a cap) (h j σ : ℝ) (k : Field) : AnalyticOnNhd ℂ (complexField h j σ (PressureDatum.complexPressure g a) k) (regularSet h j σ)

theorem NavierStokes.NaturalAxisCoefficients.exists_common_neighborhood {h j σ : ℝ} (hp : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ∃ (ρ : ℝ), 0 < ρ ∧ ∃ (K : Set ℂ), IsCompact K ∧ (∀ x ∈ window.interval, Metric.closedBall (↑x) ρ ⊆ K) ∧ K ⊆ regularSet h j σ

One compact complex neighborhood for the whole finite family.

theorem NavierStokes.NaturalAxisCoefficients.exists_convex_common_neighborhood {h j σ : ℝ} (hp : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ∃ (ρ : ℝ), 0 < ρ ∧ ∃ (U : Set ℂ) (K : Set ℂ), IsOpen U ∧ Convex ℝ U ∧ 0 ∈ U ∧ IsCompact K ∧ (∀ x ∈ window.interval, Metric.closedBall (↑x) ρ ⊆ K) ∧ K ⊆ U ∧ U ⊆ regularSet h j σ

A convex open outer neighborhood and compact inner neighborhood. The inner radius can be used for both the fixed fields and an analytic primitive.

theorem NavierStokes.NaturalAxisCoefficients.finite_family_bound {ι : Type u_1} [Finite ι] {K : Set ℂ} (hK : IsCompact K) (f : ι → ℂ → ℂ) (hf : ∀ (i : ι), ContinuousOn (f i) K) : ∃ (B : ℝ), 0 < B ∧ ∀ (i : ι), ∀ z ∈ K, ‖f i z‖ ≤ B

Compactness and finiteness give one common value bound for all inputs.

theorem NavierStokes.NaturalAxisCoefficients.unitHolomorphic_of_bound {I : AxisCoefficientSpace.Window} {ρ B : ℝ} {f : ℂ → ℂ} (hB : 0 < B) (hf : AnalyticOnNhd ℂ f (AnalyticCoefficientBounds.closedTube I ρ)) (hb : ∀ z ∈ AnalyticCoefficientBounds.closedTube I ρ, ‖f z‖ ≤ B) : AnalyticCoefficientBounds.UnitHolomorphic I ρ fun (z : ℂ) => f z / ↑B

theorem NavierStokes.NaturalAxisCoefficients.coefficient_smul (I : AxisCoefficientSpace.Window) (ε c : ℝ) (a : ↥(AxisCoefficientSpace.AxisSpace I ε)) (n : ℕ) (x : ℝ) : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) (c • a) n x = c * AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) a n x

noncomputable def NavierStokes.NaturalAxisCoefficients.boundedAxisElement {I : AxisCoefficientSpace.Window} {ε ρ B : ℝ} {f : ℂ → ℂ} (hε : 0 < ε) (hερ : ε < ρ) (hB : 0 < B) (hf : AnalyticOnNhd ℂ f (AnalyticCoefficientBounds.closedTube I ρ)) (hb : ∀ z ∈ AnalyticCoefficientBounds.closedTube I ρ, ‖f z‖ ≤ B) : ↥(AxisCoefficientSpace.AxisSpace I ε)

An arbitrary finite complex bound is reduced to the unit-bound Cauchy constructor.

Equations

• NavierStokes.NaturalAxisCoefficients.boundedAxisElement hε hερ hB hf hb = B • ⋯.toAxisSpace hε hερ

theorem NavierStokes.NaturalAxisCoefficients.boundedAxisElement_norm {I : AxisCoefficientSpace.Window} {ε ρ B : ℝ} {f : ℂ → ℂ} (hε : 0 < ε) (hερ : ε < ρ) (hB : 0 < B) (hf : AnalyticOnNhd ℂ f (AnalyticCoefficientBounds.closedTube I ρ)) (hb : ∀ z ∈ AnalyticCoefficientBounds.closedTube I ρ, ‖f z‖ ≤ B) : ‖boundedAxisElement hε hερ hB hf hb‖ ≤ B * AnalyticCoefficientBounds.radiusLoss (ε / ρ)

theorem NavierStokes.NaturalAxisCoefficients.boundedAxisElement_coefficient {I : AxisCoefficientSpace.Window} {ε ρ B : ℝ} {f : ℂ → ℂ} (hε : 0 < ε) (hερ : ε < ρ) (hB : 0 < B) (hf : AnalyticOnNhd ℂ f (AnalyticCoefficientBounds.closedTube I ρ)) (hb : ∀ z ∈ AnalyticCoefficientBounds.closedTube I ρ, ‖f z‖ ≤ B) (n : ℕ) {x : ℝ} (hx : x ∈ I.interval) : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) (boundedAxisElement hε hερ hB hf hb) n x = if n = 0 then (f ↑x).re else 0

structure NavierStokes.NaturalAxisCoefficients.CoefficientFamily (h j σ : ℝ) (P : ℝ → ℝ) : Type

A finite family of actual degree-zero fields, all using the same positive parameter radius and the same finite norm bound.

• epsilon : ℝ

  Epsilon of CoefficientFamily, of type ℝ.

• epsilon_pos : 0 < self.epsilon
• elements : Field → ↥(AxisCoefficientSpace.AxisSpace window self.epsilon)

  Elements of CoefficientFamily, of type Field → AxisSpace window epsilon.

• bound : ℝ

  Bound of CoefficientFamily, of type ℝ.

• bound_nonneg : 0 ≤ self.bound
• norm_le (k : Field) : ‖self.elements k‖ ≤ self.bound
• coefficient_eq (k : Field) (n : ℕ) (x : ℝ) : x ∈ window.interval → AxisCoefficientSpace.coefficient window (AxisWeightEstimates.weight self.epsilon) (self.elements k) n x = if n = 0 then realField h j σ P k x else 0

theorem NavierStokes.NaturalAxisCoefficients.exists_coefficientFamily_on_neighborhood {h j σ ρ : ℝ} {g a : ℝ → ℝ} {cap : ℝ} (hp : PressureDatum.Admissible g a cap) (hρ : 0 < ρ) {K : Set ℂ} (hK : IsCompact K) (hcover : ∀ x ∈ window.interval, Metric.closedBall (↑x) ρ ⊆ K) (hKU : K ⊆ regularSet h j σ) : ∃ (v : CoefficientFamily h j σ (PressureDatum.pressure g a)), v.epsilon = ρ / 2

theorem NavierStokes.NaturalAxisCoefficients.exists_coefficientFamily {h j σ : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {g a : ℝ → ℝ} {cap : ℝ} (hp : PressureDatum.Admissible g a cap) : Nonempty (CoefficientFamily h j σ (PressureDatum.pressure g a))

theorem NavierStokes.NaturalAxisCoefficients.exists_coefficientFamily_with_convex_domain {h j σ : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {g a : ℝ → ℝ} {cap : ℝ} (hp : PressureDatum.Admissible g a cap) : ∃ (v : CoefficientFamily h j σ (PressureDatum.pressure g a)) (ρ : ℝ), v.epsilon < ρ ∧ ∃ (U : Set ℂ) (K : Set ℂ), IsOpen U ∧ Convex ℝ U ∧ 0 ∈ U ∧ IsCompact K ∧ (∀ x ∈ window.interval, Metric.closedBall (↑x) ρ ⊆ K) ∧ K ⊆ U ∧ U ⊆ regularSet h j σ

The coefficient family and the open convex domain for its primitive can be chosen together, with an explicit strict gap between the two radii.

noncomputable def NavierStokes.NaturalAxisCoefficients.CoefficientFamily.axisData {h j σ : ℝ} {P : ℝ → ℝ} (v : CoefficientFamily h j σ P) : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace window v.epsilon)

Axis data, bundling A, D, h, one and the required compatibility proofs.

Equations

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

theorem NavierStokes.NaturalAxisCoefficients.CoefficientFamily.radiallyConstant {h j σ : ℝ} {P : ℝ → ℝ} (v : CoefficientFamily h j σ P) (k : Field) : NaturalAxisBridge.RadiallyConstant window v.epsilon (v.elements k)

theorem NavierStokes.NaturalAxisCoefficients.CoefficientFamily.value {h j σ : ℝ} {P : ℝ → ℝ} (v : CoefficientFamily h j σ P) (k : Field) {x : ℝ} (hx : x ∈ window.interval) : NaturalAxisBridge.inputValue window v.epsilon (v.elements k) x = realField h j σ P k x

theorem NavierStokes.NaturalAxisCoefficients.CoefficientFamily.compatible {h j σ : ℝ} {P : ℝ → ℝ} (v : CoefficientFamily h j σ P) : NaturalAxisBridge.CompatibleData window v.epsilon (v.elements Field.chi) v.axisData

theorem NavierStokes.NaturalAxisCoefficients.ideal_prefix_fixed_coefficients {h j : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) {g a : ℝ → ℝ} {cap B : ℝ} (hp : PressureDatum.Admissible g a cap) (hB : 2 ≤ B) (hg : ∀ y ≤ 0, g y = B ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) : ∃ (δ : ℝ) (σ : ℝ), 0 < δ ∧ 0 < σ ∧ (∀ x ∈ Set.Icc (-1) 1, |NaturalAxisData.Z h j (PressureDatum.pressure g a) x| ≤ δ → 99 / 100 < NaturalAxisData.chi h j σ x) ∧ Nonempty (CoefficientFamily h j σ (PressureDatum.pressure g a))

noncomputable def NavierStokes.NaturalAxisCoefficients.axisPhase (h j σ : ℝ) : ℂ → ℂ

The actual normalized logarithmic phase, as a complex segment integral.

Equations

• NavierStokes.NaturalAxisCoefficients.axisPhase h j σ = NavierStokes.AnalyticPrimitive.primitive (NavierStokes.NaturalAxisCoefficients.complexGradient h j σ)

noncomputable def NavierStokes.NaturalAxisCoefficients.realPhase (h j σ x : ℝ) : ℝ

Real phase, given by x * ∫ t in (0 : ℝ)..1, realGradient h j σ (t * x).

Equations

• NavierStokes.NaturalAxisCoefficients.realPhase h j σ x = x * ∫ (t : ℝ) in 0..1, NavierStokes.NaturalAxisCoefficients.realGradient h j σ (t * x)

@[simp]

theorem NavierStokes.NaturalAxisCoefficients.axisPhase_zero (h j σ : ℝ) : axisPhase h j σ 0 = 0

@[simp]

theorem NavierStokes.NaturalAxisCoefficients.axisPhase_ofReal (h j σ x : ℝ) : axisPhase h j σ ↑x = ↑(realPhase h j σ x)

structure NavierStokes.NaturalAxisCoefficients.AnalyticInputs (h j σ : ℝ) (P : ℝ → ℝ) : Type

The fixed coefficient family and its actual analytic phase on one common compact neighborhood. No primitive or coefficient record is assumed by the existence theorem below.

• coefficients : CoefficientFamily h j σ P

  Coefficients of AnalyticInputs, of type CoefficientFamily h j σ P.

• radius : ℝ

  Radius of AnalyticInputs, of type ℝ.

• radius_gap : self.coefficients.epsilon < self.radius
• compactSet : Set ℂ

  Compact set of AnalyticInputs, of type Set ℂ.

• isCompact : IsCompact self.compactSet
• covers (x : ℝ) : x ∈ window.interval → Metric.closedBall (↑x) self.radius ⊆ self.compactSet
• phase_analytic : AnalyticOnNhd ℂ (axisPhase h j σ) self.compactSet
• phase_derivative (z : ℂ) : z ∈ self.compactSet → HasDerivAt (axisPhase h j σ) (complexGradient h j σ z) z

theorem NavierStokes.NaturalAxisCoefficients.exists_analyticInputs {h j σ : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {g a : ℝ → ℝ} {cap : ℝ} (hp : PressureDatum.Admissible g a cap) : Nonempty (AnalyticInputs h j σ (PressureDatum.pressure g a))

theorem NavierStokes.NaturalAxisCoefficients.AnalyticInputs.radius_pos {h j σ : ℝ} {P : ℝ → ℝ} (d : AnalyticInputs h j σ P) : 0 < d.radius

theorem NavierStokes.NaturalAxisCoefficients.AnalyticInputs.real_mem_compact {h j σ : ℝ} {P : ℝ → ℝ} (d : AnalyticInputs h j σ P) {x : ℝ} (hx : x ∈ window.interval) : ↑x ∈ d.compactSet

theorem NavierStokes.NaturalAxisCoefficients.AnalyticInputs.realPhase_hasDerivAt {h j σ : ℝ} {P : ℝ → ℝ} (d : AnalyticInputs h j σ P) {x : ℝ} (hx : x ∈ window.interval) : HasDerivAt (realPhase h j σ) (realGradient h j σ x) x

noncomputable def NavierStokes.NaturalAxisCoefficients.realAmplitude (h j σ Λ C x : ℝ) : ℝ

Real amplitude, given by Real.exp (Λ * realPhase h j σ x) / C.

Equations

• NavierStokes.NaturalAxisCoefficients.realAmplitude h j σ Λ C x = Real.exp (Λ * NavierStokes.NaturalAxisCoefficients.realPhase h j σ x) / C

theorem NavierStokes.NaturalAxisCoefficients.AnalyticInputs.realAmplitude_hasDerivAt {h j σ : ℝ} {P : ℝ → ℝ} (d : AnalyticInputs h j σ P) (Λ C : ℝ) {x : ℝ} (hx : x ∈ window.interval) : HasDerivAt (realAmplitude h j σ Λ C) (Λ * realGradient h j σ x * realAmplitude h j σ Λ C x) x

theorem NavierStokes.NaturalAxisCoefficients.realAmplitude_pos (h j σ Λ : ℝ) {C : ℝ} (hC : 0 < C) (x : ℝ) : 0 < realAmplitude h j σ Λ C x

theorem NavierStokes.NaturalAxisCoefficients.AnalyticInputs.realAmplitude_logDerivative {h j σ : ℝ} {P : ℝ → ℝ} (d : AnalyticInputs h j σ P) (Λ : ℝ) {C : ℝ} (hC : 0 < C) {x : ℝ} (hx : x ∈ window.interval) : deriv (realAmplitude h j σ Λ C) x / realAmplitude h j σ Λ C x = Λ * realGradient h j σ x

The true logarithmic derivative is the prescribed ξ₀=Λκ.

noncomputable def NavierStokes.NaturalAxisCoefficients.AnalyticInputs.normalizationThreshold {h j σ : ℝ} {P : ℝ → ℝ} (d : AnalyticInputs h j σ P) (Λ : ℝ) : ℝ

Normalization threshold, given by Real.exp (Λ * realPartSup (axisPhase h j σ) d.compactSet).

Equations

• d.normalizationThreshold Λ = Real.exp (Λ * NavierStokes.AnalyticCoefficientBounds.realPartSup (NavierStokes.NaturalAxisCoefficients.axisPhase h j σ) d.compactSet)

noncomputable def NavierStokes.NaturalAxisCoefficients.AnalyticInputs.amplitudeBound {h j σ : ℝ} {P : ℝ → ℝ} (d : AnalyticInputs h j σ P) : ℝ

Amplitude bound, given by radiusLoss (d.coefficients.epsilon / d.radius).

Equations

• d.amplitudeBound = NavierStokes.AnalyticCoefficientBounds.radiusLoss (d.coefficients.epsilon / d.radius)

theorem NavierStokes.NaturalAxisCoefficients.AnalyticInputs.amplitudeBound_nonneg {h j σ : ℝ} {P : ℝ → ℝ} (d : AnalyticInputs h j σ P) : 0 ≤ d.amplitudeBound

theorem NavierStokes.NaturalAxisCoefficients.AnalyticInputs.uniformAmplitude {h j σ : ℝ} {P : ℝ → ℝ} (d : AnalyticInputs h j σ P) (Λ : ℝ) : 0 ≤ Λ → ∀ (C : ℝ), d.normalizationThreshold Λ ≤ C → ∃ (a : ↥(AxisCoefficientSpace.AxisSpace window d.coefficients.epsilon)), ‖a‖ ≤ d.amplitudeBound ∧ NaturalAxisBridge.RadiallyConstant window d.coefficients.epsilon a ∧ ∀ x ∈ window.interval, NaturalAxisBridge.inputValue window d.coefficients.epsilon a x = realAmplitude h j σ Λ C x

The actual φ*/C belongs to exactly the same coefficient space as all fixed data, uniformly for every allowed large parameter and normalization.

theorem NavierStokes.NaturalAxisCoefficients.ideal_prefix_analytic_inputs {h j : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) {g a : ℝ → ℝ} {cap B : ℝ} (hp : PressureDatum.Admissible g a cap) (hB : 2 ≤ B) (hg : ∀ y ≤ 0, g y = B ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) : ∃ (δ : ℝ) (σ : ℝ), 0 < δ ∧ 0 < σ ∧ (∀ x ∈ Set.Icc (-1) 1, |NaturalAxisData.Z h j (PressureDatum.pressure g a) x| ≤ δ → 99 / 100 < NaturalAxisData.chi h j σ x) ∧ Nonempty (AnalyticInputs h j σ (PressureDatum.pressure g a))

End-to-end fixed analytic input construction from the actual pressure integral and ideal prefix, including the normalized amplitude source.

def NavierStokes.NaturalProfile.rescalePoint (Λ : ℝ) (p : ℝ × ℝ) : ℝ × ℝ

Rescale point, given by (Λ * p.1, p.2).

Equations

• NavierStokes.NaturalProfile.rescalePoint Λ p = (Λ * p.1, p.2)

def NavierStokes.NaturalProfile.domain (Λ : ℝ) : Set (ℝ × ℝ)

Domain, given by rescalePoint Λ ⁻¹' AxisEvaluation.strip window 20.

Equations

• NavierStokes.NaturalProfile.domain Λ = NavierStokes.NaturalProfile.rescalePoint Λ ⁻¹' NavierStokes.AxisEvaluation.strip NavierStokes.NaturalAxisCoefficients.window 20

def NavierStokes.NaturalProfile.pullback (Λ : ℝ) (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Pullback, given by F (rescalePoint Λ p).

Equations

• NavierStokes.NaturalProfile.pullback Λ F p = F (NavierStokes.NaturalProfile.rescalePoint Λ p)

def NavierStokes.NaturalProfile.affineProfile (b : ℝ → ℝ) (c Λ : ℝ) (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Affine profile, given by b p.2 + c * pullback Λ F p.

Equations

• NavierStokes.NaturalProfile.affineProfile b c Λ F p = b p.2 + c * NavierStokes.NaturalProfile.pullback Λ F p

def NavierStokes.NaturalProfile.angularProfile (a : ℝ → ℝ) (Λ : ℝ) (Φ : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Angular profile, given by a p.2 * pullback Λ Φ p.

Equations

• NavierStokes.NaturalProfile.angularProfile a Λ Φ p = a p.2 * NavierStokes.NaturalProfile.pullback Λ Φ p

theorem NavierStokes.NaturalProfile.contDiff_rescalePoint (Λ : ℝ) : ContDiff ℝ (↑⊤) (rescalePoint Λ)

theorem NavierStokes.NaturalProfile.domain_isOpen (Λ : ℝ) : IsOpen (domain Λ)

theorem NavierStokes.NaturalProfile.pullback_smooth {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (Λ : ℝ) : ContDiffOn ℝ (↑⊤) (pullback Λ F) (domain Λ)

theorem NavierStokes.NaturalProfile.affineProfile_smooth {b : ℝ → ℝ} (hb : ContDiffOn ℝ (↑⊤) b (Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right)) {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (c Λ : ℝ) : ContDiffOn ℝ (↑⊤) (affineProfile b c Λ F) (domain Λ)

theorem NavierStokes.NaturalProfile.angularProfile_smooth {a : ℝ → ℝ} (ha : ContDiffOn ℝ (↑⊤) a (Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right)) {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (Λ : ℝ) : ContDiffOn ℝ (↑⊤) (angularProfile a Λ Φ) (domain Λ)

theorem NavierStokes.NaturalProfile.sliceY_smooth {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip NaturalAxisCoefficients.window 20) : ContDiffAt ℝ (↑⊤) (fun (Y : ℝ) => F (Y, p.2)) p.1

theorem NavierStokes.NaturalProfile.sliceEta_smooth {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip NaturalAxisCoefficients.window 20) : ContDiffAt ℝ (↑⊤) (fun (η : ℝ) => F (p.1, η)) p.2

theorem NavierStokes.NaturalProfile.pullback_hasDerivAt_Y {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (Λ : ℝ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : HasDerivAt (fun (X : ℝ) => pullback Λ F (X, p.2)) (Λ * NaturalAxisBridge.partialY F (rescalePoint Λ p)) p.1

theorem NavierStokes.NaturalProfile.pullback_partialY {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (Λ : ℝ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : NaturalAxisBridge.partialY (pullback Λ F) p = Λ * NaturalAxisBridge.partialY F (rescalePoint Λ p)

theorem NavierStokes.NaturalProfile.pullback_partialEta (Λ : ℝ) (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : NaturalAxisBridge.partialEta (pullback Λ F) p = NaturalAxisBridge.partialEta F (rescalePoint Λ p)

theorem NavierStokes.NaturalProfile.pullback_second_Y {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (Λ : ℝ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : iteratedDeriv 2 (fun (X : ℝ) => pullback Λ F (X, p.2)) p.1 = Λ ^ 2 * iteratedDeriv 2 (fun (Y : ℝ) => F (Y, p.2)) (Λ * p.1)

theorem NavierStokes.NaturalProfile.pullback_radialDifferential {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (Λ : ℝ) (r : ℕ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : NaturalAxisBridge.radialDifferential r (pullback Λ F) p = Λ * NaturalAxisBridge.radialDifferential r F (rescalePoint Λ p)

theorem NavierStokes.NaturalProfile.affineProfile_partialY {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (b : ℝ → ℝ) (c Λ : ℝ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : NaturalAxisBridge.partialY (affineProfile b c Λ F) p = c * Λ * NaturalAxisBridge.partialY F (rescalePoint Λ p)

theorem NavierStokes.NaturalProfile.affineProfile_partialEta {b : ℝ → ℝ} {b' : ℝ} {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (c Λ : ℝ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) (hb : HasDerivAt b b' p.2) : NaturalAxisBridge.partialEta (affineProfile b c Λ F) p = b' + c * NaturalAxisBridge.partialEta F (rescalePoint Λ p)

theorem NavierStokes.NaturalProfile.affineProfile_radialDifferential {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (b : ℝ → ℝ) (c Λ : ℝ) (r : ℕ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : NaturalAxisBridge.radialDifferential r (affineProfile b c Λ F) p = c * Λ * NaturalAxisBridge.radialDifferential r F (rescalePoint Λ p)

theorem NavierStokes.NaturalProfile.angularProfile_partialY {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (a : ℝ → ℝ) (Λ : ℝ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : NaturalAxisBridge.partialY (angularProfile a Λ Φ) p = a p.2 * Λ * NaturalAxisBridge.partialY Φ (rescalePoint Λ p)

theorem NavierStokes.NaturalProfile.angularProfile_partialEta {a : ℝ → ℝ} {a' : ℝ} {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (Λ : ℝ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) (ha : HasDerivAt a a' p.2) : NaturalAxisBridge.partialEta (angularProfile a Λ Φ) p = a' * Φ (rescalePoint Λ p) + a p.2 * NaturalAxisBridge.partialEta Φ (rescalePoint Λ p)

theorem NavierStokes.NaturalProfile.angularProfile_radialDifferential {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (a : ℝ → ℝ) (Λ : ℝ) (r : ℕ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : NaturalAxisBridge.radialDifferential r (angularProfile a Λ Φ) p = a p.2 * Λ * NaturalAxisBridge.radialDifferential r Φ (rescalePoint Λ p)

noncomputable def NavierStokes.NaturalProfile.actualData (h j σ : ℝ) (P0 : ℝ → ℝ) : NaturalAxisBridge.ParameterData

The fixed polynomial and pressure fields, interpreted as real functions.

Equations

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

theorem NavierStokes.NaturalProfile.materialize_scaled {h j σ t : ℝ} {P0 a₀ : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (a : ↥(AxisCoefficientSpace.AxisSpace NaturalAxisCoefficients.window v.epsilon)) (ha : ∀ η ∈ NaturalAxisCoefficients.window.interval, NaturalAxisBridge.inputValue NaturalAxisCoefficients.window v.epsilon a η = a₀ η) {Φ u B P : ℝ × ℝ → ℝ} (hs : NaturalAxisBridge.IsScaledSolution NaturalAxisCoefficients.window (NaturalAxisBridge.parameters NaturalAxisCoefficients.window v.epsilon (v.elements NaturalAxisCoefficients.Field.chi) v.axisData) t (NaturalAxisBridge.inputValue NaturalAxisCoefficients.window v.epsilon a) Φ u B P) : NaturalAxisBridge.IsScaledSolution NaturalAxisCoefficients.window (actualData h j σ P0) t a₀ Φ u B P

Replace all coefficient evaluations by their proved concrete values.

theorem NavierStokes.NaturalProfile.amplitude_smooth {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (Λ C : ℝ) : ContDiffOn ℝ (↑⊤) (NaturalAxisCoefficients.realAmplitude h j σ Λ C) (Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right)

theorem NavierStokes.NaturalProfile.uStar_hasDerivAt (j η : ℝ) : HasDerivAt (NaturalAxisData.U j) 4 η

theorem NavierStokes.NaturalProfile.uStar_smooth (j : ℝ) : ContDiff ℝ (↑⊤) (NaturalAxisData.U j)

noncomputable def NavierStokes.NaturalProfile.transportW (h : ℝ) (V : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The natural transport coefficient recovered from the true radial average.

Equations

• NavierStokes.NaturalProfile.transportW h V p = 1 - 2 * NavierStokes.NaturalAxisData.D h * p.2 * V p - NavierStokes.NaturalAxisData.d p.2 * NavierStokes.NaturalAxisBridge.partialEta V p

noncomputable def NavierStokes.NaturalProfile.transportH (h : ℝ) (U : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Transport H, given by NaturalAxisData.D h * p.2 + NaturalAxisData.d p.2 * U p.

Equations

• NavierStokes.NaturalProfile.transportH h U p = NavierStokes.NaturalAxisData.D h * p.2 + NavierStokes.NaturalAxisData.d p.2 * U p

theorem NavierStokes.NaturalProfile.transportW_reconstruct {h j σ Λ : ℝ} (P0 : ℝ → ℝ) {B : ℝ × ℝ → ℝ} (hB : ContDiffOn ℝ (↑⊤) B (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : transportW h (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ B) p = NaturalAxisBridge.reconstructedW (actualData h j σ P0) (1 / Λ) B (rescalePoint Λ p)

theorem NavierStokes.NaturalProfile.transportH_reconstruct (h j σ Λ : ℝ) (P0 : ℝ → ℝ) (u : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : transportH h (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u) p = NaturalAxisBridge.reconstructedH (actualData h j σ P0) (1 / Λ) u (rescalePoint Λ p)

theorem NavierStokes.NaturalProfile.gradient_identity (h j σ η : ℝ) : NaturalAxisData.H h j η * NaturalAxisCoefficients.realGradient h j σ η = -NaturalAxisData.L h η * NaturalAxisData.chi h j σ η

structure NavierStokes.NaturalProfile.IsNaturalSolution (h j Λ : ℝ) (P0 a₀ : ℝ → ℝ) (f U V Pr : ℝ × ℝ → ℝ) : Prop

The actual unscaled system, with all derivatives taken on real functions.

• f_smooth : ContDiffOn ℝ (↑⊤) f (domain Λ)
• U_smooth : ContDiffOn ℝ (↑⊤) U (domain Λ)
• average_smooth : ContDiffOn ℝ (↑⊤) V (domain Λ)
• pressure_smooth : ContDiffOn ℝ (↑⊤) Pr (domain Λ)
• f_axis (η : ℝ) : η ∈ Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right → f (0, η) = a₀ η
• U_axis (η : ℝ) : η ∈ Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right → U (0, η) = NaturalAxisData.U j η
• average_axis (η : ℝ) : η ∈ Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right → V (0, η) = NaturalAxisData.U j η
• pressure_axis (η : ℝ) : η ∈ Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right → Pr (0, η) = P0 η
• average_equation (p : ℝ × ℝ) : p ∈ domain Λ → V p + p.1 * NaturalAxisBridge.partialY V p = U p
• pressure_equation (p : ℝ × ℝ) : p ∈ domain Λ → NaturalAxisBridge.partialY Pr p = f p ^ 2
• average_integral (p : ℝ × ℝ) : p ∈ domain Λ → p.1 * V p = ∫ (X : ℝ) in 0..p.1, U (X, p.2)
• pressure_integral (p : ℝ × ℝ) : p ∈ domain Λ → Pr p - P0 p.2 = ∫ (X : ℝ) in 0..p.1, f (X, p.2) ^ 2
• angular_equation (p : ℝ × ℝ) : p ∈ domain Λ → 2 * NaturalAxisData.L h p.2 * NaturalAxisBridge.radialDifferential 2 f p = transportW h V p * (p.1 * NaturalAxisBridge.partialY f p + f p) + h * (1 - 2 * p.2 * U p) * f p + transportH h U p * NaturalAxisBridge.partialEta f p
• axial_equation (p : ℝ × ℝ) : p ∈ domain Λ → 2 * NaturalAxisData.L h p.2 * NaturalAxisBridge.radialDifferential 1 U p = transportW h V p * (p.1 * NaturalAxisBridge.partialY U p) + NaturalAxisData.A h * (1 - 2 * p.2 * U p) * U p + transportH h U p * NaturalAxisBridge.partialEta U p + NaturalAxisData.d p.2 * NaturalAxisBridge.partialEta Pr p - 4 * NaturalAxisData.A h * p.2 * Pr p - 2 * p.2 * p.1 * NaturalAxisBridge.partialY Pr p

theorem NavierStokes.NaturalProfile.angular_equation_reconstruct {h j σ Λ : ℝ} {P0 a₀ : ℝ → ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hΛ : Λ ≠ 0) {Φ u B P : ℝ × ℝ → ℝ} (hs : NaturalAxisBridge.IsScaledSolution NaturalAxisCoefficients.window (actualData h j σ P0) (1 / Λ) a₀ Φ u B P) {p : ℝ × ℝ} (hp : p ∈ domain Λ) (ha : HasDerivAt a₀ (Λ * NaturalAxisCoefficients.realGradient h j σ p.2 * a₀ p.2) p.2) : 2 * NaturalAxisData.L h p.2 * NaturalAxisBridge.radialDifferential 2 (angularProfile a₀ Λ Φ) p = transportW h (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ B) p * (p.1 * NaturalAxisBridge.partialY (angularProfile a₀ Λ Φ) p + angularProfile a₀ Λ Φ p) + h * (1 - 2 * p.2 * affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u p) * angularProfile a₀ Λ Φ p + transportH h (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u) p * NaturalAxisBridge.partialEta (angularProfile a₀ Λ Φ) p

theorem NavierStokes.NaturalProfile.axial_equation_reconstruct {h j σ Λ : ℝ} {P0 a₀ : ℝ → ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hΛ : Λ ≠ 0) (hP0 : ContDiff ℝ (↑⊤) P0) {Φ u B P : ℝ × ℝ → ℝ} (hs : NaturalAxisBridge.IsScaledSolution NaturalAxisCoefficients.window (actualData h j σ P0) (1 / Λ) a₀ Φ u B P) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : 2 * NaturalAxisData.L h p.2 * NaturalAxisBridge.radialDifferential 1 (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u) p = transportW h (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ B) p * (p.1 * NaturalAxisBridge.partialY (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u) p) + NaturalAxisData.A h * (1 - 2 * p.2 * affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u p) * affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u p + transportH h (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u) p * NaturalAxisBridge.partialEta (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u) p + NaturalAxisData.d p.2 * NaturalAxisBridge.partialEta (affineProfile P0 (1 / Λ) Λ P) p - 4 * NaturalAxisData.A h * p.2 * affineProfile P0 (1 / Λ) Λ P p - 2 * p.2 * p.1 * NaturalAxisBridge.partialY (affineProfile P0 (1 / Λ) Λ P) p

theorem NavierStokes.NaturalProfile.domain_segment {Λ : ℝ} (hΛ : 0 < Λ) {p : ℝ × ℝ} (hp : p ∈ domain Λ) {X : ℝ} (hX : X ∈ Set.uIcc 0 p.1) : (X, p.2) ∈ domain Λ

theorem NavierStokes.NaturalProfile.average_integral_reconstruct {Λ : ℝ} (hΛ : 0 < Λ) (b : ℝ → ℝ) (c : ℝ) {u B : ℝ × ℝ → ℝ} (hu : ContDiffOn ℝ (↑⊤) u (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (havg : ∀ q ∈ AxisEvaluation.strip NaturalAxisCoefficients.window 20, q.1 * B q = ∫ (Y : ℝ) in 0..q.1, u (Y, q.2)) {p : ℝ × ℝ} (hp : p ∈ domain Λ) : p.1 * affineProfile b c Λ B p = ∫ (X : ℝ) in 0..p.1, affineProfile b c Λ u (X, p.2)

theorem NavierStokes.NaturalProfile.reconstruct_solution {h j σ Λ : ℝ} {P0 a₀ : ℝ → ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) (haSmooth : ContDiffOn ℝ (↑⊤) a₀ (Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right)) (ha : ∀ η ∈ Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right, HasDerivAt a₀ (Λ * NaturalAxisCoefficients.realGradient h j σ η * a₀ η) η) {Φ u B P : ℝ × ℝ → ℝ} (hs : NaturalAxisBridge.IsScaledSolution NaturalAxisCoefficients.window (actualData h j σ P0) (1 / Λ) a₀ Φ u B P) : IsNaturalSolution h j Λ P0 a₀ (angularProfile a₀ Λ Φ) (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u) (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ B) (affineProfile P0 (1 / Λ) Λ P)

Reconstruction preserves the full differential and integral system.

theorem NavierStokes.NaturalProfile.angularProfile_log_slope_at_four {Λ : ℝ} (hΛ : 0 < Λ) {a : ℝ → ℝ} {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) {η : ℝ} (hη : η ∈ Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right) (ha : 0 < a η) (hval : 0 < Φ (4, η)) : -2 * (4 / Λ) * NaturalAxisBridge.partialY (angularProfile a Λ Φ) (4 / Λ, η) / angularProfile a Λ Φ (4 / Λ, η) = -8 * NaturalAxisBridge.partialY Φ (4, η) / Φ (4, η)

noncomputable def NavierStokes.NaturalProfile.profileErrorConstant {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) : ℝ

Profile error constant, constructed using errorConstant.

Equations

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

structure NavierStokes.NaturalProfile.ProfileFamily {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (Λ C : ℝ) : Type

The functions and estimates obtained from one actual coefficient-space fixed point. All unscaled functions are explicit expressions in these fields.

• phi : ℝ × ℝ → ℝ

  Phi of ProfileFamily, of type ℝ × ℝ → ℝ.

• u : ℝ × ℝ → ℝ

  U of ProfileFamily, of type ℝ × ℝ → ℝ.

• average : ℝ × ℝ → ℝ

  Average of ProfileFamily, of type ℝ × ℝ → ℝ.

• pressure : ℝ × ℝ → ℝ

  Pressure field of ProfileFamily, of type ℝ × ℝ → ℝ.

• natural : IsNaturalSolution h j Λ P0 (NaturalAxisCoefficients.realAmplitude h j σ Λ C) (angularProfile (NaturalAxisCoefficients.realAmplitude h j σ Λ C) Λ self.phi) (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ self.u) (affineProfile (NaturalAxisData.U j) (1 / Λ) Λ self.average) (affineProfile P0 (1 / Λ) Λ self.pressure)
• mixed_error : NaturalAxisBridge.UniformMixedError NaturalAxisCoefficients.window d.coefficients.epsilon (profileErrorConstant d / (2 * Λ)) self.phi self.u (AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon (NaturalAxisBridge.referenceCoefficients NaturalAxisCoefficients.window ⋯ (d.coefficients.elements NaturalAxisCoefficients.Field.chi) d.coefficients.axisData).1) (AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon (NaturalAxisBridge.referenceCoefficients NaturalAxisCoefficients.window ⋯ (d.coefficients.elements NaturalAxisCoefficients.Field.chi) d.coefficients.axisData).2)
• positive (p : ℝ × ℝ) : p ∈ domain Λ → 0 ≤ Λ * p.1 → Λ * p.1 ≤ 41 / 10 → 0 < angularProfile (NaturalAxisCoefficients.realAmplitude h j σ Λ C) Λ self.phi p
• slope (η : ℝ) : η ∈ Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right → 99 / 100 ≤ NaturalAxisData.chi h j σ η → 23 / 10 < -2 * (4 / Λ) * NaturalAxisBridge.partialY (angularProfile (NaturalAxisCoefficients.realAmplitude h j σ Λ C) Λ self.phi) (4 / Λ, η) / angularProfile (NaturalAxisCoefficients.realAmplitude h j σ Λ C) Λ self.phi (4 / Λ, η)

noncomputable def NavierStokes.NaturalProfile.ProfileFamily.f {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : ProfileFamily d Λ C) : ℝ × ℝ → ℝ

F, given by angularProfile (realAmplitude h j σ Λ C) Λ F.phi.

Equations

• F.f = NavierStokes.NaturalProfile.angularProfile (NavierStokes.NaturalAxisCoefficients.realAmplitude h j σ Λ C) Λ F.phi

noncomputable def NavierStokes.NaturalProfile.ProfileFamily.U {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : ProfileFamily d Λ C) : ℝ × ℝ → ℝ

U, given by affineProfile (NaturalAxisData.U j) (1 / Λ) Λ F.u.

Equations

• F.U = NavierStokes.NaturalProfile.affineProfile (NavierStokes.NaturalAxisData.U j) (1 / Λ) Λ F.u

noncomputable def NavierStokes.NaturalProfile.ProfileFamily.Ubar {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : ProfileFamily d Λ C) : ℝ × ℝ → ℝ

Ubar, given by affineProfile (NaturalAxisData.U j) (1 / Λ) Λ F.average.

Equations

• F.Ubar = NavierStokes.NaturalProfile.affineProfile (NavierStokes.NaturalAxisData.U j) (1 / Λ) Λ F.average

noncomputable def NavierStokes.NaturalProfile.ProfileFamily.Pi {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : ProfileFamily d Λ C) : ℝ × ℝ → ℝ

Pi, given by affineProfile P0 (1 / Λ) Λ F.pressure.

Equations

• F.Pi = NavierStokes.NaturalProfile.affineProfile P0 (1 / Λ) Λ F.pressure

theorem NavierStokes.NaturalProfile.exists_profileFamily {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hP0 : ContDiff ℝ (↑⊤) P0) : ∃ (Λ₀ : ℝ), 0 < Λ₀ ∧ ∀ (Λ : ℝ), Λ₀ ≤ Λ → ∀ (C : ℝ), d.normalizationThreshold Λ ≤ C → Nonempty (ProfileFamily d Λ C)

The scale threshold is uniform over every normalization above the actual compact-domain exponential threshold.

theorem NavierStokes.NaturalProfile.ideal_prefix_profileFamily {h j : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) {g a : ℝ → ℝ} {cap B : ℝ} (hp : PressureDatum.Admissible g a cap) (hB : 2 ≤ B) (hg : ∀ y ≤ 0, g y = B ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) : ∃ (δ : ℝ) (σ : ℝ), 0 < δ ∧ 0 < σ ∧ (∀ η ∈ Set.Icc (-1) 1, |NaturalAxisData.Z h j (PressureDatum.pressure g a) η| ≤ δ → 99 / 100 < NaturalAxisData.chi h j σ η) ∧ ∃ (d : NaturalAxisCoefficients.AnalyticInputs h j σ (PressureDatum.pressure g a)) (Λ₀ : ℝ), 0 < Λ₀ ∧ ∀ (Λ : ℝ), Λ₀ ≤ Λ → ∀ (C : ℝ), d.normalizationThreshold Λ ≤ C → Nonempty (ProfileFamily d Λ C)

The pressure integral and ideal prefix yield actual unscaled natural profiles after selecting the cutoff and common analytic coefficient radius.

theorem NavierStokes.NaturalProfile.exists_natural_profiles {h j : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) {g a : ℝ → ℝ} {cap B : ℝ} (hp : PressureDatum.Admissible g a cap) (hB : 2 ≤ B) (hg : ∀ y ≤ 0, g y = B ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) : ∃ (δ : ℝ) (σ : ℝ) (Λ : ℝ) (C : ℝ), 0 < δ ∧ 0 < σ ∧ 0 < Λ ∧ 0 < C ∧ ∃ (f : ℝ × ℝ → ℝ) (U : ℝ × ℝ → ℝ) (V : ℝ × ℝ → ℝ) (Pr : ℝ × ℝ → ℝ), IsNaturalSolution h j Λ (PressureDatum.pressure g a) (NaturalAxisCoefficients.realAmplitude h j σ Λ C) f U V Pr ∧ (∀ p ∈ domain Λ, 0 ≤ Λ * p.1 → Λ * p.1 ≤ 41 / 10 → 0 < f p) ∧ ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisData.Z h j (PressureDatum.pressure g a) η| ≤ δ → 23 / 10 < -2 * (4 / Λ) * NaturalAxisBridge.partialY f (4 / Λ, η) / f (4 / Λ, η)

A direct existence theorem for the unscaled real functions. The cutoff, analytic input family, large scale, and normalization are all constructed from the stated pressure assumptions.