The actual natural/ACT base in the all-order local axis recursion

The finite base functions below are the constructed holomorphic natural/ACT functions. Every regularity field required by SlowRecursion is derived from those functions. In particular the angular slow coefficient is C*f.

Holomorphic parameter extension of the evaluated axis space

The extension is the convergent vertical Taylor series of the genuine compatible parameter jets. Its Cauchy--Riemann identity follows by termwise differentiation.

noncomputable def NavierStokes.AxisHolomorphic.geometricMoment (q : ℝ) (k : ℕ) : ℝ

The polynomial moment of a geometric series.

Equations

• NavierStokes.AxisHolomorphic.geometricMoment q k = ∑' (n : ℕ), (↑n + 1) ^ k * q ^ n

theorem NavierStokes.AxisHolomorphic.summable_geometricMoment {q : ℝ} (hq : 0 < q) (hq1 : q < 1) (k : ℕ) : Summable fun (n : ℕ) => (↑n + 1) ^ k * q ^ n

theorem NavierStokes.AxisHolomorphic.geometricMoment_nonneg {q : ℝ} (hq : 0 ≤ q) (k : ℕ) : 0 ≤ geometricMoment q k

theorem NavierStokes.AxisHolomorphic.weight_le_core {ε : ℝ} (hε : 0 < ε) (n m : ℕ) : AxisWeightEstimates.weight ε n m ≤ AxisWeightEstimates.coreWeight ε n m

theorem NavierStokes.AxisHolomorphic.choose_geometric_le {s : ℝ} (hs : 0 < s) (hs1 : s < 1) (n m : ℕ) : ↑((n + m).choose m) * s ^ n ≤ 1 / (1 - s) ^ (m + 1)

theorem NavierStokes.AxisHolomorphic.term_factorial_bound (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m n : ℕ) {p : ℝ × ℝ} (hp : |p.1| ≤ R) : ‖AxisEvaluation.term I ε A k m n p‖ ≤ ‖A‖ / (1 - s) * ↑m.factorial * (ε * (1 - s))⁻¹ ^ m * ((↑n + 1) ^ k * (R / 20 / s) ^ n)

A sharp majorant retaining the binomial factor in the axis norm.

theorem NavierStokes.AxisHolomorphic.mixedSeries_factorial_bound (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {p : ℝ × ℝ} (hp : |p.1| ≤ R) : ‖AxisEvaluation.mixedSeries I ε A k m p‖ ≤ ‖A‖ / (1 - s) * geometricMoment (R / 20 / s) k * ↑m.factorial * (ε * (1 - s))⁻¹ ^ m

Uniform genuine factorial bounds for all evaluated parameter derivatives. The positive radius is independent of the fixed radial derivative order k.

noncomputable def NavierStokes.AxisHolomorphic.parameterStrip (I : AxisCoefficientSpace.Window) (a : ℝ) : Set ℂ

The rectangle above the real window used by the vertical Taylor series.

Equations

• NavierStokes.AxisHolomorphic.parameterStrip I a = {z : ℂ | z.re ∈ Set.Ioo I.left I.right ∧ |z.im| < a / 2}

theorem NavierStokes.AxisHolomorphic.parameterStrip_isOpen (I : AxisCoefficientSpace.Window) (a : ℝ) : IsOpen (parameterStrip I a)

theorem NavierStokes.AxisHolomorphic.parameterStrip_convex (I : AxisCoefficientSpace.Window) (a : ℝ) : Convex ℝ (parameterStrip I a)

noncomputable def NavierStokes.AxisHolomorphic.complexLinearForm (u v : ℂ) : ℂ →L[ℝ] ℂ

A real-linear map specified by its real and imaginary partial derivatives.

Equations

• NavierStokes.AxisHolomorphic.complexLinearForm u v = Complex.reCLM.smulRight u + Complex.imCLM.smulRight v

theorem NavierStokes.AxisHolomorphic.complexLinearForm_norm (u v : ℂ) : ‖complexLinearForm u v‖ ≤ ‖u‖ + ‖v‖

theorem NavierStokes.AxisHolomorphic.complexLinearForm_tsum {u v : ℕ → ℂ} (hu : Summable u) (hv : Summable v) : ∑' (n : ℕ), complexLinearForm (u n) (v n) = complexLinearForm (∑' (n : ℕ), u n) (∑' (n : ℕ), v n)

noncomputable def NavierStokes.AxisHolomorphic.verticalTerm (c : ℕ → ℝ → ℝ) (m : ℕ) (z : ℂ) : ℂ

A vertical Taylor monomial; c m is the normalized genuine real jet.

Equations

• NavierStokes.AxisHolomorphic.verticalTerm c m z = ↑(c m z.re) * (↑z.im * Complex.I) ^ m

noncomputable def NavierStokes.AxisHolomorphic.verticalX (c : ℕ → ℝ → ℝ) (m : ℕ) (z : ℂ) : ℂ

Vertical X, given by ((m : ℂ) + 1) * verticalTerm (fun n => c (n + 1)) m z.

Equations

• NavierStokes.AxisHolomorphic.verticalX c m z = (↑m + 1) * NavierStokes.AxisHolomorphic.verticalTerm (fun (n : ℕ) => c (n + 1)) m z

noncomputable def NavierStokes.AxisHolomorphic.verticalY (c : ℕ → ℝ → ℝ) (m : ℕ) (z : ℂ) : ℂ

Vertical Y, with branches according to m = 0.

Equations

• NavierStokes.AxisHolomorphic.verticalY c m z = if m = 0 then 0 else Complex.I * NavierStokes.AxisHolomorphic.verticalX c (m - 1) z

@[simp]

theorem NavierStokes.AxisHolomorphic.verticalY_zero (c : ℕ → ℝ → ℝ) (z : ℂ) : verticalY c 0 z = 0

@[simp]

theorem NavierStokes.AxisHolomorphic.verticalY_succ (c : ℕ → ℝ → ℝ) (m : ℕ) (z : ℂ) : verticalY c (m + 1) z = Complex.I * verticalX c m z

noncomputable def NavierStokes.AxisHolomorphic.verticalExtension (c : ℕ → ℝ → ℝ) (z : ℂ) : ℂ

The actual complex extension, defined by a Taylor series in the imaginary direction.

Equations

• NavierStokes.AxisHolomorphic.verticalExtension c z = ∑' (m : ℕ), NavierStokes.AxisHolomorphic.verticalTerm c m z

theorem NavierStokes.AxisHolomorphic.verticalExtension_ofReal (c : ℕ → ℝ → ℝ) (x : ℝ) : verticalExtension c ↑x = ↑(c 0 x)

theorem NavierStokes.AxisHolomorphic.verticalTerm_hasFDerivAt {c : ℕ → ℝ → ℝ} {z : ℂ} (m : ℕ) (hc : ∀ (n : ℕ), HasDerivAt (c n) ((↑n + 1) * c (n + 1) z.re) z.re) : HasFDerivAt (verticalTerm c m) (complexLinearForm (verticalX c m z) (verticalY c m z)) z

theorem NavierStokes.AxisHolomorphic.verticalTerm_bound {c : ℕ → ℝ → ℝ} {C a : ℝ} (hC : 0 ≤ C) (ha : 0 < a) {z : ℂ} (hz : |z.im| ≤ a / 2) (hc : ∀ (n : ℕ), ‖c n z.re‖ ≤ C * a⁻¹ ^ n) (m : ℕ) : ‖verticalTerm c m z‖ ≤ C * (1 / 2) ^ m

theorem NavierStokes.AxisHolomorphic.verticalX_bound {c : ℕ → ℝ → ℝ} {C a : ℝ} (hC : 0 ≤ C) (ha : 0 < a) {z : ℂ} (hz : |z.im| ≤ a / 2) (hc : ∀ (n : ℕ), ‖c n z.re‖ ≤ C * a⁻¹ ^ n) (m : ℕ) : ‖verticalX c m z‖ ≤ C / a * (↑m + 1) * (1 / 2) ^ m

theorem NavierStokes.AxisHolomorphic.verticalY_bound {c : ℕ → ℝ → ℝ} {C a : ℝ} (hC : 0 ≤ C) (ha : 0 < a) {z : ℂ} (hz : |z.im| ≤ a / 2) (hc : ∀ (n : ℕ), ‖c n z.re‖ ≤ C * a⁻¹ ^ n) (m : ℕ) : ‖verticalY c m z‖ ≤ 2 * (C / a * (↑m + 1) * (1 / 2) ^ m)

theorem NavierStokes.AxisHolomorphic.summable_verticalTerm {c : ℕ → ℝ → ℝ} {C a : ℝ} (hC : 0 ≤ C) (ha : 0 < a) {z : ℂ} (hz : |z.im| ≤ a / 2) (hc : ∀ (n : ℕ), ‖c n z.re‖ ≤ C * a⁻¹ ^ n) : Summable fun (m : ℕ) => verticalTerm c m z

theorem NavierStokes.AxisHolomorphic.summable_verticalX {c : ℕ → ℝ → ℝ} {C a : ℝ} (hC : 0 ≤ C) (ha : 0 < a) {z : ℂ} (hz : |z.im| ≤ a / 2) (hc : ∀ (n : ℕ), ‖c n z.re‖ ≤ C * a⁻¹ ^ n) : Summable fun (m : ℕ) => verticalX c m z

theorem NavierStokes.AxisHolomorphic.summable_verticalY {c : ℕ → ℝ → ℝ} {C a : ℝ} (hC : 0 ≤ C) (ha : 0 < a) {z : ℂ} (hz : |z.im| ≤ a / 2) (hc : ∀ (n : ℕ), ‖c n z.re‖ ≤ C * a⁻¹ ^ n) : Summable fun (m : ℕ) => verticalY c m z

theorem NavierStokes.AxisHolomorphic.verticalY_tsum {c : ℕ → ℝ → ℝ} {z : ℂ} (hX : Summable fun (m : ℕ) => verticalX c m z) (hY : Summable fun (m : ℕ) => verticalY c m z) : ∑' (m : ℕ), verticalY c m z = Complex.I * ∑' (m : ℕ), verticalX c m z

The Cauchy--Riemann identity is an exact shift of the convergent Taylor series.

theorem NavierStokes.AxisHolomorphic.verticalExtension_hasDerivAt (I : AxisCoefficientSpace.Window) {c : ℕ → ℝ → ℝ} {C a : ℝ} (hC : 0 ≤ C) (ha : 0 < a) (hderiv : ∀ (m : ℕ), ∀ x ∈ Set.Ioo I.left I.right, HasDerivAt (c m) ((↑m + 1) * c (m + 1) x) x) (hbound : ∀ (m : ℕ), ∀ x ∈ Set.Ioo I.left I.right, ‖c m x‖ ≤ C * a⁻¹ ^ m) {z : ℂ} (hz : z ∈ parameterStrip I a) : HasDerivAt (verticalExtension c) (∑' (m : ℕ), verticalX c m z) z

Summing the actual real derivatives gives the complex derivative of the vertical Taylor series. No analytic continuation is assumed.

theorem NavierStokes.AxisHolomorphic.verticalExtension_analytic (I : AxisCoefficientSpace.Window) {c : ℕ → ℝ → ℝ} {C a : ℝ} (hC : 0 ≤ C) (ha : 0 < a) (hderiv : ∀ (m : ℕ), ∀ x ∈ Set.Ioo I.left I.right, HasDerivAt (c m) ((↑m + 1) * c (m + 1) x) x) (hbound : ∀ (m : ℕ), ∀ x ∈ Set.Ioo I.left I.right, ‖c m x‖ ≤ C * a⁻¹ ^ m) : AnalyticOnNhd ℂ (verticalExtension c) (parameterStrip I a)

theorem NavierStokes.AxisHolomorphic.verticalExtension_bound {c : ℕ → ℝ → ℝ} {C a : ℝ} (hC : 0 ≤ C) (ha : 0 < a) {z : ℂ} (hz : |z.im| ≤ a / 2) (hbound : ∀ (m : ℕ), ‖c m z.re‖ ≤ C * a⁻¹ ^ m) : ‖verticalExtension c z‖ ≤ 2 * C

noncomputable def NavierStokes.AxisHolomorphic.normalizedJet (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) (Y : ℝ) (m : ℕ) (x : ℝ) : ℝ

The actual parameter jets of the evaluated profile, divided by their factorials.

Equations

• NavierStokes.AxisHolomorphic.normalizedJet I ε A k Y m x = NavierStokes.AxisEvaluation.mixedSeries I ε A k m (Y, x) / ↑m.factorial

noncomputable def NavierStokes.AxisHolomorphic.jetConstant (R s : ℝ) (k : ℕ) : ℝ

Jet constant, given by geometricMoment (R / 20 / s) k / (1 - s).

Equations

• NavierStokes.AxisHolomorphic.jetConstant R s k = NavierStokes.AxisHolomorphic.geometricMoment (R / 20 / s) k / (1 - s)

theorem NavierStokes.AxisHolomorphic.jetConstant_nonneg {R s : ℝ} (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (k : ℕ) : 0 ≤ jetConstant R s k

theorem NavierStokes.AxisHolomorphic.normalizedJet_bound (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {Y : ℝ} (hY : |Y| ≤ R) (x : ℝ) : ‖normalizedJet I ε A k Y m x‖ ≤ jetConstant R s k * ‖A‖ * (ε * (1 - s))⁻¹ ^ m

theorem NavierStokes.AxisHolomorphic.normalizedJet_hasDerivAt_eta (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {Y x : ℝ} (hY : |Y| < 20) (hx : x ∈ Set.Ioo I.left I.right) : HasDerivAt (normalizedJet I ε A k Y m) ((↑m + 1) * normalizedJet I ε A k Y (m + 1) x) x

theorem NavierStokes.AxisHolomorphic.normalizedJet_hasDerivAt_Y (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {Y x : ℝ} (hY : |Y| < 20) (hx : x ∈ Set.Ioo I.left I.right) : HasDerivAt (fun (y : ℝ) => normalizedJet I ε A k y m x) (normalizedJet I ε A (k + 1) Y m x) Y

noncomputable def NavierStokes.AxisHolomorphic.complexProfile (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) (Y : ℝ) : ℂ → ℂ

The complex extension of the kth genuine radial derivative.

Equations

• NavierStokes.AxisHolomorphic.complexProfile I ε A k Y = NavierStokes.AxisHolomorphic.verticalExtension (NavierStokes.AxisHolomorphic.normalizedJet I ε A k Y)

theorem NavierStokes.AxisHolomorphic.complexProfile_ofReal (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) (Y x : ℝ) : complexProfile I ε A k Y ↑x = ↑(AxisEvaluation.mixedSeries I ε A k 0 (Y, x))

theorem NavierStokes.AxisHolomorphic.complexProfile_zero_ofReal (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (Y x : ℝ) : complexProfile I ε A 0 Y ↑x = ↑(AxisEvaluation.profile I ε A (Y, x))

theorem NavierStokes.AxisHolomorphic.complexProfile_analytic (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) {Y : ℝ} (hY : |Y| ≤ R) : AnalyticOnNhd ℂ (complexProfile I ε A k Y) (parameterStrip I (ε * (1 - s)))

Holomorphy of every fixed radial derivative, on one common parameter strip.

theorem NavierStokes.AxisHolomorphic.complexProfile_bound (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) {Y : ℝ} (hY : |Y| ≤ R) {z : ℂ} (hz : |z.im| ≤ ε * (1 - s) / 2) : ‖complexProfile I ε A k Y z‖ ≤ 2 * jetConstant R s k * ‖A‖

The bound is linear in the coefficient norm; the constant and strip width are independent of the particular solved coefficient vector.

theorem NavierStokes.AxisHolomorphic.verticalTerm_hasDerivAt_Y (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {Y : ℝ} {z : ℂ} (hY : |Y| < 20) (hz : z.re ∈ Set.Ioo I.left I.right) : HasDerivAt (fun (y : ℝ) => verticalTerm (normalizedJet I ε A k y) m z) (verticalTerm (normalizedJet I ε A (k + 1) Y) m z) Y

theorem NavierStokes.AxisHolomorphic.complexProfile_hasDerivAt_Y (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) {Y : ℝ} (hY : |Y| < R) {z : ℂ} (hz : z ∈ parameterStrip I (ε * (1 - s))) : HasDerivAt (fun (y : ℝ) => complexProfile I ε A k y z) (complexProfile I ε A (k + 1) Y z) Y

Radial differentiation commutes with the constructed complex extension.

theorem NavierStokes.AxisHolomorphic.complexProfile_iteratedDeriv_Y (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k r : ℕ) {Y : ℝ} (hY : |Y| < R) {z : ℂ} (hz : z ∈ parameterStrip I (ε * (1 - s))) : iteratedDeriv r (fun (y : ℝ) => complexProfile I ε A k y z) Y = complexProfile I ε A (k + r) Y z

Every member of the holomorphic family is the actual corresponding radial derivative.

theorem NavierStokes.AxisHolomorphic.complexProfile_iteratedDeriv_ofReal (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k m : ℕ) {Y x : ℝ} (hY : |Y| ≤ R) (hx : x ∈ Set.Ioo I.left I.right) : iteratedDeriv m (complexProfile I ε A k Y) ↑x = ↑(AxisEvaluation.mixedSeries I ε A k m (Y, x))

On the real axis, every genuine complex derivative is the corresponding already constructed compatible parameter jet.

noncomputable def NavierStokes.AxisHolomorphic.parameterTube (J : AxisCoefficientSpace.Window) (δ : ℝ) : Set ℂ

The open complex tube around a closed real window.

Equations

• NavierStokes.AxisHolomorphic.parameterTube J δ = {z : ℂ | ∃ x ∈ J.interval, dist z ↑x < δ}

theorem NavierStokes.AxisHolomorphic.parameterTube_contains_real (J : AxisCoefficientSpace.Window) {δ : ℝ} (hδ : 0 < δ) {x : ℝ} (hx : x ∈ J.interval) : ↑x ∈ parameterTube J δ

theorem NavierStokes.AxisHolomorphic.exists_parameterTube_subset (I J : AxisCoefficientSpace.Window) (hleft : I.left < J.left) (hright : J.right < I.right) {a : ℝ} (ha : 0 < a) : ∃ (δ : ℝ), 0 < δ ∧ parameterTube J δ ⊆ parameterStrip I a

Strict containment of real windows supplies a positive complex tube in the strip. Its width does not depend on any coefficient vector or derivative order.

theorem NavierStokes.AxisHolomorphic.exists_common_holomorphic_extension (I J : AxisCoefficientSpace.Window) (hleft : I.left < J.left) (hright : J.right < I.right) {ε R : ℝ} (hε : 0 < ε) (hR20 : R < 20) : ∃ (δ : ℝ), 0 < δ ∧ ∃ (B : ℕ → ℝ), (∀ (k : ℕ), 0 ≤ B k) ∧ ∀ (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (Y : ℝ), |Y| ≤ R → ∀ (k : ℕ), AnalyticOnNhd ℂ (complexProfile I ε A k Y) (parameterTube J δ) ∧ (∀ z ∈ parameterTube J δ, ‖complexProfile I ε A k Y z‖ ≤ B k * ‖A‖) ∧ (∀ z ∈ parameterTube J δ, iteratedDeriv k (fun (y : ℝ) => complexProfile I ε A 0 y z) Y = complexProfile I ε A k Y z) ∧ ∀ (m : ℕ), ∀ x ∈ J.interval, iteratedDeriv m (complexProfile I ε A k Y) ↑x = ↑(AxisEvaluation.mixedSeries I ε A k m (Y, x))

A common, explicitly constructed holomorphic extension exists on a positive tube over every strictly smaller real window and compact radial interval.

The tube and all bound constants are chosen before the coefficient vector. Every radial derivative uses this same tube, and all complex parameter jets match the genuine real jets.

Joint smoothness of the actual holomorphic axis profile

The uniform bounds for the next radial derivative imply continuity in the supremum norm on every closed parameter disk. A uniform mean-value remainder then identifies the actual derivative of the disk-valued curve. Iterating this argument and using the fixed-contour holomorphic-family theorem proves joint real smoothness of the constructed extension.

theorem NavierStokes.AxisHolomorphicJoint.hasDerivAt_compactFamily {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : Set ℝ} (hS : IsOpen S) (V V' : ℝ → C(K, E)) (hc : ContinuousOn V' S) (hd : ∀ y ∈ S, ∀ (z : K), HasDerivAt (fun (q : ℝ) => (V q) z) ((V' y) z) y) {y : ℝ} (hy : y ∈ S) : HasDerivAt V (V' y) y

A continuous derivative in the supremum norm and the actual coordinate derivatives give the actual derivative of a compact-family curve.

noncomputable def NavierStokes.AxisHolomorphicJoint.diskProfile (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (c : ℂ) (σ : ℝ) (k : ℕ) : ℝ → C(CauchyRestriction.Disk c σ, ℂ)

The actual holomorphic profile restricted to a closed parameter disk. The zero fallback in family is used only outside the proved radial domain.

Equations

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

theorem NavierStokes.AxisHolomorphicJoint.diskProfile_apply (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (c : ℂ) (σ : ℝ) (hK : Metric.closedBall c σ ⊆ AxisHolomorphic.parameterStrip I (ε * (1 - s))) (k : ℕ) {Y : ℝ} (hY : |Y| ≤ R) (z : CauchyRestriction.Disk c σ) : (diskProfile I ε A c σ k Y) z = AxisHolomorphic.complexProfile I ε A k Y ↑z

theorem NavierStokes.AxisHolomorphicJoint.diskProfile_norm_sub_le (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (c : ℂ) (σ : ℝ) (hK : Metric.closedBall c σ ⊆ AxisHolomorphic.parameterStrip I (ε * (1 - s))) (k : ℕ) {Y Y' : ℝ} (hY : |Y| < R) (hY' : |Y'| < R) : ‖diskProfile I ε A c σ k Y' - diskProfile I ε A c σ k Y‖ ≤ 2 * AxisHolomorphic.jetConstant R s (k + 1) * ‖A‖ * ‖Y' - Y‖

The next radial derivative controls a whole disk in the supremum norm.

theorem NavierStokes.AxisHolomorphicJoint.diskProfile_continuousOn (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (c : ℂ) (σ : ℝ) (hK : Metric.closedBall c σ ⊆ AxisHolomorphic.parameterStrip I (ε * (1 - s))) (k : ℕ) : ContinuousOn (diskProfile I ε A c σ k) (Set.Ioo (-R) R)

theorem NavierStokes.AxisHolomorphicJoint.diskProfile_hasDerivAt (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (c : ℂ) (σ : ℝ) (hK : Metric.closedBall c σ ⊆ AxisHolomorphic.parameterStrip I (ε * (1 - s))) (k : ℕ) {Y : ℝ} (hY : |Y| < R) : HasDerivAt (diskProfile I ε A c σ k) (diskProfile I ε A c σ (k + 1) Y) Y

The derivative in the disk supremum norm is the already constructed next radial derivative, with no regularity assumption on the output family.

theorem NavierStokes.AxisHolomorphicJoint.diskProfile_contDiffOn_nat (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (c : ℂ) (σ : ℝ) (hK : Metric.closedBall c σ ⊆ AxisHolomorphic.parameterStrip I (ε * (1 - s))) (n k : ℕ) : ContDiffOn ℝ (↑n) (diskProfile I ε A c σ k) (Set.Ioo (-R) R)

theorem NavierStokes.AxisHolomorphicJoint.diskProfile_contDiffOn (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (c : ℂ) (σ : ℝ) (hK : Metric.closedBall c σ ⊆ AxisHolomorphic.parameterStrip I (ε * (1 - s))) (k : ℕ) : ContDiffOn ℝ (↑⊤) (diskProfile I ε A c σ k) (Set.Ioo (-R) R)

theorem NavierStokes.AxisHolomorphicJoint.complexProfile_joint_smooth (I : AxisCoefficientSpace.Window) {ε R s : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => AxisHolomorphic.complexProfile I ε A k p.1 p.2) (Set.Ioo (-R) R ×ˢ AxisHolomorphic.parameterStrip I (ε * (1 - s)))

Genuine joint real smoothness of every radial jet of the holomorphic axis profile on the same radial interval and the same parameter strip.

theorem NavierStokes.AxisHolomorphicJoint.complexProfile_joint_smooth_tube (I J : AxisCoefficientSpace.Window) {ε R s δ : ℝ} (hε : 0 < ε) (hR : 1 ≤ R) (hs : R / 20 < s) (hs1 : s < 1) (htube : AxisHolomorphic.parameterTube J δ ⊆ AxisHolomorphic.parameterStrip I (ε * (1 - s))) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => AxisHolomorphic.complexProfile I ε A k p.1 p.2) (Set.Ioo (-R) R ×ˢ AxisHolomorphic.parameterTube J δ)

Every tube contained in the constructed strip inherits joint smoothness.

theorem NavierStokes.AxisHolomorphicJoint.complexProfile_joint_real_agreement (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ) (Y x : ℝ) : AxisHolomorphic.complexProfile I ε A k Y ↑x = ↑(AxisEvaluation.mixedSeries I ε A k 0 (Y, x))

The jointly smooth extension is exactly the original real radial jet on the real slice, rather than a separately selected continuation.

theorem NavierStokes.AxisHolomorphicJoint.complexProfile_joint_zero_real_agreement (I : AxisCoefficientSpace.Window) (ε : ℝ) (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (Y x : ℝ) : AxisHolomorphic.complexProfile I ε A 0 Y ↑x = ↑(AxisEvaluation.profile I ε A (Y, x))

theorem NavierStokes.AxisHolomorphicJoint.exists_common_joint_extension (I J : AxisCoefficientSpace.Window) (hleft : I.left < J.left) (hright : J.right < I.right) {ε R : ℝ} (hε : 0 < ε) (hR20 : R < 20) : ∃ (δ : ℝ), 0 < δ ∧ ∃ (S : ℝ), R < S ∧ S < 20 ∧ ∃ (B : ℕ → ℝ), (∀ (k : ℕ), 0 ≤ B k) ∧ ∀ (A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (k : ℕ), ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => AxisHolomorphic.complexProfile I ε A k p.1 p.2) (Set.Ioo (-S) S ×ˢ AxisHolomorphic.parameterTube J δ) ∧ ∀ (Y : ℝ), |Y| ≤ R → AnalyticOnNhd ℂ (AxisHolomorphic.complexProfile I ε A k Y) (AxisHolomorphic.parameterTube J δ) ∧ (∀ z ∈ AxisHolomorphic.parameterTube J δ, ‖AxisHolomorphic.complexProfile I ε A k Y z‖ ≤ B k * ‖A‖) ∧ (∀ z ∈ AxisHolomorphic.parameterTube J δ, iteratedDeriv k (fun (y : ℝ) => AxisHolomorphic.complexProfile I ε A 0 y z) Y = AxisHolomorphic.complexProfile I ε A k Y z) ∧ ∀ (m : ℕ), ∀ x ∈ J.interval, iteratedDeriv m (AxisHolomorphic.complexProfile I ε A k Y) ↑x = ↑(AxisEvaluation.mixedSeries I ε A k m (Y, x))

A common positive tube and a genuine open radial neighborhood work for every coefficient vector and every radial derivative order. The extension is jointly real smooth, holomorphic in the complex parameter, uniformly bounded, and agrees with all actual real parameter jets.

A common holomorphic parameter neighborhood through initial activation

All continuations below are explicit integrals of the actual natural slopes. The complex neighborhood is obtained from compactness and real positivity.

@[reducible, inline]

abbrev NavierStokes.ActivationHolomorphic.CPoint : Type

C point: an abbreviation for ℝ × ℂ.

Equations

• NavierStokes.ActivationHolomorphic.CPoint = (ℝ × ℂ)

@[reducible, inline]

abbrev NavierStokes.ActivationHolomorphic.CField : Type

C field: an abbreviation for CPoint → ℂ.

Equations

• NavierStokes.ActivationHolomorphic.CField = (NavierStokes.ActivationHolomorphic.CPoint → ℂ)

noncomputable def NavierStokes.ActivationHolomorphic.radial (F : CField) (p : CPoint) : ℂ

Radial, given by deriv (fun x => F (x, p.2)) p.1.

Equations

• NavierStokes.ActivationHolomorphic.radial F p = deriv (fun (x : ℝ) => F (x, p.2)) p.1

structure NavierStokes.ActivationHolomorphic.Regular (S : Set ℝ) (Ω : Set ℂ) (F : CField) : Prop

Joint real smoothness and actual holomorphic parameter slices.

• smooth : ContDiffOn ℝ (↑⊤) F (S ×ˢ Ω)
• holomorphic (x : ℝ) : x ∈ S → DifferentiableOn ℂ (fun (z : ℂ) => F (x, z)) Ω

theorem NavierStokes.ActivationHolomorphic.radial_smooth {S : Set ℝ} {Ω : Set ℂ} (hS : IsOpen S) (hΩ : IsOpen Ω) {F : CField} (hF : ContDiffOn ℝ (↑⊤) F (S ×ˢ Ω)) : ContDiffOn ℝ (↑⊤) (radial F) (S ×ˢ Ω)

theorem NavierStokes.ActivationHolomorphic.radial_holomorphic {S : Set ℝ} {Ω : Set ℂ} (hS : IsOpen S) (hΩ : IsOpen Ω) {F : CField} (hF : ContDiffOn ℝ (↑⊤) F (S ×ˢ Ω)) (hhol : ∀ r ∈ S, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) Ω) {r : ℝ} (hr : r ∈ S) : DifferentiableOn ℂ (fun (z : ℂ) => radial F (r, z)) Ω

Radial differentiation preserves holomorphy on an arbitrary open radial domain. The difference quotients converge uniformly on each compact disk.

theorem NavierStokes.ActivationHolomorphic.Regular.radial {S : Set ℝ} {Ω : Set ℂ} {F : CField} (hF : Regular S Ω F) (hS : IsOpen S) (hΩ : IsOpen Ω) : Regular S Ω (ActivationHolomorphic.radial F)

theorem NavierStokes.ActivationHolomorphic.Regular.mono {S S' : Set ℝ} {Ω Ω' : Set ℂ} {F : CField} (hF : Regular S Ω F) (hS : S' ⊆ S) (hΩ : Ω' ⊆ Ω) : Regular S' Ω' F

theorem NavierStokes.ActivationHolomorphic.regular_const (S : Set ℝ) (Ω : Set ℂ) (c : ℂ) : Regular S Ω fun (x : CPoint) => c

theorem NavierStokes.ActivationHolomorphic.Regular.add {S : Set ℝ} {Ω : Set ℂ} {F G : CField} (hF : Regular S Ω F) (hG : Regular S Ω G) : Regular S Ω fun (p : CPoint) => F p + G p

theorem NavierStokes.ActivationHolomorphic.Regular.mul {S : Set ℝ} {Ω : Set ℂ} {F G : CField} (hF : Regular S Ω F) (hG : Regular S Ω G) : Regular S Ω fun (p : CPoint) => F p * G p

theorem NavierStokes.ActivationHolomorphic.Regular.cexp {S : Set ℝ} {Ω : Set ℂ} {F : CField} (hF : Regular S Ω F) : Regular S Ω fun (p : CPoint) => Complex.exp (F p)

theorem NavierStokes.ActivationHolomorphic.Regular.clog {S : Set ℝ} {Ω : Set ℂ} {F : CField} (hF : Regular S Ω F) (hne : ∀ p ∈ S ×ˢ Ω, F p ∈ Complex.slitPlane) : Regular S Ω fun (p : CPoint) => Complex.log (F p)

theorem NavierStokes.ActivationHolomorphic.regular_parameter {S : Set ℝ} {Ω : Set ℂ} {g : ℂ → ℂ} (hg : AnalyticOnNhd ℂ g Ω) : Regular S Ω fun (p : CPoint) => g p.2

theorem NavierStokes.ActivationHolomorphic.regular_radius {S : Set ℝ} {Ω : Set ℂ} {g : ℝ → ℝ} (hg : ContDiffOn ℝ (↑⊤) g S) : Regular S Ω fun (p : CPoint) => ↑(g p.1)

theorem NavierStokes.ActivationHolomorphic.compact_integral_smooth {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] [ProperSpace H] {s : Set H} {G : H × ℝ → ℂ} (hs : IsOpen s) (hG : ∀ p ∈ s, ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑⊤) G (p, t)) : ContDiffOn ℝ (↑⊤) (fun (p : H) => ∫ (t : ℝ) in 0..1, G (p, t)) s

@[reducible, inline]

abbrev NavierStokes.ActivationHolomorphic.Segment : Type

Segment: an abbreviation for ↥(Icc (0 : ℝ) 1).

Equations

• NavierStokes.ActivationHolomorphic.Segment = ↑(Set.Icc 0 1)

noncomputable def NavierStokes.ActivationHolomorphic.segmentExtend (f : C(Segment, ℂ)) (t : ℝ) : ℂ

Segment extend, given by f (projIcc 0 1 zero_le_one t).

Equations

• NavierStokes.ActivationHolomorphic.segmentExtend f t = f (Set.projIcc 0 1 NavierStokes.ActivationHolomorphic.segmentExtend._proof_1 t)

theorem NavierStokes.ActivationHolomorphic.segmentExtend_continuous (f : C(Segment, ℂ)) : Continuous (segmentExtend f)

theorem NavierStokes.ActivationHolomorphic.segmentIntegral_norm (f : C(Segment, ℂ)) : ‖∫ (t : ℝ) in 0..1, segmentExtend f t‖ ≤ 1 * ‖f‖

noncomputable def NavierStokes.ActivationHolomorphic.segmentIntegral : C(Segment, ℂ) →L[ℂ] ℂ

Segment integral, constructed using LinearMap.mkContinuous.

Equations

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

theorem NavierStokes.ActivationHolomorphic.compact_integral_holomorphic {Ω : Set ℂ} (hΩ : IsOpen Ω) {G : ℂ × ℝ → ℂ} (hG : ∀ z ∈ Ω, ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑⊤) G (z, t)) (hhol : ∀ t ∈ Set.Icc 0 1, DifferentiableOn ℂ (fun (z : ℂ) => G (z, t)) Ω) : DifferentiableOn ℂ (fun (z : ℂ) => ∫ (t : ℝ) in 0..1, G (z, t)) Ω

Holomorphic integration only requires smoothness near the actual compact integration segment, with no assumptions outside that segment.

noncomputable def NavierStokes.ActivationHolomorphic.average (F : CField) (p : CPoint) : ℂ

Average, given by ∫ t in (0 : ℝ)..1, F (t*p.1,p.2).

Equations

• NavierStokes.ActivationHolomorphic.average F p = ∫ (t : ℝ) in 0..1, F (t * p.1, p.2)

noncomputable def NavierStokes.ActivationHolomorphic.primitive (F : CField) (p : CPoint) : ℂ

Primitive, given by ∫ x in (0 : ℝ)..p.1, F (x,p.2).

Equations

• NavierStokes.ActivationHolomorphic.primitive F p = ∫ (x : ℝ) in 0..p.1, F (x, p.2)

theorem NavierStokes.ActivationHolomorphic.primitive_eq_mul_average (F : CField) (p : CPoint) : primitive F p = ↑p.1 * average F p

theorem NavierStokes.ActivationHolomorphic.Regular.average {S : Set ℝ} {Ω : Set ℂ} {F : CField} (hF : Regular S Ω F) (hS : IsOpen S) (hΩ : IsOpen Ω) (hscale : ∀ x ∈ S, ∀ t ∈ Set.Icc 0 1, t * x ∈ S) : Regular S Ω (ActivationHolomorphic.average F)

theorem NavierStokes.ActivationHolomorphic.Regular.primitive {S : Set ℝ} {Ω : Set ℂ} {F : CField} (hF : Regular S Ω F) (hS : IsOpen S) (hΩ : IsOpen Ω) (hscale : ∀ x ∈ S, ∀ t ∈ Set.Icc 0 1, t * x ∈ S) : Regular S Ω (ActivationHolomorphic.primitive F)

theorem NavierStokes.ActivationHolomorphic.radial_hasDerivAt {S : Set ℝ} {Ω : Set ℂ} {F : CField} (hS : IsOpen S) (hΩ : IsOpen Ω) (hF : ContDiffOn ℝ (↑⊤) F (S ×ˢ Ω)) {p : CPoint} (hp : p ∈ S ×ˢ Ω) : HasDerivAt (fun (x : ℝ) => F (x, p.2)) (radial F p) p.1

theorem NavierStokes.ActivationHolomorphic.slice_continuous {Ω : Set ℂ} {F : CField} (hΩ : IsOpen Ω) (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Ω)) {z : ℂ} (hz : z ∈ Ω) : Continuous fun (x : ℝ) => F (x, z)

theorem NavierStokes.ActivationHolomorphic.primitive_hasDerivAt {Ω : Set ℂ} {F : CField} (hΩ : IsOpen Ω) (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Ω)) {p : CPoint} (hp : p.2 ∈ Ω) : HasDerivAt (fun (x : ℝ) => primitive F (x, p.2)) (F p) p.1

noncomputable def NavierStokes.ActivationHolomorphic.dampedSlope (δ : ℝ) (G : CField) (p : CPoint) : ℂ

Damped slope, given by (ReferencePath.slopeCutoff δ p.1 : ℂ) * radial G p.

Equations

• NavierStokes.ActivationHolomorphic.dampedSlope δ G p = ↑(NavierStokes.ReferencePath.slopeCutoff δ p.1) * NavierStokes.ActivationHolomorphic.radial G p

noncomputable def NavierStokes.ActivationHolomorphic.continuation (δ : ℝ) (G : CField) (p : CPoint) : ℂ

Continuation, given by G (0,p.2) + primitive (dampedSlope δ G) p.

Equations

• NavierStokes.ActivationHolomorphic.continuation δ G p = G (0, p.2) + NavierStokes.ActivationHolomorphic.primitive (NavierStokes.ActivationHolomorphic.dampedSlope δ G) p

theorem NavierStokes.ActivationHolomorphic.regular_dampedSlope {T δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < T) {Ω : Set ℂ} (hΩ : IsOpen Ω) {G : CField} (hG : Regular (Set.Iio T) Ω G) : Regular Set.univ Ω (dampedSlope δ G)

theorem NavierStokes.ActivationHolomorphic.regular_continuation {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < T) {Ω : Set ℂ} (hΩ : IsOpen Ω) {G : CField} (hG : Regular (Set.Iio T) Ω G) : Regular Set.univ Ω (continuation δ G)

theorem NavierStokes.ActivationHolomorphic.continuation_hasDerivAt {T δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < T) {Ω : Set ℂ} (hΩ : IsOpen Ω) {G : CField} (hG : Regular (Set.Iio T) Ω G) {p : CPoint} (hp : p.2 ∈ Ω) : HasDerivAt (fun (x : ℝ) => continuation δ G (x, p.2)) (dampedSlope δ G p) p.1

theorem NavierStokes.ActivationHolomorphic.continuation_eq_initial {T δ : ℝ} : 0 < T → ∀ (hδ : 0 < δ) (hδT : 2 * δ < T) {Ω : Set ℂ} (hΩ : IsOpen Ω) {G : CField} (hG : Regular (Set.Iio T) Ω G) {p : CPoint} (hp : p.2 ∈ Ω) (hx : p.1 ≤ δ), continuation δ G p = G p

noncomputable def NavierStokes.ActivationHolomorphic.controlled (T κ : ℝ) (G : CField) (p : CPoint) : ℂ

Controlled, given by `G (0,p.2) + primitive (fun q => (StressActivation.damping T κ q.1 : ℂ)

• radial G q) p`.

Equations

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

theorem NavierStokes.ActivationHolomorphic.regular_controlled (T κ : ℝ) {Ω : Set ℂ} (hΩ : IsOpen Ω) {G : CField} (hG : Regular Set.univ Ω G) : Regular Set.univ Ω (controlled T κ G)

theorem NavierStokes.ActivationHolomorphic.controlled_eq_initial {T : ℝ} (hT : 0 < T) (κ : ℝ) {Ω : Set ℂ} (hΩ : IsOpen Ω) {G : CField} (hG : Regular Set.univ Ω G) {p : CPoint} (hp : p.2 ∈ Ω) (hx : p.1 ≤ 0) : controlled T κ G p = G p

theorem NavierStokes.ActivationHolomorphic.radial_ofReal {S : Set ℝ} (hS : IsOpen S) {G : CField} {g : ProfileHistories.Field} {x η : ℝ} (hx : x ∈ S) (hg : ContDiffAt ℝ (↑⊤) g (x, η)) (heq : ∀ y ∈ S, G (y, ↑η) = ↑(g (y, η))) : radial G (x, ↑η) = ↑(ProfileHistories.radialPartial g (x, η))

theorem NavierStokes.ActivationHolomorphic.continuation_ofReal {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < T) {J : Set ℝ} (hJ : IsOpen J) {G : CField} {g : ProfileHistories.Field} (hg : ContDiffOn ℝ (↑⊤) g (Set.Iio T ×ˢ J)) (heq : ∀ x < T, ∀ η ∈ J, G (x, ↑η) = ↑(g (x, η))) (x : ℝ) {η : ℝ} (hη : η ∈ J) : continuation δ G (x, ↑η) = ↑(ReferencePath.continuation δ g (x, η))

theorem NavierStokes.ActivationHolomorphic.controlled_ofReal (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {G : CField} {g : ProfileHistories.Field} (hg : ContDiffOn ℝ (↑⊤) g (Set.univ ×ˢ J)) (heq : ∀ (x η : ℝ), η ∈ J → G (x, ↑η) = ↑(g (x, η))) (x : ℝ) {η : ℝ} (hη : η ∈ J) : controlled T κ G (x, ↑η) = ↑(StressActivation.controlled T κ g (x, η))

noncomputable def NavierStokes.ActivationHolomorphic.logPoint (N : ReferencePath.Input) (p : CPoint) : CPoint

Log point, given by (N.logTime p.1,p.2).

Equations

• NavierStokes.ActivationHolomorphic.logPoint N p = (N.logTime p.1, p.2)

noncomputable def NavierStokes.ActivationHolomorphic.expPoint (N : ReferencePath.Input) (p : CPoint) : CPoint

Exp point, given by (N.endpoint*Real.exp p.1,p.2).

Equations

• NavierStokes.ActivationHolomorphic.expPoint N p = (N.endpoint * Real.exp p.1, p.2)

theorem NavierStokes.ActivationHolomorphic.logPoint_smoothAt (N : ReferencePath.Input) {p : CPoint} (hp : 0 < p.1) : ContDiffAt ℝ (↑⊤) (logPoint N) p

theorem NavierStokes.ActivationHolomorphic.expPoint_smooth (N : ReferencePath.Input) : ContDiff ℝ (↑⊤) (expPoint N)

theorem NavierStokes.ActivationHolomorphic.expPoint_logPoint (N : ReferencePath.Input) {p : CPoint} (hp : 0 < p.1) : expPoint N (logPoint N p) = p

noncomputable def NavierStokes.ActivationHolomorphic.attach (N : ReferencePath.Input) (F G : CField) (p : CPoint) : ℂ

Attach, with branches according to p.1 ≤ N.endpoint.

Equations

• NavierStokes.ActivationHolomorphic.attach N F G p = if p.1 ≤ N.endpoint then F p else G (NavierStokes.ActivationHolomorphic.logPoint N p)

theorem NavierStokes.ActivationHolomorphic.attach_logPoint (N : ReferencePath.Input) {F G : CField} {Ω : Set ℂ} (heq : ∀ (p : CPoint), 0 < p.1 → p.1 ≤ N.endpoint → p.2 ∈ Ω → G (logPoint N p) = F p) {p : CPoint} (hp : 0 < p.1) (hz : p.2 ∈ Ω) : attach N F G p = G (logPoint N p)

theorem NavierStokes.ActivationHolomorphic.regular_attach (N : ReferencePath.Input) {R : ℝ} (hR : 0 < R) (hXR : N.endpoint < R) {Ω : Set ℂ} (hΩ : IsOpen Ω) {F G : CField} (hF : Regular (Set.Ioo (-R) R) Ω F) (hG : Regular Set.univ Ω G) (heq : ∀ (p : CPoint), 0 < p.1 → p.1 ≤ N.endpoint → p.2 ∈ Ω → G (logPoint N p) = F p) : Regular (Set.Ioi (-R)) Ω (attach N F G)

structure NavierStokes.ActivationHolomorphic.NaturalExtension (N : ReferencePath.Input) (Ω : Set ℂ) (R : ℝ) : Type

An explicit natural extension, including the positivity neighborhood needed by the logarithm. It is constructed from the coefficient series below.

• radius_pos : 0 < R
• endpoint_lt : N.endpoint < R
• f : CField

  F of NaturalExtension, of type CField.

• U : CField

  U of NaturalExtension, of type CField.

• f_regular : Regular (Set.Ioo (-R) R) Ω self.f
• U_regular : Regular (Set.Ioo (-R) R) Ω self.U
• f_real (x η : ℝ) : self.f (x, ↑η) = ↑(N.f (x, η))
• U_real (x η : ℝ) : self.U (x, ↑η) = ↑(N.U (x, η))
• exp_mem (t : ℝ) : t < ReferencePath.rampLimit → N.endpoint * Real.exp t ∈ Set.Ioo (-R) R
• right_half (t : ℝ) : t < ReferencePath.rampLimit → ∀ z ∈ Ω, 0 < (self.f (N.endpoint * Real.exp t, z)).re
• initial_half (x : ℝ) : x ∈ Set.Icc 0 N.endpoint → ∀ z ∈ Ω, 0 < (self.f (x, z)).re

noncomputable def NavierStokes.ActivationHolomorphic.NaturalExtension.logF {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) : CField

Log F, defined pointwise by Complex.log (E.f (expPoint N p)).

Equations

• E.logF p = Complex.log (E.f (NavierStokes.ActivationHolomorphic.expPoint N p))

noncomputable def NavierStokes.ActivationHolomorphic.NaturalExtension.logU {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) : CField

Log U, defined pointwise by E.U (expPoint N p).

Equations

• E.logU p = E.U (NavierStokes.ActivationHolomorphic.expPoint N p)

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.logF_regular {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) : Regular (Set.Iio ReferencePath.rampLimit) Ω E.logF

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.logU_regular {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) : Regular (Set.Iio ReferencePath.rampLimit) Ω E.logU

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.logF_real {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) {t η : ℝ} (ht : t < ReferencePath.rampLimit) (hη : η ∈ ReferencePath.parameterInterval) : E.logF (t, ↑η) = ↑(N.logF (t, η))

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.logU_real {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (t η : ℝ) : E.logU (t, ↑η) = ↑(N.logU (t, η))

noncomputable def NavierStokes.ActivationHolomorphic.NaturalExtension.refLog {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (δ : ℝ) : CField

Ref log, given by continuation δ E.logF.

Equations

• E.refLog δ = NavierStokes.ActivationHolomorphic.continuation δ E.logF

noncomputable def NavierStokes.ActivationHolomorphic.NaturalExtension.refAxial {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (δ : ℝ) : CField

Ref axial, given by continuation δ E.logU.

Equations

• E.refAxial δ = NavierStokes.ActivationHolomorphic.continuation δ E.logU

noncomputable def NavierStokes.ActivationHolomorphic.NaturalExtension.refF {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (δ : ℝ) : CField

Ref F, given by attach N E.f (fun p => Complex.exp (E.refLog δ p)).

Equations

• E.refF δ = NavierStokes.ActivationHolomorphic.attach N E.f fun (p : NavierStokes.ActivationHolomorphic.CPoint) => Complex.exp (E.refLog δ p)

noncomputable def NavierStokes.ActivationHolomorphic.NaturalExtension.refU {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (δ : ℝ) : CField

Ref U, given by attach N E.U (E.refAxial δ).

Equations

• E.refU δ = NavierStokes.ActivationHolomorphic.attach N E.U (E.refAxial δ)

noncomputable def NavierStokes.ActivationHolomorphic.NaturalExtension.actLog {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (T κ δ : ℝ) : CField

Act log, given by controlled T κ (E.refLog δ).

Equations

• E.actLog T κ δ = NavierStokes.ActivationHolomorphic.controlled T κ (E.refLog δ)

noncomputable def NavierStokes.ActivationHolomorphic.NaturalExtension.actAxial {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (T κ δ : ℝ) : CField

Act axial, given by controlled T κ (E.refAxial δ).

Equations

• E.actAxial T κ δ = NavierStokes.ActivationHolomorphic.controlled T κ (E.refAxial δ)

noncomputable def NavierStokes.ActivationHolomorphic.NaturalExtension.actF {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (T κ δ : ℝ) : CField

Act F, given by attach N E.f (fun p => Complex.exp (E.actLog T κ δ p)).

Equations

• E.actF T κ δ = NavierStokes.ActivationHolomorphic.attach N E.f fun (p : NavierStokes.ActivationHolomorphic.CPoint) => Complex.exp (E.actLog T κ δ p)

noncomputable def NavierStokes.ActivationHolomorphic.NaturalExtension.actU {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (T κ δ : ℝ) : CField

Act U, given by attach N E.U (E.actAxial T κ δ).

Equations

• E.actU T κ δ = NavierStokes.ActivationHolomorphic.attach N E.U (E.actAxial T κ δ)

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.refLog_regular {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (hΩ : IsOpen Ω) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) : Regular Set.univ Ω (E.refLog δ)

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.refAxial_regular {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (hΩ : IsOpen Ω) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) : Regular Set.univ Ω (E.refAxial δ)

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.refLog_initial {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (hΩ : IsOpen Ω) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : CPoint} (hp : p.2 ∈ Ω) (ht : p.1 ≤ 0) : E.refLog δ p = E.logF p

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.refAxial_initial {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (hΩ : IsOpen Ω) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : CPoint} (hp : p.2 ∈ Ω) (ht : p.1 ≤ 0) : E.refAxial δ p = E.logU p

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.angular_attach_regular {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (hΩ : IsOpen Ω) {G : CField} (hG : Regular Set.univ Ω G) (hinit : ∀ (p : CPoint), p.2 ∈ Ω → p.1 ≤ 0 → G p = E.logF p) : Regular (Set.Ioi (-R)) Ω (attach N E.f fun (p : CPoint) => Complex.exp (G p))

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.axial_attach_regular {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (hΩ : IsOpen Ω) {G : CField} (hG : Regular Set.univ Ω G) (hinit : ∀ (p : CPoint), p.2 ∈ Ω → p.1 ≤ 0 → G p = E.logU p) : Regular (Set.Ioi (-R)) Ω (attach N E.U G)

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.refF_regular {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (hΩ : IsOpen Ω) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) : Regular (Set.Ioi (-R)) Ω (E.refF δ)

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.refU_regular {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (hΩ : IsOpen Ω) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) : Regular (Set.Ioi (-R)) Ω (E.refU δ)

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.actF_regular {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (hΩ : IsOpen Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) : Regular (Set.Ioi (-R)) Ω (E.actF T κ δ)

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.actU_regular {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (hΩ : IsOpen Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) : Regular (Set.Ioi (-R)) Ω (E.actU T κ δ)

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.refLog_real {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (x : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : E.refLog δ (x, ↑η) = ↑(StressActivation.FromReference.refLog N δ (x, η))

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.refAxial_real {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (x : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : E.refAxial δ (x, ↑η) = ↑(StressActivation.FromReference.refAxial N δ (x, η))

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.actLog_real {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (T κ x : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : E.actLog T κ δ (x, ↑η) = ↑(StressActivation.controlled T κ (StressActivation.FromReference.refLog N δ) (x, η))

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.actAxial_real {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (T κ x : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : E.actAxial T κ δ (x, ↑η) = ↑(StressActivation.controlled T κ (StressActivation.FromReference.refAxial N δ) (x, η))

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.refF_real {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (x : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : E.refF δ (x, ↑η) = ↑(N.refF δ (x, η))

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.refU_real {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (x : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : E.refU δ (x, ↑η) = ↑(N.refU δ (x, η))

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.actF_real {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (T κ x : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : E.actF T κ δ (x, ↑η) = ↑(StressActivation.FromReference.f N T κ δ (x, η))

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.actU_real {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (T κ x : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : E.actU T κ δ (x, ↑η) = ↑(StressActivation.FromReference.U N T κ δ (x, η))

theorem NavierStokes.ActivationHolomorphic.NaturalExtension.actF_ne_zero {N : ReferencePath.Input} {Ω : Set ℂ} {R : ℝ} (E : NaturalExtension N Ω R) (T κ δ : ℝ) {p : CPoint} (hx : 0 ≤ p.1) (hz : p.2 ∈ Ω) : E.actF T κ δ p ≠ 0

noncomputable def NavierStokes.ActivationHolomorphic.parameterWindow : AxisCoefficientSpace.Window

Parameter window, bundling left, right, nondegenerate.

Equations

• NavierStokes.ActivationHolomorphic.parameterWindow = { left := -21 / 20, right := 21 / 20, nondegenerate := NavierStokes.ActivationHolomorphic.parameterWindow._proof_1 }

theorem NavierStokes.ActivationHolomorphic.parameterWindow_subset {η : ℝ} (hη : η ∈ parameterWindow.interval) : η ∈ NaturalAxisCoefficients.window.interval ∧ η ∈ ReferencePath.parameterInterval

theorem NavierStokes.ActivationHolomorphic.closed_parameter_subset {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : η ∈ parameterWindow.interval

theorem NavierStokes.ActivationHolomorphic.parameterTube_open (J : AxisCoefficientSpace.Window) (δ : ℝ) : IsOpen (AxisHolomorphic.parameterTube J δ)

noncomputable def NavierStokes.ActivationHolomorphic.naturalF {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (p : CPoint) : ℂ

Natural F as an element of ℂ.

Equations

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

noncomputable def NavierStokes.ActivationHolomorphic.naturalU {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (p : CPoint) : ℂ

Natural U, given by complexU j p.2 + (1/(Λ : ℂ)) * AxisHolomorphic.complexProfile window d.coefficients.epsilon F.coefficients.2 0 (Λ*p.1) p.2.

Equations

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

theorem NavierStokes.ActivationHolomorphic.naturalF_real {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (x η : ℝ) : naturalF F (x, ↑η) = ↑(F.family.f (x, η))

theorem NavierStokes.ActivationHolomorphic.naturalU_real {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (x η : ℝ) : naturalU F (x, ↑η) = ↑(F.family.U (x, η))

theorem NavierStokes.ActivationHolomorphic.scaled_radius_mem {Λ : ℝ} (hΛ : 0 < Λ) {x : ℝ} (hx : x ∈ Set.Ioo (-(5 / Λ)) (5 / Λ)) : Λ * x ∈ Set.Ioo (-5) 5

theorem NavierStokes.ActivationHolomorphic.coefficient_regular {h j σ Λ : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) {Ω : Set ℂ} (hΩ : Ω ⊆ AxisHolomorphic.parameterStrip NaturalAxisCoefficients.window (d.coefficients.epsilon * (1 - 1 / 2))) (A : ↥(AxisCoefficientSpace.AxisSpace NaturalAxisCoefficients.window d.coefficients.epsilon)) : Regular (Set.Ioo (-(5 / Λ)) (5 / Λ)) Ω fun (p : CPoint) => AxisHolomorphic.complexProfile NaturalAxisCoefficients.window d.coefficients.epsilon A 0 (Λ * p.1) p.2

theorem NavierStokes.ActivationHolomorphic.naturalF_regular {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {Ω : Set ℂ} (hstrip : Ω ⊆ AxisHolomorphic.parameterStrip NaturalAxisCoefficients.window (d.coefficients.epsilon * (1 - 1 / 2))) (hphase : Ω ⊆ d.compactSet) : Regular (Set.Ioo (-(5 / Λ)) (5 / Λ)) Ω (naturalF F)

theorem NavierStokes.ActivationHolomorphic.naturalU_regular {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {Ω : Set ℂ} (hstrip : Ω ⊆ AxisHolomorphic.parameterStrip NaturalAxisCoefficients.window (d.coefficients.epsilon * (1 - 1 / 2))) : Regular (Set.Ioo (-(5 / Λ)) (5 / Λ)) Ω (naturalU F)

theorem NavierStokes.ActivationHolomorphic.exists_preliminary_tube {h j σ : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ∃ (Ω : Set ℂ), IsOpen Ω ∧ (∀ η ∈ parameterWindow.interval, ↑η ∈ Ω) ∧ Ω ⊆ AxisHolomorphic.parameterStrip NaturalAxisCoefficients.window (d.coefficients.epsilon * (1 - 1 / 2)) ∧ Ω ⊆ d.compactSet ∧ Ω ⊆ NaturalAxisCoefficients.regularSet h j σ

theorem NavierStokes.ActivationHolomorphic.exists_positive_natural_tube {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ∃ (δ : ℝ), 0 < δ ∧ have Ω := AxisHolomorphic.parameterTube parameterWindow δ; IsOpen Ω ∧ Ω ⊆ NaturalAxisCoefficients.regularSet h j σ ∧ Regular (Set.Ioo (-(5 / Λ)) (5 / Λ)) Ω (naturalF F) ∧ Regular (Set.Ioo (-(5 / Λ)) (5 / Λ)) Ω (naturalU F) ∧ ∀ x ∈ Set.Icc 0 (41 / 10 / Λ), ∀ z ∈ Ω, 0 < (naturalF F (x, z)).re

Compact real positivity produces a single complex tube, uniformly over the whole natural radial interval used by REF.

theorem NavierStokes.ActivationHolomorphic.natural_log_radius {Λ : ℝ} (hΛ : 0 < Λ) {t : ℝ} (ht : t < ReferencePath.rampLimit) : 0 < 4 / Λ * Real.exp t ∧ 4 / Λ * Real.exp t < 41 / 10 / Λ

theorem NavierStokes.ActivationHolomorphic.exists_natural_extension {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ∃ (ρ : ℝ), 0 < ρ ∧ ∃ (x : NaturalExtension (ReferenceJetBounds.referenceInput F hΛ) (AxisHolomorphic.parameterTube parameterWindow ρ) (5 / Λ)), AxisHolomorphic.parameterTube parameterWindow ρ ⊆ NaturalAxisCoefficients.regularSet h j σ

Construction from the actual coefficient witness. In particular the natural extension and its common positive neighborhood are not assumptions.

noncomputable def NavierStokes.ActivationHolomorphic.radialJet (F : CField) (k : ℕ) (p : CPoint) : ℂ

Radial jet, given by iteratedDeriv k (fun x => F (x,p.2)) p.1.

Equations

• NavierStokes.ActivationHolomorphic.radialJet F k p = iteratedDeriv k (fun (x : ℝ) => F (x, p.2)) p.1

theorem NavierStokes.ActivationHolomorphic.radialJet_succ (F : CField) (k : ℕ) : radialJet F (k + 1) = radial (radialJet F k)

theorem NavierStokes.ActivationHolomorphic.Regular.radialJet {S : Set ℝ} {Ω : Set ℂ} {F : CField} (hF : Regular S Ω F) (hS : IsOpen S) (hΩ : IsOpen Ω) (k : ℕ) : Regular S Ω (ActivationHolomorphic.radialJet F k)

theorem NavierStokes.ActivationHolomorphic.scale_half_interval {R : ℝ} (hR : 0 < R) {x : ℝ} (hx : x ∈ Set.Ioi (-R)) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : t * x ∈ Set.Ioi (-R)

theorem NavierStokes.ActivationHolomorphic.Regular.pow {S : Set ℝ} {Ω : Set ℂ} {F : CField} (hF : Regular S Ω F) (n : ℕ) : Regular S Ω fun (p : CPoint) => F p ^ n

noncomputable def NavierStokes.ActivationHolomorphic.pressure (P0 : ℂ → ℂ) (f : CField) (p : CPoint) : ℂ

Pressure, given by P0 p.2 + primitive (fun q => f q ^ 2) p.

Equations

• NavierStokes.ActivationHolomorphic.pressure P0 f p = P0 p.2 + NavierStokes.ActivationHolomorphic.primitive (fun (q : NavierStokes.ActivationHolomorphic.CPoint) => f q ^ 2) p

theorem NavierStokes.ActivationHolomorphic.regular_pressure {R : ℝ} (hR : 0 < R) {Ω : Set ℂ} (hΩ : IsOpen Ω) {f : CField} (hf : Regular (Set.Ioi (-R)) Ω f) {P0 : ℂ → ℂ} (hP0 : AnalyticOnNhd ℂ P0 Ω) : Regular (Set.Ioi (-R)) Ω (pressure P0 f)

theorem NavierStokes.ActivationHolomorphic.average_ofReal {F : CField} {g : ProfileHistories.Field} {η : ℝ} (heq : ∀ (x : ℝ), F (x, ↑η) = ↑(g (x, η))) (x : ℝ) : average F (x, ↑η) = ↑(ProfileHistories.average g (x, η))

theorem NavierStokes.ActivationHolomorphic.primitive_ofReal {F : CField} {g : ProfileHistories.Field} {η : ℝ} (heq : ∀ (x : ℝ), F (x, ↑η) = ↑(g (x, η))) (x : ℝ) : primitive F (x, ↑η) = ↑(ProfileHistories.primitive g (x, η))

theorem NavierStokes.ActivationHolomorphic.pressure_ofReal {F : CField} {g : ProfileHistories.Field} {η : ℝ} (heq : ∀ (x : ℝ), F (x, ↑η) = ↑(g (x, η))) {P0 : ℂ → ℂ} {p0 : ℝ → ℝ} (hP0 : P0 ↑η = ↑(p0 η)) (x : ℝ) : pressure P0 F (x, ↑η) = ↑(p0 η + ProfileHistories.primitive (fun (p : ProfileHistories.Point) => g p ^ 2) (x, η))

def NavierStokes.ActivationHolomorphic.signedSquare (F : CField) (p : CPoint) : ℂ

Pull back a complex field along the square of its radial coordinate.

Equations

• NavierStokes.ActivationHolomorphic.signedSquare F p = F (p.1 ^ 2, p.2)

theorem NavierStokes.ActivationHolomorphic.Regular.signedSquare {R : ℝ} (hR : 0 < R) {Ω : Set ℂ} {F : CField} (hF : Regular (Set.Ioi (-R)) Ω F) : Regular Set.univ Ω (ActivationHolomorphic.signedSquare F)

theorem NavierStokes.ActivationHolomorphic.signedSquare_even (F : CField) (z : ℂ) : Function.Even fun (r : ℝ) => signedSquare F (r, z)

structure NavierStokes.ActivationHolomorphic.InitialTube (N : ReferencePath.Input) (h : ℝ) (P0 : ℝ → ℝ) (R : ℝ) (Ω : Set ℂ) : Type

The actual base data on one common complex tube. The constructor below supplies the pressure extension from its proved defining integral.

• natural : NaturalExtension N Ω R

  Natural of InitialTube, of type NaturalExtension N Ω R.

• isOpen : IsOpen Ω
• real_mem (η : ℝ) : η ∈ Set.Icc (-1) 1 → ↑η ∈ Ω
• elliptic_ne_zero (z : ℂ) : z ∈ Ω → NaturalAxisCoefficients.complexL h z ≠ 0
• pressure0 : ℂ → ℂ

  Pressure0 of InitialTube, of type ℂ → ℂ.

• pressure0_analytic : AnalyticOnNhd ℂ self.pressure0 Ω
• pressure0_real (η : ℝ) : self.pressure0 ↑η = ↑(P0 η)

noncomputable def NavierStokes.ActivationHolomorphic.InitialTube.f {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) (T κ δ : ℝ) : CField

F, given by E.natural.actF T κ δ.

Equations

• E.f T κ δ = E.natural.actF T κ δ

noncomputable def NavierStokes.ActivationHolomorphic.InitialTube.U {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) (T κ δ : ℝ) : CField

U, given by E.natural.actU T κ δ.

Equations

• E.U T κ δ = E.natural.actU T κ δ

noncomputable def NavierStokes.ActivationHolomorphic.InitialTube.Ubar {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) (T κ δ : ℝ) : CField

Ubar, given by average (E.U T κ δ).

Equations

• E.Ubar T κ δ = NavierStokes.ActivationHolomorphic.average (E.U T κ δ)

noncomputable def NavierStokes.ActivationHolomorphic.InitialTube.Pi {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) (T κ δ : ℝ) : CField

Pi, given by pressure E.pressure0 (E.f T κ δ).

Equations

• E.Pi T κ δ = NavierStokes.ActivationHolomorphic.pressure E.pressure0 (E.f T κ δ)

theorem NavierStokes.ActivationHolomorphic.InitialTube.regular {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) : Regular (Set.Ioi (-R)) Ω (E.f T κ δ) ∧ Regular (Set.Ioi (-R)) Ω (E.U T κ δ) ∧ Regular (Set.Ioi (-R)) Ω (E.Ubar T κ δ) ∧ Regular (Set.Ioi (-R)) Ω (E.Pi T κ δ)

theorem NavierStokes.ActivationHolomorphic.InitialTube.all_radial_jets {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (k : ℕ) : Regular (Set.Ioi (-R)) Ω (radialJet (E.f T κ δ) k) ∧ Regular (Set.Ioi (-R)) Ω (radialJet (E.U T κ δ) k) ∧ Regular (Set.Ioi (-R)) Ω (radialJet (E.Ubar T κ δ) k) ∧ Regular (Set.Ioi (-R)) Ω (radialJet (E.Pi T κ δ) k)

The width of the holomorphic domain is unchanged at every fixed radial derivative order. These are actual iterated derivatives of the functions.

theorem NavierStokes.ActivationHolomorphic.InitialTube.signed_regular {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) : Regular Set.univ Ω (signedSquare (E.f T κ δ)) ∧ Regular Set.univ Ω (signedSquare (E.U T κ δ)) ∧ Regular Set.univ Ω (signedSquare (E.Ubar T κ δ)) ∧ Regular Set.univ Ω (signedSquare (E.Pi T κ δ))

The signed-square pullbacks are smooth and holomorphic through the axis, and are even in the signed radius.

theorem NavierStokes.ActivationHolomorphic.InitialTube.f_ne_zero {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) (T κ δ : ℝ) {x : ℝ} (hx : 0 ≤ x) {z : ℂ} (hz : z ∈ Ω) : E.f T κ δ (x, z) ≠ 0

theorem NavierStokes.ActivationHolomorphic.InitialTube.real_profiles {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (x : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : have P := StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0; E.f T κ δ (x, ↑η) = ↑(P.f (x, η)) ∧ E.U T κ δ (x, ↑η) = ↑(P.U (x, η)) ∧ E.Ubar T κ δ (x, ↑η) = ↑(P.Ubar (x, η)) ∧ E.Pi T κ δ (x, ↑η) = ↑(P.pressure (x, η))

Agreement includes the literal axis-to-radius average and pressure, with no independently prescribed moment data.

theorem NavierStokes.ActivationHolomorphic.InitialTube.reference_regular {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) : Regular (Set.Ioi (-R)) Ω (E.natural.refF δ) ∧ Regular (Set.Ioi (-R)) Ω (E.natural.refU δ) ∧ Regular (Set.Ioi (-R)) Ω (average (E.natural.refU δ)) ∧ Regular (Set.Ioi (-R)) Ω (pressure E.pressure0 (E.natural.refF δ))

theorem NavierStokes.ActivationHolomorphic.InitialTube.reference_real_profiles {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (x : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : have P := N.histories hδ hδT P0 hP0; E.natural.refF δ (x, ↑η) = ↑(P.f (x, η)) ∧ E.natural.refU δ (x, ↑η) = ↑(P.U (x, η)) ∧ average (E.natural.refU δ) (x, ↑η) = ↑(P.Ubar (x, η)) ∧ pressure E.pressure0 (E.natural.refF δ) (x, ↑η) = ↑(P.pressure (x, η))

theorem NavierStokes.ActivationHolomorphic.exists_initialTube {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} (hp : PressureDatum.Admissible g a cap) {d : NaturalAxisCoefficients.AnalyticInputs h j σ (PressureDatum.pressure g a)} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ∃ (ρ : ℝ), 0 < ρ ∧ Nonempty (InitialTube (ReferenceJetBounds.referenceInput F hΛ) h (PressureDatum.pressure g a) (5 / Λ) (AxisHolomorphic.parameterTube parameterWindow ρ))

Actual coefficient profiles and the actual pressure datum construct the common tube. The width is chosen before the REF and ACT cutoff lengths.

theorem NavierStokes.ActivationHolomorphic.natural_average_identity {h j Λ : ℝ} {P0 a : ℝ → ℝ} {f U V Pr : ProfileHistories.Field} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a f U V Pr) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : ProfileHistories.average U p = V p

theorem NavierStokes.ActivationHolomorphic.natural_Ubar_real {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : average (naturalU F) (p.1, ↑p.2) = ↑(F.family.Ubar p)

The natural average recovered by complex integration is the original natural profile's actual average, including the regular value at the axis.

theorem NavierStokes.ActivationHolomorphic.natural_Pi_real {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) {P : ℂ → ℂ} (hP : ∀ (η : ℝ), P ↑η = ↑(P0 η)) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : pressure P (naturalF F) (p.1, ↑p.2) = ↑(F.family.Pi p)

theorem NavierStokes.ActivationHolomorphic.iteratedDeriv_smooth {S : Set ℝ} (hS : IsOpen S) {g : ℝ → ℝ} (hg : ContDiffOn ℝ (↑⊤) g S) (k : ℕ) : ContDiffOn ℝ (↑⊤) (iteratedDeriv k g) S

theorem NavierStokes.ActivationHolomorphic.iteratedDeriv_ofReal {S : Set ℝ} (hS : IsOpen S) {g : ℝ → ℝ} (hg : ContDiffOn ℝ (↑⊤) g S) (k : ℕ) {x : ℝ} (hx : x ∈ S) : iteratedDeriv k (fun (y : ℝ) => ↑(g y)) x = ↑(iteratedDeriv k g x)

theorem NavierStokes.ActivationHolomorphic.radialJet_real {S : Set ℝ} {Ω : Set ℂ} (hS : IsOpen S) : IsOpen Ω → ∀ {F : CField} (hF : Regular S Ω F) {g : ℝ → ℝ} {η : ℝ} (hη : ↑η ∈ Ω) (heq : ∀ x ∈ S, F (x, ↑η) = ↑(g x)) (k : ℕ) {x : ℝ} (hx : x ∈ S), radialJet F k (x, ↑η) = ↑(iteratedDeriv k g x)

The holomorphic radial jets extend the actual real radial derivatives, including at the axis; agreement is derived from equality of the functions.

theorem NavierStokes.ActivationHolomorphic.InitialTube.real_radial_jets {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (k : ℕ) {x η : ℝ} (hx : x ∈ Set.Ioi (-R)) (hη : η ∈ Set.Icc (-1) 1) : have P := StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0; radialJet (E.f T κ δ) k (x, ↑η) = ↑(iteratedDeriv k (fun (y : ℝ) => P.f (y, η)) x) ∧ radialJet (E.U T κ δ) k (x, ↑η) = ↑(iteratedDeriv k (fun (y : ℝ) => P.U (y, η)) x) ∧ radialJet (E.Ubar T κ δ) k (x, ↑η) = ↑(iteratedDeriv k (fun (y : ℝ) => P.Ubar (y, η)) x) ∧ radialJet (E.Pi T κ δ) k (x, ↑η) = ↑(iteratedDeriv k (fun (y : ℝ) => P.pressure (y, η)) x)

theorem NavierStokes.ActivationHolomorphic.scale_symmetric_interval {R x t : ℝ} (hx : x ∈ Set.Ioo (-R) R) (ht : t ∈ Set.Icc 0 1) : t * x ∈ Set.Ioo (-R) R

theorem NavierStokes.ActivationHolomorphic.InitialTube.natural_regular {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) : Regular (Set.Ioo (-R) R) Ω E.natural.f ∧ Regular (Set.Ioo (-R) R) Ω E.natural.U ∧ Regular (Set.Ioo (-R) R) Ω (average E.natural.U) ∧ Regular (Set.Ioo (-R) R) Ω (pressure E.pressure0 E.natural.f)

theorem NavierStokes.ActivationHolomorphic.InitialTube.natural_all_radial_jets {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) (k : ℕ) : Regular (Set.Ioo (-R) R) Ω (radialJet E.natural.f k) ∧ Regular (Set.Ioo (-R) R) Ω (radialJet E.natural.U k) ∧ Regular (Set.Ioo (-R) R) Ω (radialJet (average E.natural.U) k) ∧ Regular (Set.Ioo (-R) R) Ω (radialJet (pressure E.pressure0 E.natural.f) k)

theorem NavierStokes.ActivationHolomorphic.InitialTube.reference_all_radial_jets {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : InitialTube N h P0 R Ω) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (k : ℕ) : Regular (Set.Ioi (-R)) Ω (radialJet (E.natural.refF δ) k) ∧ Regular (Set.Ioi (-R)) Ω (radialJet (E.natural.refU δ) k) ∧ Regular (Set.Ioi (-R)) Ω (radialJet (average (E.natural.refU δ)) k) ∧ Regular (Set.Ioi (-R)) Ω (radialJet (pressure E.pressure0 (E.natural.refF δ)) k)

theorem NavierStokes.ActivationHolomorphic.InitialTube.natural_real_profiles {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {R : ℝ} {Ω : Set ℂ} (E : InitialTube (ReferenceJetBounds.referenceInput F hΛ) h P0 R Ω) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : E.natural.f (p.1, ↑p.2) = ↑(F.family.f p) ∧ E.natural.U (p.1, ↑p.2) = ↑(F.family.U p) ∧ average E.natural.U (p.1, ↑p.2) = ↑(F.family.Ubar p) ∧ pressure E.pressure0 E.natural.f (p.1, ↑p.2) = ↑(F.family.Pi p)

noncomputable def NavierStokes.ActualSlowAxis.parameterDomain (Ω : Set ℂ) : Set ℂ

A conjugation-invariant open neighborhood whose real points remain in the real profile domain. It retains the entire closed physical window.

Equations

• NavierStokes.ActualSlowAxis.parameterDomain Ω = Ω ∩ ⇑(starRingEnd ℂ) ⁻¹' Ω ∩ Complex.re ⁻¹' NavierStokes.ReferencePath.parameterInterval

theorem NavierStokes.ActualSlowAxis.parameterDomain_open {Ω : Set ℂ} (hΩ : IsOpen Ω) : IsOpen (parameterDomain Ω)

theorem NavierStokes.ActualSlowAxis.parameterDomain_subset (Ω : Set ℂ) : parameterDomain Ω ⊆ Ω

theorem NavierStokes.ActualSlowAxis.parameterDomain_conjugate {Ω : Set ℂ} {z : ℂ} (hz : z ∈ parameterDomain Ω) : (starRingEnd ℂ) z ∈ parameterDomain Ω

theorem NavierStokes.ActualSlowAxis.parameterDomain_real {Ω : Set ℂ} (hreal : ∀ eta ∈ Set.Icc (-1) 1, ↑eta ∈ Ω) {eta : ℝ} (heta : eta ∈ Set.Icc (-1) 1) : ↑eta ∈ parameterDomain Ω

theorem NavierStokes.ActualSlowAxis.parameterDomain_real_interval {Ω : Set ℂ} {eta : ℝ} (heta : ↑eta ∈ parameterDomain Ω) : eta ∈ ReferencePath.parameterInterval

theorem NavierStokes.ActualSlowAxis.parameterTube_conjugate (J : AxisCoefficientSpace.Window) {ρ : ℝ} {z : ℂ} (hz : z ∈ AxisHolomorphic.parameterTube J ρ) : (starRingEnd ℂ) z ∈ AxisHolomorphic.parameterTube J ρ

theorem NavierStokes.ActualSlowAxis.smallTube_subset_domain {ρ τ : ℝ} (hτρ : τ ≤ ρ) (hτ : τ ≤ 1 / 40) : AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow τ ⊆ parameterDomain (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow ρ)

theorem NavierStokes.ActualSlowAxis.histories_congr_below {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') {X eta : ℝ} (hX : 0 ≤ X) (hP0 : P.pressure0 eta = Q.pressure0 eta) (hf : ∀ Y ∈ Set.Icc 0 X, P.f (Y, eta) = Q.f (Y, eta)) (hu : ∀ Y ∈ Set.Icc 0 X, P.U (Y, eta) = Q.U (Y, eta)) : P.Ubar (X, eta) = Q.Ubar (X, eta) ∧ P.pressure (X, eta) = Q.pressure (X, eta)

theorem NavierStokes.ActualSlowAxis.domain {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {S : ℝ} (hS : 0 < S) : SlowRecursion.Domain S (parameterDomain Ω) h

noncomputable def NavierStokes.ActualSlowAxis.fields {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) (T κ δ : ℝ) : Fin 4 → ActivationHolomorphic.CField

Fields, given by ![E.f T κ δ, E.U T κ δ, E.Ubar T κ δ, E.Pi T κ δ].

Equations

• NavierStokes.ActualSlowAxis.fields E T κ δ = ![E.f T κ δ, E.U T κ δ, E.Ubar T κ δ, E.Pi T κ δ]

noncomputable def NavierStokes.ActualSlowAxis.realFields {N : ReferencePath.Input} {P0 : ℝ → ℝ} {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) : Fin 4 → ProfileHistories.Field

Real fields, given by let P := StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0 ![P.f, P.U, P.Ubar, P.pressure].

Equations

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

theorem NavierStokes.ActualSlowAxis.fields_regular {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (i : Fin 4) : ActivationHolomorphic.Regular Set.univ Ω (ActivationHolomorphic.signedSquare (fields E T κ δ i))

theorem NavierStokes.ActualSlowAxis.fields_real {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (i : Fin 4) (x : ℝ) {eta : ℝ} (heta : eta ∈ ReferencePath.parameterInterval) : fields E T κ δ i (x, ↑eta) = ↑(realFields hT hδ hδT κ hP0 i (x, eta))

noncomputable def NavierStokes.ActualSlowAxis.element {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (S : ℝ) (i : Fin 4) : SlowRecursion.AxisFunction S (parameterDomain Ω)

Each base component is an actual member of the compatible function algebra; no separate jet data or extension hypothesis is supplied.

Equations

• NavierStokes.ActualSlowAxis.element E hT hδ hδT κ hP0 S i = ⟨NavierStokes.ActivationHolomorphic.signedSquare (NavierStokes.ActualSlowAxis.fields E T κ δ i), ⋯⟩

theorem NavierStokes.ActualSlowAxis.element_complexProfile {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (S : ℝ) (i : Fin 4) {X : ℝ} (hX : 0 ≤ X) (z : ℂ) : SlowRecursion.complexProfile (element E hT hδ hδT κ hP0 S i) (X, z) = fields E T κ δ i (X, z)

theorem NavierStokes.ActualSlowAxis.element_profile {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (S : ℝ) (i : Fin 4) {X eta : ℝ} (hX : 0 ≤ X) (heta : eta ∈ ReferencePath.parameterInterval) : SlowRecursion.profile (element E hT hδ hδT κ hP0 S i) (X, eta) = realFields hT hδ hδT κ hP0 i (X, eta)

theorem NavierStokes.ActualSlowAxis.realFields_smooth {N : ReferencePath.Input} {P0 : ℝ → ℝ} {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (i : Fin 4) : ContDiffOn ℝ (↑⊤) (realFields hT hδ hδT κ hP0 i) N.radialDomain.carrier

theorem NavierStokes.ActualSlowAxis.real_domain_mem (N : ReferencePath.Input) {X eta : ℝ} (hX : 0 ≤ X) (heta : eta ∈ ReferencePath.parameterInterval) : (X, eta) ∈ N.radialDomain.carrier

theorem NavierStokes.ActualSlowAxis.element_right_jets {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (S : ℝ) (i : Fin 4) (k : ℕ) {X eta : ℝ} (hX : 0 ≤ X) (heta : eta ∈ ReferencePath.parameterInterval) : iteratedDerivWithin k (fun (Y : ℝ) => SlowRecursion.profile (element E hT hδ hδT κ hP0 S i) (Y, eta)) (Set.Ici 0) X = iteratedDeriv k (fun (Y : ℝ) => realFields hT hδ hδT κ hP0 i (Y, eta)) X

The canonical right jets agree with the actual smooth ACT jets at the axis as well as at every positive radius.

theorem NavierStokes.ActualSlowAxis.element_profile_germ {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (S : ℝ) (i : Fin 4) {X eta : ℝ} (hX : 0 < X) (heta : eta ∈ ReferencePath.parameterInterval) : SlowRecursion.profile (element E hT hδ hδT κ hP0 S i) =ᶠ[nhds (X, eta)] realFields hT hδ hδT κ hP0 i

noncomputable def NavierStokes.ActualSlowAxis.base {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (C : ℝ) {S : ℝ} (hS : 0 < S) : SlowRecursion.Coefficient S (parameterDomain Ω)

Base, constructed using SlowRecursion.makeBase.

Equations

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

theorem NavierStokes.ActualSlowAxis.base_values {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (C : ℝ) {S : ℝ} (hS : 0 < S) {X eta : ℝ} (hX : 0 ≤ X) (heta : eta ∈ ReferencePath.parameterInterval) : have A := base E hT hδ hδT κ hP0 C hS; have P := StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0; SlowRecursion.profile (A 0) (X, eta) = C * P.f (X, eta) ∧ SlowRecursion.profile (A 1) (X, eta) = P.U (X, eta) ∧ SlowRecursion.profile (A 2) (X, eta) = P.Ubar (X, eta) - P.U (X, eta) ∧ SlowRecursion.profile (A 3) (X, eta) = P.pressure (X, eta)

theorem NavierStokes.ActualSlowAxis.base_beta_value {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (C : ℝ) {S : ℝ} (hS : 0 < S) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (S ^ 2)) (heta : ↑eta ∈ parameterDomain Ω) : have P := StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0; SlowRecursion.profile (base E hT hδ hδT κ hP0 C hS 4) (X, eta) = SlowDivergence.radialFlux h 0 P.U (X, eta) / X

noncomputable def NavierStokes.ActualSlowAxis.axisRadius (N : ReferencePath.Input) (δ : ℝ) : ℝ

A fixed radial rectangle strictly containing the entire initial collar.

Equations

• NavierStokes.ActualSlowAxis.axisRadius N δ = √(N.endpoint * Real.exp δ) + 1

theorem NavierStokes.ActualSlowAxis.axisRadius_pos (N : ReferencePath.Input) (δ : ℝ) : 0 < axisRadius N δ

theorem NavierStokes.ActualSlowAxis.collar_lt_square (N : ReferencePath.Input) (δ : ℝ) : N.endpoint * Real.exp δ < axisRadius N δ ^ 2

noncomputable def NavierStokes.ActualSlowAxis.hierarchy {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (C : ℝ) : SlowRecursion.LocalHierarchy (axisRadius N δ) (parameterDomain Ω) h C fun (i : Fin 5) => SlowRecursion.profile (base E hT hδ hδT κ hP0 C ⋯ i)

Hierarchy used in actual slow axis.

Equations

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

theorem NavierStokes.ActualSlowAxis.hierarchy_base_values {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (C : ℝ) {X eta : ℝ} (hX : 0 ≤ X) (heta : eta ∈ ReferencePath.parameterInterval) : have A := hierarchy E hT hδ hδT κ hP0 C; have P := StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0; SlowRecursion.profile (A.coefficients 0 0) (X, eta) = C * P.f (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 1) (X, eta) = P.U (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 2) (X, eta) = P.Ubar (X, eta) - P.U (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 3) (X, eta) = P.pressure (X, eta)

theorem NavierStokes.ActualSlowAxis.hierarchy_physical_swirl {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) {C : ℝ} (hC : C ≠ 0) {X eta : ℝ} (hX : 0 ≤ X) (heta : eta ∈ ReferencePath.parameterInterval) : have A := hierarchy E hT hδ hδT κ hP0 C; have P := StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0; √(2 * X) * SlowRecursion.profile (A.coefficients 0 0) (X, eta) / C = P.E (X, eta)

theorem NavierStokes.ActualSlowAxis.hierarchy_on_collar {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (C : ℝ) {n : ℕ} (hn : 0 < n) {X eta : ℝ} (hX : 0 < X) (hcollar : X ≤ N.endpoint * Real.exp δ) (heta : eta ∈ Set.Icc (-1) 1) : SlowRecursion.OrderEquations h C (hierarchy E hT hδ hδT κ hP0 C).coefficients n (X, eta)

theorem NavierStokes.ActualSlowAxis.exists_tube_of_pressure_eq {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ∃ (ρ : ℝ), 0 < ρ ∧ Nonempty (ActivationHolomorphic.InitialTube (ReferenceJetBounds.referenceInput F hΛ) h P0 (5 / Λ) (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow ρ))

noncomputable def NavierStokes.ActualSlowAxis.tubeWidth {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ℝ

Tube width, given by Classical.choose (exists_tube_of_pressure_eq hp hP0 F hΛ hsmall hσ).

Equations

• NavierStokes.ActualSlowAxis.tubeWidth hp hP0 F hΛ hsmall hσ = Classical.choose ⋯

theorem NavierStokes.ActualSlowAxis.tubeWidth_pos {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : 0 < tubeWidth hp hP0 F hΛ hsmall hσ

noncomputable def NavierStokes.ActualSlowAxis.constructedTube {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ActivationHolomorphic.InitialTube (ReferenceJetBounds.referenceInput F hΛ) h P0 (5 / Λ) (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow (tubeWidth hp hP0 F hΛ hsmall hσ))

This witness is obtained from the actual coefficient-space natural solution and the proved pressure integral, not supplied by the caller.

Equations

• NavierStokes.ActualSlowAxis.constructedTube hp hP0 F hΛ hsmall hσ = Classical.choice ⋯

theorem NavierStokes.ActualSlowAxis.actualPressure_smooth {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) : ContDiff ℝ (↑⊤) P0

noncomputable def NavierStokes.ActualSlowAxis.fromNatural {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) : SlowRecursion.LocalHierarchy (axisRadius (ReferenceJetBounds.referenceInput F hΛ) δ) (parameterDomain (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow (tubeWidth hp hP0 F hΛ hsmall hσ))) h C fun (i : Fin 5) => SlowRecursion.profile (base (constructedTube hp hP0 F hΛ hsmall hσ) hT hδ hδT κ ⋯ C ⋯ i)

From natural, given by hierarchy (constructedTube hp hP0 F hΛ hsmall hσ) hT hδ hδT κ (actualPressure_smooth hp hP0) C.

Equations

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

theorem NavierStokes.ActualSlowAxis.fromNatural_window {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {eta : ℝ} (heta : eta ∈ Set.Icc (-1) 1) : ↑eta ∈ parameterDomain (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow (tubeWidth hp hP0 F hΛ hsmall hσ))

theorem NavierStokes.ActualSlowAxis.fromNatural_uniform_tube {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ∃ (τ : ℝ), 0 < τ ∧ AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow τ ⊆ parameterDomain (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow (tubeWidth hp hP0 F hΛ hsmall hσ))

theorem NavierStokes.ActualSlowAxis.fromNatural_base_values {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) {X eta : ℝ} (hX : 0 ≤ X) (heta : eta ∈ ReferencePath.parameterInterval) : have A := fromNatural hp hP0 F hΛ hsmall hσ hT hδ hδT κ; have P := StressActivation.FromReference.histories (ReferenceJetBounds.referenceInput F hΛ) hT hδ hδT κ P0 ⋯; SlowRecursion.profile (A.coefficients 0 0) (X, eta) = C * P.f (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 1) (X, eta) = P.U (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 2) (X, eta) = P.Ubar (X, eta) - P.U (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 3) (X, eta) = P.pressure (X, eta)

theorem NavierStokes.ActualSlowAxis.fromNatural_positive_order {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) {n : ℕ} (hn : 0 < n) {X eta : ℝ} (hX : 0 < X) (hcollar : X ≤ (ReferenceJetBounds.referenceInput F hΛ).endpoint * Real.exp δ) (heta : eta ∈ Set.Icc (-1) 1) : SlowRecursion.OrderEquations h C (fromNatural hp hP0 F hΛ hsmall hσ hT hδ hδT κ).coefficients n (X, eta)

theorem NavierStokes.ActualSlowAxis.fromNatural_initial {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) {X eta : ℝ} (hX : 0 ≤ X) (hinitial : X ≤ 4 / Λ) (heta : eta ∈ ReferencePath.parameterInterval) : have A := fromNatural hp hP0 F hΛ hsmall hσ hT hδ hδT κ; SlowRecursion.profile (A.coefficients 0 0) (X, eta) = C * F.family.f (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 1) (X, eta) = F.family.U (X, eta)

theorem NavierStokes.ActualSlowAxis.fromNatural_stock_prefix {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ κ w₁ w₂ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hb : δ ≤ (TransitionRamp.ofNatural F.family hΛ hsmall hδ hδT ⋯).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {X eta : ℝ} (hX : 0 ≤ X) (hcollar : X ≤ (ReferenceJetBounds.referenceInput F hΛ).endpoint * Real.exp δ) (heta : eta ∈ ReferencePath.parameterInterval) : have A := fromNatural hp hP0 F hΛ hsmall hσ hT hδ hδT κ; have Q := TransitionRamp.physicalProfiles F.family hΛ hsmall hδ hδT ⋯ hT hb hw₁ hw₂; SlowRecursion.profile (A.coefficients 0 0) (X, eta) = C * Q.f (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 1) (X, eta) = Q.U (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 2) (X, eta) = Q.Ubar (X, eta) - Q.U (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 3) (X, eta) = Q.pressure (X, eta)

theorem NavierStokes.ActualSlowAxis.fromNatural_stock_fields {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ κ w₁ w₂ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hC : C ≠ 0) (hb : δ ≤ (TransitionRamp.ofNatural F.family hΛ hsmall hδ hδT ⋯).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {X eta : ℝ} (hX : 0 ≤ X) (hcollar : X ≤ (ReferenceJetBounds.referenceInput F hΛ).endpoint * Real.exp δ) (heta : eta ∈ ReferencePath.parameterInterval) : have A := fromNatural hp hP0 F hΛ hsmall hσ hT hδ hδT κ; have Q := TransitionRamp.physicalProfiles F.family hΛ hsmall hδ hδT ⋯ hT hb hw₁ hw₂; √(2 * X) * SlowRecursion.profile (A.coefficients 0 0) (X, eta) / C = Q.E (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 1) (X, eta) = Q.U (X, eta) ∧ SlowRecursion.profile (A.coefficients 0 3) (X, eta) = Q.pressure (X, eta)

theorem NavierStokes.ActualSlowAxis.fromNatural_profiles_smooth {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (n : ℕ) (i : Fin 5) : ContDiffOn ℝ (↑⊤) (SlowRecursion.profile ((fromNatural hp hP0 F hΛ hsmall hσ hT hδ hδT κ).coefficients n i)) (Set.Ico 0 (axisRadius (ReferenceJetBounds.referenceInput F hΛ) δ ^ 2) ×ˢ PositiveAxisExistence.realParameterDomain (parameterDomain (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow (tubeWidth hp hP0 F hΛ hsmall hσ))))

theorem NavierStokes.ActualSlowAxis.fromNatural_zero_axis {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) {n : ℕ} (hn : 0 < n) (i : Fin 5) {eta : ℝ} (heta : eta ∈ Set.Icc (-1) 1) : ↑((fromNatural hp hP0 F hΛ hsmall hσ hT hδ hδT κ).coefficients n i) (0, ↑eta) = 0

theorem NavierStokes.ActualSlowAxis.fromNatural_axis_jets {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (n : ℕ) (i : Fin 5) (k : ℕ) {eta : ℝ} (heta : eta ∈ Set.Icc (-1) 1) : have A := fromNatural hp hP0 F hΛ hsmall hσ hT hδ hδT κ; iteratedDerivWithin k (fun (X : ℝ) => SlowRecursion.profile (A.coefficients n i) (X, eta)) (Set.Ici 0) 0 = (↑k.factorial / ↑(2 * k).factorial) • iteratedDeriv (2 * k) (fun (r : ℝ) => (↑(A.coefficients n i) (r, ↑eta)).re) 0