The relaxed continuation after the initial activation

The comparison formulas use actual stock coordinates. The scalar barrier uses the differential equation of the primitive-defined angular lag.

Bounds for the actual reference continuation

The history estimates below use the primitive-defined lags and pressure of ProfileHistories. The reference source estimates and the ordered parameter choices are derived from the constructed natural and reference profiles.

noncomputable def NavierStokes.ReferenceBounds.logSlope {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) : ℝ

Log slope, given by 1 + p.1 * radialPartial P.f p / P.f p.

Equations

• NavierStokes.ReferenceBounds.logSlope P p = 1 + p.1 * NavierStokes.ProfileHistories.radialPartial P.f p / P.f p

noncomputable def NavierStokes.ReferenceBounds.sourceQ {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : ℝ

Source Q as an element of ℝ.

Equations

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

noncomputable def NavierStokes.ReferenceBounds.p1 {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : ℝ

P1, given by p.1 * P.angularLag h p / NaturalAxisData.L h p.2.

Equations

• NavierStokes.ReferenceBounds.p1 P h p = p.1 * P.angularLag h p / NavierStokes.NaturalAxisData.L h p.2

noncomputable def NavierStokes.ReferenceBounds.ns {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : ℝ

Ns, given by P.axialLag h p / NaturalAxisData.L h p.2.

Equations

• NavierStokes.ReferenceBounds.ns P h p = P.axialLag h p / NavierStokes.NaturalAxisData.L h p.2

noncomputable def NavierStokes.ReferenceBounds.p2 {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : ℝ

P2, given by p.1 * ns P h p / P.E p.

Equations

• NavierStokes.ReferenceBounds.p2 P h p = p.1 * NavierStokes.ReferenceBounds.ns P h p / P.E p

noncomputable def NavierStokes.ReferenceBounds.coneSize {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : ℝ

Cone size, given by p1 P h p + p2 P h p ^ 2 / p1 P h p.

Equations

• NavierStokes.ReferenceBounds.coneSize P h p = NavierStokes.ReferenceBounds.p1 P h p + NavierStokes.ReferenceBounds.p2 P h p ^ 2 / NavierStokes.ReferenceBounds.p1 P h p

theorem NavierStokes.ReferenceBounds.H_radialPartial {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) : ProfileHistories.radialPartial P.H p = 2 * P.f p + 2 * p.1 * ProfileHistories.radialPartial P.f p

theorem NavierStokes.ReferenceBounds.angularSource_eq {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hf : P.f p ≠ 0) (h : ℝ) : P.angularSource h p = P.H p * sourceQ P h p

theorem NavierStokes.ReferenceBounds.p1_primitive {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hX : p.1 ≠ 0) (h : ℝ) : p1 P h p = ProfileHistories.primitive (P.angularSource h) p / (NaturalAxisData.L h p.2 * P.H p)

theorem NavierStokes.ReferenceBounds.ns_primitive {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) (h : ℝ) : ns P h p = ProfileHistories.primitive (P.axialSource h) p / (NaturalAxisData.L h p.2 * p.1)

theorem NavierStokes.ReferenceBounds.parameterPartial_square {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) : ProfileHistories.parameterPartial (fun (q : ProfileHistories.Point) => P.f q ^ 2) p = 2 * P.f p * ProfileHistories.parameterPartial P.f p

theorem NavierStokes.ReferenceBounds.pressure_parameter_increment {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) : ProfileHistories.parameterPartial P.pressure p - deriv P.pressure0 p.2 = ∫ (s : ℝ) in 0..p.1, 2 * P.f (s, p.2) * ProfileHistories.parameterPartial P.f (s, p.2)

theorem NavierStokes.ReferenceBounds.pressure_increment_bound {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} : p ∈ D.carrier → ∀ (hX : 0 ≤ p.1) {K C : ℝ}, 0 ≤ K → 0 < C → ∀ (hf : ∀ s ∈ Set.Icc 0 p.1, |P.f (s, p.2)| ≤ K / C), |P.pressure p - P.pressure0 p.2| ≤ p.1 * K ^ 2 / C ^ 2

theorem NavierStokes.ReferenceBounds.pressure_parameter_increment_bound {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 ≤ p.1) {K C : ℝ} (hK : 0 ≤ K) (hC : 0 < C) (hf : ∀ s ∈ Set.Icc 0 p.1, |P.f (s, p.2)| ≤ K / C) (hfη : ∀ s ∈ Set.Icc 0 p.1, |ProfileHistories.parameterPartial P.f (s, p.2)| ≤ K / C) : |ProfileHistories.parameterPartial P.pressure p - deriv P.pressure0 p.2| ≤ 2 * p.1 * K ^ 2 / C ^ 2

theorem NavierStokes.ReferenceBounds.pressure_dot_bound {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 ≤ p.1) {K C : ℝ} (hf : |P.f p| ≤ K / C) : |p.1 * ProfileHistories.radialPartial P.pressure p| ≤ p.1 * K ^ 2 / C ^ 2

theorem NavierStokes.ReferenceBounds.p1_lower_from_source {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (h : ℝ) (hL : 0 < NaturalAxisData.L h p.2) {q : ℝ} (hq : 0 ≤ q) (hf : ∀ s ∈ Set.Icc 0 p.1, 0 < P.f (s, p.2)) (hmono : AntitoneOn (fun (s : ℝ) => P.f (s, p.2)) (Set.Icc 0 p.1)) (hsource : ∀ s ∈ Set.Icc 0 p.1, q ≤ sourceQ P h (s, p.2)) : q * p.1 / (2 * NaturalAxisData.L h p.2) ≤ p1 P h p

theorem NavierStokes.ReferenceBounds.ns_deviation_bound {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (h : ℝ) (hL : 0 < NaturalAxisData.L h p.2) {Z ε : ℝ} (hsource : ∀ s ∈ Set.Icc 0 p.1, |P.axialSource h (s, p.2) - Z| ≤ ε) : |ns P h p - Z / NaturalAxisData.L h p.2| ≤ ε / NaturalAxisData.L h p.2

theorem NavierStokes.ReferenceBounds.p1_lower_from_initial {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (h : ℝ) (hL : 0 < NaturalAxisData.L h p.2) {a b q : ℝ} (ha : 0 < a) (haX : a ≤ p.1) (hb : 0 ≤ b) (hq : 0 ≤ q) (hf : ∀ s ∈ Set.Icc 0 p.1, 0 < P.f (s, p.2)) (hmono : AntitoneOn (fun (s : ℝ) => P.f (s, p.2)) (Set.Icc 0 p.1)) (hsource : ∀ s ∈ Set.Icc a p.1, q ≤ sourceQ P h (s, p.2)) (hinit : b ≤ p1 P h (a, p.2)) : b * a / p.1 + q / (2 * NaturalAxisData.L h p.2) * (p.1 - a ^ 2 / p.1) ≤ p1 P h p

theorem NavierStokes.ReferenceBounds.p1_equation {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (hf : P.f p ≠ 0) (h : ℝ) : p.1 * deriv (fun (x : ℝ) => p1 P h (x, p.2)) p.1 + logSlope P p * p1 P h p = p.1 * sourceQ P h p / NaturalAxisData.L h p.2

theorem NavierStokes.ReferenceBounds.ns_equation {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : p.1 ≠ 0) (h : ℝ) : p.1 * deriv (fun (x : ℝ) => ns P h (x, p.2)) p.1 + ns P h p = P.axialSource h p / NaturalAxisData.L h p.2

theorem NavierStokes.ReferenceBounds.lower_comparison_preserves {X a L b q : ℝ} (ha : 0 < a) (haX : a ≤ X) (hL : 0 < L) (hq : 0 ≤ q) (hqa : b * L ≤ q * a) : b ≤ b * a / X + q / (2 * L) * (X - a ^ 2 / X)

theorem NavierStokes.ReferenceBounds.p1_preserves_lower {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (h : ℝ) (hL : 0 < NaturalAxisData.L h p.2) {a b q : ℝ} (ha : 0 < a) (haX : a ≤ p.1) (hb : 0 ≤ b) (hq : 0 ≤ q) (hqa : b * NaturalAxisData.L h p.2 ≤ q * a) (hf : ∀ s ∈ Set.Icc 0 p.1, 0 < P.f (s, p.2)) (hmono : AntitoneOn (fun (s : ℝ) => P.f (s, p.2)) (Set.Icc 0 p.1)) (hsource : ∀ s ∈ Set.Icc a p.1, q ≤ sourceQ P h (s, p.2)) (hinit : b ≤ p1 P h (a, p.2)) : b ≤ p1 P h p

theorem NavierStokes.ReferenceBounds.p1_at_hundred_gt_three {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {η h : ℝ} (hp : (100, η) ∈ D.carrier) (hL : 0 < NaturalAxisData.L h η) (hL1 : NaturalAxisData.L h η ≤ 1) (hf : ∀ s ∈ Set.Icc 0 100, 0 < P.f (s, η)) (hmono : AntitoneOn (fun (s : ℝ) => P.f (s, η)) (Set.Icc 0 100)) (hsource : ∀ s ∈ Set.Icc 0 100, 12 / 5 ≤ sourceQ P h (s, η)) : 3 < p1 P h (100, η)

theorem NavierStokes.ReferenceBounds.p2_large_of_small_f {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hX : 0 < p.1) (hX110 : p.1 ≤ 110) (h : ℝ) {a K C ν : ℝ} (ha : 0 < a) (haX : a ≤ p.1) : 0 < K → ∀ (hC : 0 < C) (hν : 0 < ν) (hf : 0 < P.f p) (hfbound : P.f p ≤ K / C) (hn : ν ≤ |ns P h p|) (hlarge : 18 * K / (a * ν) < C), 6 / 5 < |p2 P h p|

theorem NavierStokes.ReferenceBounds.cone_margin_of_dichotomy {a b : ℝ} (ha : 0 < a) (hlarge : 23 / 10 ≤ a ∨ 6 / 5 < |b|) : 9 / 4 < a + b ^ 2 / a

Uniform source estimates from bounded low-level jets

The compact variables below are the normalized axial value and average jets, the positive natural angular value, and the bounded remainder of its parameter logarithmic derivative. They are not source or cone assumptions.

@[reducible, inline]

abbrev NavierStokes.ReferenceBounds.BoundedJets (B : ℝ) : Set (Fin 5 → ℝ)

Bounded jets: an abbreviation for Metric.closedBall (0 : Fin 5 → ℝ) B instance (B : ℝ) : CompactSpace (BoundedJets B) := isCompact_iff_compactSpace.mp (isCompact_closedBall _ _).

Equations

• NavierStokes.ReferenceBounds.BoundedJets B = Metric.closedBall 0 B

instance NavierStokes.ReferenceBounds.instCompactSpaceElemForallFinOfNatNatRealBoundedJets (B : ℝ) : CompactSpace ↑(BoundedJets B)

@[reducible, inline]

abbrev NavierStokes.ReferenceBounds.SourceParameter (B : ℝ) : Type

Source parameter: an abbreviation for NaturalEntrance.entranceSet × (Icc (0 : ℝ) 1 × BoundedJets B).

Equations

• NavierStokes.ReferenceBounds.SourceParameter B = (↑NavierStokes.NaturalEntrance.entranceSet × ↑(Set.Icc 0 1) × ↑(NavierStokes.ReferenceBounds.BoundedJets B))

noncomputable def NavierStokes.ReferenceBounds.qRemainder (h j σ : ℝ) (p : ProfileHistories.Point) (θ : ℝ) (v : Fin 5 → ℝ) (t r : ℝ) : ℝ

v 0 is the natural positive angular factor, v 1 the normalized axial value, v 2, v 3 the normalized radial-average jets, and v 4 the bounded parameter-log-gradient remainder.

Equations

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

theorem NavierStokes.ReferenceBounds.qRemainder_continuous (h j : ℝ) {σ : ℝ} (hσ : 0 < σ) : Continuous fun (z : ((ProfileHistories.Point × ℝ) × (Fin 5 → ℝ)) × ℝ × ℝ) => qRemainder h j σ z.1.1.1 z.1.1.2 z.1.2 z.2.1 z.2.2

noncomputable def NavierStokes.ReferenceBounds.qModel {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (B : ℝ) (p : SourceParameter B) (z : ℝ × ℝ) : ℝ

Q model, constructed using qRemainder.

Equations

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

theorem NavierStokes.ReferenceBounds.qModel_continuous {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (B : ℝ) (hσ : 0 < σ) : Continuous fun (p : SourceParameter B × ℝ × ℝ) => qModel v B p.1 p.2

theorem NavierStokes.ReferenceBounds.qModel_at_chi_zero {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (B : ℝ) (hσ : 0 < σ) (p : SourceParameter B) (hchi : NaturalAxisData.chi h j σ (↑p.1).2 = 0) : qModel v B p 0 = -NaturalAxisData.W h j (↑p.1).2 - h * (1 - 2 * (↑p.1).2 * NaturalAxisData.U j (↑p.1).2)

theorem NavierStokes.ReferenceBounds.qModel_uniform_lower {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (B : ℝ) {K : ℝ} (hK : 0 ≤ K) : ∃ (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ (p : SourceParameter B) (e : ℝ), |e| ≤ K / Λ → 47 / 50 * NaturalAxisData.L h (↑p.1).2 * Λ * NaturalAxisData.chi h j σ (↑p.1).2 + 12 / 5 < NaturalAxisData.L h (↑p.1).2 * Λ * NaturalAxisData.chi h j σ (↑p.1).2 + qModel v B p (1 / Λ, e)

Uniformity in all bounded reference jets is proved before the scale and normalization are chosen. The growing term supplies no help at χ=0; there the concrete axis source supplies the positive margin.

@[reducible, inline]

abbrev NavierStokes.ReferenceBounds.AxialSourceParameter (B : ℝ) : Type

Axial source parameter: an abbreviation for Icc (-1 : ℝ) 1 × BoundedJets B.

Equations

• NavierStokes.ReferenceBounds.AxialSourceParameter B = (↑(Set.Icc (-1) 1) × ↑(NavierStokes.ReferenceBounds.BoundedJets B))

noncomputable def NavierStokes.ReferenceBounds.nModel (h j : ℝ) (P0 : ℝ → ℝ) (B : ℝ) (p : AxialSourceParameter B) (z : Fin 4 → ℝ) : ℝ

The axial source written in normalized axial jets and the actual three pressure increments. Its zero-perturbation value is exactly Z*.

Equations

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

theorem NavierStokes.ReferenceBounds.nModel_continuous (h j : ℝ) {P0 : ℝ → ℝ} (hP0 : ContDiff ℝ (↑⊤) P0) (B : ℝ) : Continuous fun (p : AxialSourceParameter B × (Fin 4 → ℝ)) => nModel h j P0 B p.1 p.2

theorem NavierStokes.ReferenceBounds.nModel_zero (h j : ℝ) (P0 : ℝ → ℝ) (B : ℝ) (p : AxialSourceParameter B) : nModel h j P0 B p 0 = NaturalAxisData.Z h j P0 ↑p.1

theorem NavierStokes.ReferenceBounds.nModel_uniform_error (h j : ℝ) {P0 : ℝ → ℝ} (hP0 : ContDiff ℝ (↑⊤) P0) (B : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (p : AxialSourceParameter B) (z : Fin 4 → ℝ), ‖z‖ < δ → |nModel h j P0 B p z - NaturalAxisData.Z h j P0 ↑p.1| < ε

The compact models are the actual profile sources

theorem NavierStokes.ReferenceBounds.average_error_bound {D : ProfileHistories.RadialDomain} {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) {Λ b B : ℝ} (hbound : ∀ t ∈ Set.Icc 0 1, |Λ * (F (t * p.1, p.2) - b)| ≤ B) : |Λ * (ProfileHistories.average F p - b)| ≤ B

noncomputable def NavierStokes.ReferenceBounds.qJets {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (j σ h Λ φ : ℝ) (p : ProfileHistories.Point) : Fin 5 → ℝ

Q jets as an element of Fin 5 → ℝ.

Equations

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

noncomputable def NavierStokes.ReferenceBounds.nJets {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (j Λ : ℝ) (p : ProfileHistories.Point) : Fin 5 → ℝ

N jets as an element of Fin 5 → ℝ.

Equations

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

noncomputable def NavierStokes.ReferenceBounds.pressureJets {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Λ : ℝ) (p : ProfileHistories.Point) : Fin 4 → ℝ

Pressure jets, given by ![1 / Λ, P.pressure p - P.pressure0 p.2, parameterPartial P.pressure p - deriv P.pressure0 p.2, p.1 * P.f p ^ 2].

Equations

• NavierStokes.ReferenceBounds.pressureJets P Λ p = ![1 / Λ, P.pressure p - P.pressure0 p.2, NavierStokes.ProfileHistories.parameterPartial P.pressure p - deriv P.pressure0 p.2, p.1 * P.f p ^ 2]

theorem NavierStokes.ReferenceBounds.sourceQ_model {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h j σ : ℝ) {Λ φ Y θ r : ℝ} (hΛ : Λ ≠ 0) (hφ : 1 / 8 ≤ φ) (p : ProfileHistories.Point) (hrad : p.1 * ProfileHistories.radialPartial P.f p / P.f p = θ * Y * r / φ) : sourceQ P h p = NaturalAxisData.L h p.2 * Λ * NaturalAxisData.chi h j σ p.2 + qRemainder h j σ (Y, p.2) θ (qJets P j σ h Λ φ p) (1 / Λ) r

theorem NavierStokes.ReferenceBounds.sourceN_model {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h j : ℝ) {Λ B : ℝ} (hΛ : Λ ≠ 0) (p : ProfileHistories.Point) (hη : p.2 ∈ Set.Icc (-1) 1) (hv : nJets P j Λ p ∈ Metric.closedBall 0 B) : P.axialSource h p = nModel h j P.pressure0 B (⟨p.2, hη⟩, ⟨nJets P j Λ p, hv⟩) (pressureJets P Λ p)

theorem NavierStokes.ReferenceBounds.qJets_bound {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h j σ : ℝ) {Λ B φ : ℝ} (hB : 0 ≤ B) {p : ProfileHistories.Point} (hφ : |φ| ≤ B) (hu : |Λ * (P.U p - NaturalAxisData.U j p.2)| ≤ B) (hv : |Λ * (P.Ubar p - NaturalAxisData.U j p.2)| ≤ B) (hvη : |Λ * (ProfileHistories.average (ProfileHistories.parameterPartial P.U) p - 4)| ≤ B) (hfη : |ProfileHistories.parameterPartial P.f p / P.f p - Λ * NaturalAxisCoefficients.realGradient h j σ p.2| ≤ B) : qJets P j σ h Λ φ p ∈ Metric.closedBall 0 B

theorem NavierStokes.ReferenceBounds.nJets_bound {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (j : ℝ) {Λ B : ℝ} (hB : 0 ≤ B) {p : ProfileHistories.Point} (hu : |Λ * (P.U p - NaturalAxisData.U j p.2)| ≤ B) (huη : |Λ * (ProfileHistories.parameterPartial P.U p - 4)| ≤ B) (hv : |Λ * (P.Ubar p - NaturalAxisData.U j p.2)| ≤ B) (hvη : |Λ * (ProfileHistories.average (ProfileHistories.parameterPartial P.U) p - 4)| ≤ B) (huX : |Λ * (p.1 * ProfileHistories.radialPartial P.U p)| ≤ B) : nJets P j Λ p ∈ Metric.closedBall 0 B

Exact agreement with the natural entrance histories

theorem NavierStokes.ReferenceBounds.radialPartial_natural {F : ProfileHistories.Field} {p : ProfileHistories.Point} (hF : ContDiffAt ℝ (↑⊤) F p) : ProfileHistories.radialPartial F p = NaturalAxisBridge.partialY F p

theorem NavierStokes.ReferenceBounds.parameterPartial_natural {F : ProfileHistories.Field} {p : ProfileHistories.Point} (hF : ContDiffAt ℝ (↑⊤) F p) : ProfileHistories.parameterPartial F p = NaturalAxisBridge.partialEta F p

theorem NavierStokes.ReferenceBounds.natural_average_eq {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.ReferenceBounds.natural_average_eventuallyEq {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 =ᶠ[nhds p] V

theorem NavierStokes.ReferenceBounds.ref_natural_eventuallyEq (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : p.1 < N.endpoint * Real.exp δ) : N.refF δ =ᶠ[nhds p] N.f ∧ N.refU δ =ᶠ[nhds p] N.U

theorem NavierStokes.ReferenceBounds.average_refU_eq (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : p.1 ≤ N.endpoint * Real.exp δ) : ProfileHistories.average (N.refU δ) p = ProfileHistories.average N.U p

theorem NavierStokes.ReferenceBounds.average_refU_eventuallyEq (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : p.1 < N.endpoint * Real.exp δ) : ProfileHistories.average (N.refU δ) =ᶠ[nhds p] ProfileHistories.average N.U

noncomputable def NavierStokes.ReferenceBounds.referenceProfiles {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) : ProfileHistories.Profiles (ReferencePath.Input.ofNatural hΛ F.family).radialDomain

All pressure and stock fields of this profile are the literal histories of the constructed reference continuation.

Equations

• NavierStokes.ReferenceBounds.referenceProfiles F hΛ hδ hδT hP0 = (NavierStokes.ReferencePath.Input.ofNatural hΛ F.family).histories hδ hδT P0 hP0

theorem NavierStokes.ReferenceBounds.reference_mem {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {p : ProfileHistories.Point} (hX : 0 ≤ p.1) (hη : p.2 ∈ Set.Icc (-1) 1) : p ∈ (ReferencePath.Input.ofNatural hΛ F.family).radialDomain.carrier

theorem NavierStokes.ReferenceBounds.endpoint_strict_collar {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {δ : ℝ} (hδ : 0 < δ) : 4 / Λ < (ReferencePath.Input.ofNatural hΛ F.family).endpoint * Real.exp δ

theorem NavierStokes.ReferenceBounds.reference_sourceQ_natural {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) (hX : p.1 ≤ 4 / Λ) : sourceQ (referenceProfiles F hΛ hδ hδT hP0) h p = NaturalEntrance.Sq h F.family.f F.family.U F.family.Ubar p

theorem NavierStokes.ReferenceBounds.reference_p1_natural {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) {p : ProfileHistories.Point} (hη : p.2 ∈ Set.Icc (-1) 1) (hX : 0 < p.1) (ha : p.1 ≤ 4 / Λ) : p1 (referenceProfiles F hΛ hδ hδT hP0) h p = NaturalEntrance.p1 F.family.f p

theorem NavierStokes.ReferenceBounds.natural_entrance_of_logTime {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) (hΛ : 0 < Λ) {p : ProfileHistories.Point} (hX : 0 < p.1) (hη : p.2 ∈ Set.Icc (-1) 1) (ht : (ReferencePath.Input.ofNatural hΛ E.profile.family).logTime p.1 < ReferencePath.rampLimit) : NaturalProfile.rescalePoint Λ p ∈ NaturalEntrance.entranceSet

theorem NavierStokes.ReferenceBounds.reference_radial_nonpos {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) (hΛ : 0 < Λ) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hX : 0 < p.1) (hη : p.2 ∈ Set.Icc (-1) 1) : ProfileHistories.radialPartial (referenceProfiles E.profile hΛ hδ hδT hP0).f p ≤ 0

theorem NavierStokes.ReferenceBounds.reference_logSlope_le_one {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) (hΛ : 0 < Λ) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hX : 0 ≤ p.1) (hη : p.2 ∈ Set.Icc (-1) 1) : logSlope (referenceProfiles E.profile hΛ hδ hδT hP0) p ≤ 1

theorem NavierStokes.ReferenceBounds.reference_antitone {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) (hΛ : 0 < Λ) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {R η : ℝ} : 0 ≤ R → ∀ (hη : η ∈ Set.Icc (-1) 1), AntitoneOn (fun (X : ℝ) => (referenceProfiles E.profile hΛ hδ hδT hP0).f (X, η)) (Set.Icc 0 R)

A normalization chosen before the cutoff time controls pressure

theorem NavierStokes.ReferenceBounds.pressureJets_small {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : p.1 ∈ Set.Icc 0 110) {Λ C K ε : ℝ} (hε : 0 < ε) (hK : 0 ≤ K) (hΛ : 1 + 1 / ε ≤ Λ) (hC : 1 + 220 * K ^ 2 / ε ≤ C) (hf : ∀ s ∈ Set.Icc 0 p.1, |P.f (s, p.2)| ≤ K / C) (hfη : ∀ s ∈ Set.Icc 0 p.1, |ProfileHistories.parameterPartial P.f (s, p.2)| ≤ K / C) : ‖pressureJets P Λ p‖ < ε

Cone comparison for the actual reference histories

noncomputable def NavierStokes.ReferenceBounds.holdRegion : Set ProfileHistories.Point

Hold region, given by Icc (0 : ℝ) 110 ×ˢ Icc (-1 : ℝ) 1.

Equations

• NavierStokes.ReferenceBounds.holdRegion = Set.Icc 0 110 ×ˢ Set.Icc (-1) 1

structure NavierStokes.ReferenceBounds.ReferenceBoundsOnHold {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) : Prop

Reference bounds on hold data, collecting source_lower, logarithmic_slope, first_positive, cone_margin, at_hundred.

• source_lower (p : ProfileHistories.Point) : p ∈ holdRegion → 47 / 50 * NaturalAxisData.L h p.2 * Λ * NaturalAxisData.chi h j σ p.2 + 12 / 5 < sourceQ (referenceProfiles F hΛ hδ hδT hP0) h p
• logarithmic_slope (p : ProfileHistories.Point) : p ∈ holdRegion → logSlope (referenceProfiles F hΛ hδ hδT hP0) p ≤ 1
• first_positive (p : ProfileHistories.Point) : p ∈ holdRegion → 0 < p.1 → 0 < p1 (referenceProfiles F hΛ hδ hδT hP0) h p
• cone_margin (p : ProfileHistories.Point) : p ∈ holdRegion → 4 / Λ ≤ p.1 → 9 / 4 < coneSize (referenceProfiles F hΛ hδ hδT hP0) h p
• at_hundred (η : ℝ) : η ∈ Set.Icc (-1) 1 → 3 < p1 (referenceProfiles F hΛ hδ hδT hP0) h (100, η)

theorem NavierStokes.ReferenceBounds.bounds_from_sources {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) (hΛ : 0 < Λ) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {K ν : ℝ} (hK : 0 < K) (hν : 0 < ν) (hC : 0 < C) (hcut : ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisData.Z h j P0 η| ≤ ν → 99 / 100 < NaturalAxisData.chi h j σ η) (hCbig : 18 * K / (4 / Λ * (ν / 2)) < C) (hq : ∀ p ∈ holdRegion, 47 / 50 * NaturalAxisData.L h p.2 * Λ * NaturalAxisData.chi h j σ p.2 + 12 / 5 < sourceQ (referenceProfiles E.profile hΛ hδ hδT hP0) h p) (hn : ∀ p ∈ holdRegion, |(referenceProfiles E.profile hΛ hδ hδT hP0).axialSource h p - NaturalAxisData.Z h j P0 p.2| < ν / 2) (hfbound : ∀ p ∈ holdRegion, |(referenceProfiles E.profile hΛ hδ hδT hP0).f p| ≤ K / C) : ReferenceBoundsOnHold E.profile hΛ hδ hδT hP0

This comparison uses only the actual primitive-defined stocks. The source bounds are supplied below by the compact model and the concrete jet theorem.

Passing from the bounded concrete jets to the sources

theorem NavierStokes.ReferenceBounds.holdRegion_scale {p : ProfileHistories.Point} (hp : p ∈ holdRegion) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (t * p.1, p.2) ∈ holdRegion

theorem NavierStokes.ReferenceBounds.normalized_history_bounds {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {Λ B j : ℝ} (hU : ∀ p ∈ holdRegion, |Λ * (P.U p - NaturalAxisData.U j p.2)| ≤ B) (hUη : ∀ p ∈ holdRegion, |Λ * (ProfileHistories.parameterPartial P.U p - 4)| ≤ B) {p : ProfileHistories.Point} (hp : p ∈ holdRegion) (hpD : p ∈ D.carrier) : |Λ * (P.Ubar p - NaturalAxisData.U j p.2)| ≤ B ∧ |Λ * (ProfileHistories.average (ProfileHistories.parameterPartial P.U) p - 4)| ≤ B

theorem NavierStokes.ReferenceBounds.sourceQ_uniform_threshold {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {B K : ℝ} (hB : 0 ≤ B) (hK : 0 ≤ K) : ∃ M > 0, ∀ (Λ : ℝ), M ≤ Λ → ∀ {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) (Y θ φ e : ℝ), (Y, p.2) ∈ NaturalEntrance.entranceSet → θ ∈ Set.Icc 0 1 → 1 / 8 ≤ φ → φ ≤ B → |e| ≤ K / Λ → |Λ * (P.U p - NaturalAxisData.U j p.2)| ≤ B → |Λ * (P.Ubar p - NaturalAxisData.U j p.2)| ≤ B → |Λ * (ProfileHistories.average (ProfileHistories.parameterPartial P.U) p - 4)| ≤ B → |ProfileHistories.parameterPartial P.f p / P.f p - Λ * NaturalAxisCoefficients.realGradient h j σ p.2| ≤ B → p.1 * ProfileHistories.radialPartial P.f p / P.f p = θ * Y * (NaturalEntrance.sourceJets ⋯ (NaturalEntrance.referencePair v) (Y, p.2) 1 + e) / φ → 47 / 50 * NaturalAxisData.L h p.2 * Λ * NaturalAxisData.chi h j σ p.2 + 12 / 5 < sourceQ P h p

The source threshold is fixed before Λ and C. Every occurrence of a history or derivative on the right is an actual operation on P.

The ordered, constructed reference continuation

theorem NavierStokes.ReferenceBounds.exists_reference_bounds {h j σ ν : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hP0 : ContDiff ℝ (↑⊤) P0) (hν : 0 < ν) (hcut : ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisData.Z h j P0 η| ≤ ν → 99 / 100 < NaturalAxisData.chi h j σ η) : ∃ M > 0, ∀ (Λ : ℝ) (hΛ : 0 < Λ), M ≤ Λ → ∃ C₀ > 0, ∀ (C : ℝ), C₀ ≤ C → ∃ (E : NaturalEntrance.EntranceProfile d Λ C), ∃ r > 0, ∀ (δ : ℝ) (hδ : 0 < δ), δ < r → ∃ (hδT : 2 * δ < ReferencePath.rampLimit), ReferenceBoundsOnHold E.profile hΛ hδ hδT hP0

Lemma 5.2 for the actual reference path and its literal histories. The bounded jet constants and the scale threshold precede Λ; the pressure normalization threshold precedes C; the short cutoff time is chosen last. No source estimate, stock estimate, or cone condition is an input.

noncomputable def NavierStokes.ActivationContinuation.shearSize (a b : ℝ) : ℝ

Shear size, given by a * (1 + (b / a) ^ 2).

Equations

• NavierStokes.ActivationContinuation.shearSize a b = a * (1 + (b / a) ^ 2)

noncomputable def NavierStokes.ActivationContinuation.projection (p q a b : ℝ) : ℝ

Projection, given by p + q * (b / a).

Equations

• NavierStokes.ActivationContinuation.projection p q a b = p + q * (b / a)

noncomputable def NavierStokes.ActivationContinuation.transverse (p q a b : ℝ) : ℝ

Transverse, given by q - p * (b / a).

Equations

• NavierStokes.ActivationContinuation.transverse p q a b = q - p * (b / a)

structure NavierStokes.ActivationContinuation.Relaxed (a b p q : ℝ) : Prop

Relaxed data, collecting first_positive, projection_positive, cone.

• first_positive : 0 < a
• projection_positive : 2 < projection p q a b
• cone : shearSize a b < ConeAlgebra.coneBound (projection p q a b) (transverse p q a b)

noncomputable def NavierStokes.ActivationContinuation.projectionConstant (M : ℝ) : ℝ

Projection constant, given by 1 + 2 * M + M ^ 2.

Equations

• NavierStokes.ActivationContinuation.projectionConstant M = 1 + 2 * M + M ^ 2

noncomputable def NavierStokes.ActivationContinuation.speedConstant (M : ℝ) : ℝ

Speed constant, given by M * (1 + 4 * M ^ 2).

Equations

• NavierStokes.ActivationContinuation.speedConstant M = M * (1 + 4 * M ^ 2)

theorem NavierStokes.ActivationContinuation.projectionConstant_pos {M : ℝ} (hM : 0 ≤ M) : 0 < projectionConstant M

theorem NavierStokes.ActivationContinuation.speedConstant_nonneg {M : ℝ} (hM : 0 ≤ M) : 0 ≤ speedConstant M

theorem NavierStokes.ActivationContinuation.projection_identity (A B p q θ R : ℝ) : p + q * (θ * (B / A) * R) - (A + θ * B ^ 2 / A) = p - A + (q - B) * θ * (B / A) * R + θ * B * (B / A) * (R - 1)

The axial shutoff factor occurs once in the limiting projection.

theorem NavierStokes.ActivationContinuation.projection_comparison {A B p q θ R M ε : ℝ} (hM : 0 ≤ M) (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (hθ : θ ∈ Set.Icc 0 1) (hB : |B| ≤ M) (hBA : |B / A| ≤ M) (hp : |p - A| ≤ ε) (hq : |q - B| ≤ ε) (hR : |R - 1| ≤ ε) : |p + q * (θ * (B / A) * R) - (A + θ * B ^ 2 / A)| ≤ ε * projectionConstant M

theorem NavierStokes.ActivationContinuation.damped_shear_ratio {κ A : ℝ} (hκ : κ ≠ 0) (hA : A ≠ 0) (θ B R : ℝ) : κ * θ * B * R / (κ * A) = θ * (B / A) * R

theorem NavierStokes.ActivationContinuation.damped_shear_bound {κ A B θ R M : ℝ} (hκ : 0 < κ) (hA : 0 < A) (hM : 0 ≤ M) (hAM : A ≤ M) (hθ : θ ∈ Set.Icc 0 1) (hBA : |B / A| ≤ M) (hR : |R| ≤ 2) : shearSize (κ * A) (κ * θ * B * R) ≤ κ * speedConstant M

theorem NavierStokes.ActivationContinuation.damped_relaxed {κ A B p q θ R M ε : ℝ} (hκ : 0 < κ) (hA : 0 < A) (hM : 0 ≤ M) (hAM : A ≤ M) (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (hθ : θ ∈ Set.Icc 0 1) (hB : |B| ≤ M) (hBA : |B / A| ≤ M) (hp : |p - A| ≤ ε) (hq : |q - B| ≤ ε) (hR : |R - 1| ≤ ε) (hprojection : 9 / 4 ≤ A + θ * B ^ 2 / A) (herror : ε * projectionConstant M ≤ 1 / 8) (hspeed : κ * speedConstant M ≤ 1) : Relaxed (κ * A) (κ * θ * B * R) p q

Uniform finite-dimensional comparison for both the constant-damping segment and the axial shutoff. No inverse power of the damping is used.

theorem NavierStokes.ActivationContinuation.zero_axial_relaxed {a p q : ℝ} (ha : 0 < a) (ha2 : a ≤ 2) (hp : 2 < p) : Relaxed a 0 p q

theorem NavierStokes.ActivationContinuation.convex_final_shear {a θ : ℝ} (ha : 0 < a) (ha4 : a ≤ 4 / 5) (hθ : θ ∈ Set.Icc 0 1) : 0 < (1 - θ) * a + θ * (4 / 5) ∧ (1 - θ) * a + θ * (4 / 5) ≤ 4 / 5

Physical cone coordinates

noncomputable def NavierStokes.ActivationContinuation.shearA {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) : ℝ

Shear A, given by -2 * p.1 * radialPartial P.f p / P.f p.

Equations

• NavierStokes.ActivationContinuation.shearA P p = -2 * p.1 * NavierStokes.ProfileHistories.radialPartial P.f p / P.f p

noncomputable def NavierStokes.ActivationContinuation.shearB {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) : ℝ

Shear B, given by -2 * p.1 * radialPartial P.U p / P.E p.

Equations

• NavierStokes.ActivationContinuation.shearB P p = -2 * p.1 * NavierStokes.ProfileHistories.radialPartial P.U p / P.E p

noncomputable def NavierStokes.ActivationContinuation.IsRelaxed {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : Prop

Is relaxed, given by Relaxed (shearA P p) (shearB P p) (ReferenceBounds.p1 P h p) (ReferenceBounds.p2 P h p).

Equations

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

theorem NavierStokes.ActivationContinuation.logSlope_eq_shear {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) : ReferenceBounds.logSlope P p = 1 - shearA P p / 2

theorem NavierStokes.ActivationContinuation.zero_axial_relaxed_profile {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {h : ℝ} {p : ProfileHistories.Point} (ha : 0 < shearA P p) (ha2 : shearA P p ≤ 2) (hu : ProfileHistories.radialPartial P.U p = 0) (hp : 2 < ReferenceBounds.p1 P h p) : IsRelaxed P h p

An exact barrier for the final constant-slope hold

noncomputable def NavierStokes.ActivationContinuation.weightedGap (g : ℝ → ℝ) (b X : ℝ) : ℝ

Weighted gap, given by Real.exp ((3 / 5 : ℝ) * Real.log X) * (g X - b).

Equations

• NavierStokes.ActivationContinuation.weightedGap g b X = Real.exp (3 / 5 * Real.log X) * (g X - b)

theorem NavierStokes.ActivationContinuation.weightedGap_hasDerivAt {g : ℝ → ℝ} {g' X : ℝ} (hX : 0 < X) (hg : HasDerivAt g g' X) (b : ℝ) : HasDerivAt (weightedGap g b) (Real.exp (3 / 5 * Real.log X) / X * (X * g' + 3 / 5 * g X - 3 / 5 * b)) X

theorem NavierStokes.ActivationContinuation.scalar_hold_barrier {g : ℝ → ℝ} {a X b : ℝ} (ha : 0 < a) (haX : a ≤ X) (hg : ∀ t ∈ Set.Icc a X, DifferentiableAt ℝ g t) (heq : ∀ t ∈ Set.Icc a X, 3 / 5 * b ≤ t * deriv g t + 3 / 5 * g t) (hinit : b < g a) : b < g X

theorem NavierStokes.ActivationContinuation.actual_hold_barrier {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {h η a X : ℝ} (ha : 2 ≤ a) (haX : a ≤ X) (hL : 0 < NaturalAxisData.L h η) (hL1 : NaturalAxisData.L h η ≤ 1) (hmem : ∀ t ∈ Set.Icc a X, (t, η) ∈ D.carrier) (hf : ∀ t ∈ Set.Icc a X, 0 < P.f (t, η)) (hl : ∀ t ∈ Set.Icc a X, ReferenceBounds.logSlope P (t, η) = 3 / 5) (hs : ∀ t ∈ Set.Icc a X, 1 < ReferenceBounds.sourceQ P h (t, η)) (hinit : 2 < ReferenceBounds.p1 P h (a, η)) : 2 < ReferenceBounds.p1 P h (X, η)

The final hold source is derived from the axis model

noncomputable def NavierStokes.ActivationContinuation.holdVector (v : Fin 5 → ℝ) : Fin 5 → ℝ

Hold vector, given by ![1, v 1, v 2, v 3, v 4].

Equations

• NavierStokes.ActivationContinuation.holdVector v = ![1, v 1, v 2, v 3, v 4]

noncomputable def NavierStokes.ActivationContinuation.holdRemainder (h j σ η : ℝ) (v : Fin 5 → ℝ) (t : ℝ) : ℝ

Hold remainder, given by ReferenceBounds.qRemainder h j σ (1, η) 1 (holdVector v) t (-2 / 5).

Equations

• NavierStokes.ActivationContinuation.holdRemainder h j σ η v t = NavierStokes.ReferenceBounds.qRemainder h j σ (1, η) 1 (NavierStokes.ActivationContinuation.holdVector v) t (-2 / 5)

@[reducible, inline]

abbrev NavierStokes.ActivationContinuation.HoldParameter (B : ℝ) : Type

Hold parameter: an abbreviation for Icc (-1 : ℝ) 1 × ReferenceBounds.BoundedJets B.

Equations

• NavierStokes.ActivationContinuation.HoldParameter B = (↑(Set.Icc (-1) 1) × ↑(NavierStokes.ReferenceBounds.BoundedJets B))

noncomputable def NavierStokes.ActivationContinuation.holdModel (h j σ B : ℝ) (p : HoldParameter B) (t : ℝ) : ℝ

Hold model, given by holdRemainder h j σ p.1.val p.2.val t.

Equations

• NavierStokes.ActivationContinuation.holdModel h j σ B p t = NavierStokes.ActivationContinuation.holdRemainder h j σ (↑p.1) (↑p.2) t

theorem NavierStokes.ActivationContinuation.holdModel_continuous (h j B : ℝ) {σ : ℝ} (hσ : 0 < σ) : Continuous fun (p : HoldParameter B × ℝ) => holdModel h j σ B p.1 p.2

theorem NavierStokes.ActivationContinuation.hold_axis_source_lower {h j η : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hη : η ∈ Set.Icc (-1) 1) : 17 / 10 < -(3 / 5) * NaturalAxisData.W h j η - h * (1 - 2 * η * NaturalAxisData.U j η)

theorem NavierStokes.ActivationContinuation.holdModel_chi_zero (h j B : ℝ) {σ : ℝ} (hσ : 0 < σ) (p : HoldParameter B) (hchi : NaturalAxisData.chi h j σ ↑p.1 = 0) : holdModel h j σ B p 0 = -(3 / 5) * NaturalAxisData.W h j ↑p.1 - h * (1 - 2 * ↑p.1 * NaturalAxisData.U j ↑p.1)

theorem NavierStokes.ActivationContinuation.holdModel_uniform_lower {h j σ : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (B : ℝ) : ∃ M > 0, ∀ (Λ : ℝ), M ≤ Λ → ∀ (p : HoldParameter B), 5 / 4 < NaturalAxisData.L h ↑p.1 * Λ * NaturalAxisData.chi h j σ ↑p.1 + holdModel h j σ B p (1 / Λ)

theorem NavierStokes.ActivationContinuation.hold_source_identity {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h j σ : ℝ) {Λ : ℝ} (hΛ : Λ ≠ 0) (p : ProfileHistories.Point) (hl : ReferenceBounds.logSlope P p = 3 / 5) : ReferenceBounds.sourceQ P h p = NaturalAxisData.L h p.2 * Λ * NaturalAxisData.chi h j σ p.2 + holdRemainder h j σ p.2 (ReferenceBounds.qJets P j σ h Λ 1 p) (1 / Λ)

theorem NavierStokes.ActivationContinuation.actual_hold_source_threshold {h j σ B : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hB : 1 ≤ B) : ∃ M > 0, ∀ (Λ : ℝ), M ≤ Λ → ∀ {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point), p.2 ∈ Set.Icc (-1) 1 → ReferenceBounds.logSlope P p = 3 / 5 → |Λ * (P.U p - NaturalAxisData.U j p.2)| ≤ B → |Λ * (P.Ubar p - NaturalAxisData.U j p.2)| ≤ B → |Λ * (ProfileHistories.average (ProfileHistories.parameterPartial P.U) p - 4)| ≤ B → |ProfileHistories.parameterPartial P.f p / P.f p - Λ * NaturalAxisCoefficients.realGradient h j σ p.2| ≤ B → 5 / 4 < ReferenceBounds.sourceQ P h p

Uniform transfer of actual field and history jets to the stocks

theorem NavierStokes.ActivationContinuation.compact_vector_perturbation {K : Type u_1} {E : Type u_2} {F : Type u_3} [MetricSpace K] [CompactSpace K] [NormedAddCommGroup E] [ProperSpace E] [NormedAddCommGroup F] (G : K × E → F) (hG : Continuous G) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (p : K) (e : E), ‖e‖ < δ → ‖G (p, e) - G (p, 0)‖ < ε

@[reducible, inline]

abbrev NavierStokes.ActivationContinuation.StockJet : Type

Stock jet: an abbreviation for Fin 12 → ℝ.

Equations

• NavierStokes.ActivationContinuation.StockJet = (Fin 12 → ℝ)

noncomputable def NavierStokes.ActivationContinuation.stockJet {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) : StockJet

Stock jet as an element of StockJet.

Equations

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

noncomputable def NavierStokes.ActivationContinuation.stockOneMap (h : ℝ) (p : ProfileHistories.Point) (z : StockJet) : ℝ

Stock one map, given by ActivationStocks.stockOne h p.1 p.2 (z 0) (z 2) (z 3) (z 4) (z 5) (z 6) (z 7).

Equations

• NavierStokes.ActivationContinuation.stockOneMap h p z = NavierStokes.ActivationStocks.stockOne h p.1 p.2 (z 0) (z 2) (z 3) (z 4) (z 5) (z 6) (z 7)

noncomputable def NavierStokes.ActivationContinuation.stockTwoMap (h : ℝ) (p : ProfileHistories.Point) (z : StockJet) : ℝ

Stock two map, given by ActivationStocks.stockTwo h p.1 p.2 (z 0) (z 1) (z 2) (z 3) (z 8) (z 9) (z 10) (z 11).

Equations

• NavierStokes.ActivationContinuation.stockTwoMap h p z = NavierStokes.ActivationStocks.stockTwo h p.1 p.2 (z 0) (z 1) (z 2) (z 3) (z 8) (z 9) (z 10) (z 11)

theorem NavierStokes.ActivationContinuation.stockJet_coordinates {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (hf : P.f p ≠ 0) : stockOneMap h p (stockJet P p) = ReferenceBounds.p1 P h p ∧ stockTwoMap h p (stockJet P p) = ReferenceBounds.p2 P h p

@[reducible, inline]

abbrev NavierStokes.ActivationContinuation.StockBall (B : ℝ) : Set StockJet

Stock ball: an abbreviation for Metric.closedBall (0 : StockJet) B instance (B : ℝ) : CompactSpace (StockBall B) := isCompact_iff_compactSpace.mp (isCompact_closedBall _ _).

Equations

• NavierStokes.ActivationContinuation.StockBall B = Metric.closedBall 0 B

instance NavierStokes.ActivationContinuation.instCompactSpaceElemStockJetStockBall (B : ℝ) : CompactSpace ↑(StockBall B)

noncomputable def NavierStokes.ActivationContinuation.clippedStockMap (h μ : ℝ) (p : ProfileHistories.Point) (z e : StockJet) : Fin 3 → ℝ

Clipped stock map as an element of Fin 3 → ℝ.

Equations

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

theorem NavierStokes.ActivationContinuation.clippedStockMap_continuous {h j μ B : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hμ : 0 < μ) {S : Set ProfileHistories.Point} (hX : ∀ p ∈ S, 0 < p.1) (hη : ∀ p ∈ S, p.2 ∈ Set.Icc (-1) 1) : Continuous fun (q : (↑S × ↑(StockBall B)) × StockJet) => clippedStockMap h μ (↑q.1.1) (↑q.1.2) q.2

theorem NavierStokes.ActivationContinuation.uniform_stock_transfer {h j μ B ε : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hμ : 0 < μ) (hε : 0 < ε) {S : Set ProfileHistories.Point} (hS : IsCompact S) (hX : ∀ p ∈ S, 0 < p.1) (hη : ∀ p ∈ S, p.2 ∈ Set.Icc (-1) 1) : ∃ τ > 0, ∀ p ∈ S, ∀ (z w : StockJet), ‖z‖ ≤ B → 2 * μ ≤ z 0 → ‖w - z‖ < τ → μ < w 0 ∧ |stockOneMap h p w - stockOneMap h p z| < ε ∧ |stockTwoMap h p w - stockTwoMap h p z| < ε ∧ |z 0 / w 0 - 1| < ε

Uniform stock continuity on a bounded set of actual profile/history jets. The threshold is independent of the particular reference member.

The five history rows follow from actual first parameter jets

@[reducible, inline]

abbrev NavierStokes.ActivationContinuation.FieldJet : Type

Field jet: an abbreviation for Fin 4 → ℝ.

Equations

• NavierStokes.ActivationContinuation.FieldJet = (Fin 4 → ℝ)

noncomputable def NavierStokes.ActivationContinuation.fieldJet {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) : FieldJet

Field jet, given by ![P.f p, P.U p, parameterPartial P.f p, parameterPartial P.U p].

Equations

• NavierStokes.ActivationContinuation.fieldJet P p = ![P.f p, P.U p, NavierStokes.ProfileHistories.parameterPartial P.f p, NavierStokes.ProfileHistories.parameterPartial P.U p]

noncomputable def NavierStokes.ActivationContinuation.densityJet (X : ℝ) (z : FieldJet) : Fin 10 → ℝ

Density jet as an element of Fin 10 → ℝ.

Equations

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

theorem NavierStokes.ActivationContinuation.densityJet_continuous : Continuous fun (p : ℝ × FieldJet) => densityJet p.1 p.2

noncomputable def NavierStokes.ActivationContinuation.valueIndex (r : StressActivation.HistoryRow) : Fin 10

Value index, given by HistoryRow.rec (motive := fun _ => Fin 10) 0 2 4 6 8 r.

Equations

• NavierStokes.ActivationContinuation.valueIndex r = NavierStokes.StressActivation.HistoryRow.rec 0 2 4 6 8 r

noncomputable def NavierStokes.ActivationContinuation.derivativeIndex (r : StressActivation.HistoryRow) : Fin 10

Derivative index, given by HistoryRow.rec (motive := fun _ => Fin 10) 1 3 5 7 9 r.

Equations

• NavierStokes.ActivationContinuation.derivativeIndex r = NavierStokes.StressActivation.HistoryRow.rec 1 3 5 7 9 r

theorem NavierStokes.ActivationContinuation.densityJet_value {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : StressActivation.HistoryRow) (p : ProfileHistories.Point) : densityJet p.1 (fieldJet P p) (valueIndex r) = StressActivation.profileDensity P r p

theorem NavierStokes.ActivationContinuation.densityJet_derivative {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : StressActivation.HistoryRow) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) : densityJet p.1 (fieldJet P p) (derivativeIndex r) = ProfileHistories.parameterPartial (StressActivation.profileDensity P r) p

theorem NavierStokes.ActivationContinuation.profileHistory_parameter_formula {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : StressActivation.HistoryRow) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) : ProfileHistories.parameterPartial (StressActivation.profileHistory P r) p = deriv (StressActivation.profileInitial P r) p.2 + ProfileHistories.primitive (ProfileHistories.parameterPartial (StressActivation.profileDensity P r)) p

theorem NavierStokes.ActivationContinuation.profileHistory_difference {D E : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles E) (h0 : P.pressure0 = Q.pressure0) (r : StressActivation.HistoryRow) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hq : p ∈ E.carrier) : StressActivation.profileHistory P r p - StressActivation.profileHistory Q r p = ∫ (t : ℝ) in 0..p.1, StressActivation.profileDensity P r (t, p.2) - StressActivation.profileDensity Q r (t, p.2)

theorem NavierStokes.ActivationContinuation.profileHistory_parameter_difference {D E : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles E) (h0 : P.pressure0 = Q.pressure0) (r : StressActivation.HistoryRow) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hq : p ∈ E.carrier) : ProfileHistories.parameterPartial (StressActivation.profileHistory P r) p - ProfileHistories.parameterPartial (StressActivation.profileHistory Q r) p = ∫ (t : ℝ) in 0..p.1, ProfileHistories.parameterPartial (StressActivation.profileDensity P r) (t, p.2) - ProfileHistories.parameterPartial (StressActivation.profileDensity Q r) (t, p.2)

@[reducible, inline]

abbrev NavierStokes.ActivationContinuation.FieldBall (B : ℝ) : Set FieldJet

Field ball: an abbreviation for Metric.closedBall (0 : FieldJet) B instance (B : ℝ) : CompactSpace (FieldBall B) := isCompact_iff_compactSpace.mp (isCompact_closedBall _ _).

Equations

• NavierStokes.ActivationContinuation.FieldBall B = Metric.closedBall 0 B

instance NavierStokes.ActivationContinuation.instCompactSpaceElemFieldJetFieldBall (B : ℝ) : CompactSpace ↑(FieldBall B)

theorem NavierStokes.ActivationContinuation.uniform_density_transfer (B : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ τ > 0, ∀ X ∈ Set.Icc 0 110, ∀ (z w : FieldJet), ‖z‖ ≤ B → ‖w - z‖ < τ → ‖densityJet X w - densityJet X z‖ < ε

theorem NavierStokes.ActivationContinuation.short_integral_bound {f : ℝ → ℝ} {X ε : ℝ} (hX : X ∈ Set.Icc 0 110) (hε : 0 < ε) (hf : ∀ t ∈ Set.Icc 0 X, |f t| ≤ ε / 111) : |∫ (t : ℝ) in 0..X, f t| < ε

theorem NavierStokes.ActivationContinuation.field_to_stockJet_transfer (B : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ τ > 0, ∀ {D E : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles E), P.pressure0 = Q.pressure0 → ∀ p ∈ D.carrier, p ∈ E.carrier → p.1 ∈ Set.Icc 0 110 → (∀ t ∈ Set.Icc 0 p.1, ‖fieldJet Q (t, p.2)‖ ≤ B) → (∀ t ∈ Set.Icc 0 p.1, ‖fieldJet P (t, p.2) - fieldJet Q (t, p.2)‖ < τ) → ‖stockJet P p - stockJet Q p‖ < ε

Uniform first-jet closeness of actual fields gives uniform closeness of all five actual history rows and their first parameter derivatives.

theorem NavierStokes.ActivationContinuation.uniform_density_bound (B : ℝ) : ∃ K ≥ 0, ∀ X ∈ Set.Icc 0 110, ∀ (z : FieldJet), ‖z‖ ≤ B → ‖densityJet X z‖ ≤ K

theorem NavierStokes.ActivationContinuation.integral_bounded_length {f : ℝ → ℝ} {X K : ℝ} (hX : X ∈ Set.Icc 0 110) (hK : 0 ≤ K) (hf : ∀ t ∈ Set.Icc 0 X, |f t| ≤ K) : |∫ (t : ℝ) in 0..X, f t| ≤ 110 * K

theorem NavierStokes.ActivationContinuation.stockJet_uniform_bound {B B0 : ℝ} (hB : 0 ≤ B) (hB0 : 0 ≤ B0) : ∃ K > 0, ∀ {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D), ∀ p ∈ D.carrier, p.1 ∈ Set.Icc 0 110 → |P.pressure0 p.2| ≤ B0 → |deriv P.pressure0 p.2| ≤ B0 → (∀ t ∈ Set.Icc 0 p.1, ‖fieldJet P (t, p.2)‖ ≤ B) → ‖stockJet P p‖ ≤ K

A bounded actual first field jet gives a uniform bound for every stock input, including both pressure entries. This bound precedes the small ramps.

theorem NavierStokes.ActivationContinuation.uniform_stock_bound {h j μ B : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hμ : 0 < μ) {S : Set ProfileHistories.Point} (hS : IsCompact S) (hX : ∀ p ∈ S, 0 < p.1) (hη : ∀ p ∈ S, p.2 ∈ Set.Icc (-1) 1) : ∃ M > 0, ∀ p ∈ S, ∀ (z : StockJet), ‖z‖ ≤ B → μ ≤ z 0 → |stockOneMap h p z| ≤ M ∧ |stockTwoMap h p z| ≤ M

Uniform comparison constants from the concrete reference

theorem NavierStokes.ActivationContinuation.reference_first_lower {h j σ Λ C δ : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) (hΛ : 0 < Λ) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hb : ReferenceBounds.ReferenceBoundsOnHold E.profile hΛ hδ hδT hP0) {p : ProfileHistories.Point} (hp : p ∈ ReferenceBounds.holdRegion) (hX : 0 < p.1) : 6 / 5 * p.1 ≤ ReferenceBounds.p1 (ReferenceBounds.referenceProfiles E.profile hΛ hδ hδT hP0) h p

noncomputable def NavierStokes.ActivationContinuation.expJet (p : ℝ × ℝ) : ℝ × ℝ

Exp jet, given by (Real.exp p.1, Real.exp p.1 * p.2).

Equations

• NavierStokes.ActivationContinuation.expJet p = (Real.exp p.1, Real.exp p.1 * p.2)

theorem NavierStokes.ActivationContinuation.expJet_continuous : Continuous expJet

theorem NavierStokes.ActivationContinuation.expJet_uniform (B : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ τ > 0, ∀ (z w : ℝ × ℝ), ‖z‖ ≤ B → ‖w - z‖ < τ → ‖expJet w - expJet z‖ < ε

theorem NavierStokes.ActivationContinuation.comparison_tolerances {M : ℝ} (hM : 0 ≤ M) : ∃ (ε : ℝ) (κstar : ℝ), 0 < ε ∧ ε ≤ 1 ∧ 0 < κstar ∧ κstar < 1 ∧ ε * projectionConstant M ≤ 1 / 8 ∧ κstar * speedConstant M ≤ 1 ∧ κstar * M ≤ 4 / 5

theorem NavierStokes.ActivationContinuation.reference_fieldJet_bound {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {h j σ Λ C B K : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (hΛ : 1 ≤ Λ) (hC : 1 ≤ C) (hB : 0 ≤ B) (hK : 0 ≤ K) (hj : ReferenceJetBounds.JetBounds h j σ Λ C B K P.f P.U) {p : ProfileHistories.Point} (hp : p ∈ ReferenceBounds.holdRegion) : ‖fieldJet P p‖ ≤ K + B + 6

theorem NavierStokes.ActivationContinuation.pressure_initial_bound {P0 : ℝ → ℝ} (hP0 : ContDiff ℝ (↑⊤) P0) : ∃ B0 > 0, ∀ η ∈ Set.Icc (-1) 1, |P0 η| ≤ B0 ∧ |deriv P0 η| ≤ B0

theorem NavierStokes.ActivationContinuation.endpoint_field_continuous (N : ReferencePath.Input) : ContinuousOn (fun (η : ℝ) => N.f (N.endpoint, η)) (Set.Icc (-1) 1)

noncomputable def NavierStokes.ActivationContinuation.endpointLogJet (N : ReferencePath.Input) (η : ℝ) : ℝ × ℝ

Endpoint log jet, given by (Real.log (N.f (N.endpoint, η)), parameterPartial N.f (N.endpoint, η) / N.f (N.endpoint, η)).

Equations

• NavierStokes.ActivationContinuation.endpointLogJet N η = (Real.log (N.f (N.endpoint, η)), NavierStokes.ProfileHistories.parameterPartial N.f (N.endpoint, η) / N.f (N.endpoint, η))

theorem NavierStokes.ActivationContinuation.endpointLogJet_bound (N : ReferencePath.Input) : ∃ B0 ≥ 0, ∀ η ∈ Set.Icc (-1) 1, ‖endpointLogJet N η‖ ≤ B0

theorem NavierStokes.ActivationContinuation.reference_positive_uniform (N : ReferencePath.Input) : ∃ (μ : ℝ) (r : ℝ), 0 < μ ∧ 0 < r ∧ ∀ (δ : ℝ), 0 < δ → δ < r → ∀ (p : ProfileHistories.Point), N.endpoint ≤ p.1 → p.2 ∈ Set.Icc (-1) 1 → 2 * μ ≤ N.refF δ p

theorem NavierStokes.ActivationContinuation.reference_endpoint_control (N : ReferencePath.Input) {εU εF εL : ℝ} (hU : 0 < εU) (hF : 0 < εF) (hL : 0 < εL) : ∃ r > 0, ∀ (δ : ℝ), 0 < δ → δ < r → ReferenceJetBounds.TransitionControl N δ εU εF ∧ ∀ (p : ProfileHistories.Point), N.endpoint ≤ p.1 → p.2 ∈ Set.Icc (-1) 1 → |ProfileHistories.parameterPartial (N.refF δ) p / N.refF δ p - ProfileHistories.parameterPartial N.f (N.endpoint, p.2) / N.f (N.endpoint, p.2)| < εL

Ordered preparation and transfer of normalized source jets

theorem NavierStokes.ActivationContinuation.ordered_reference_preparation {h j σ ν : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hP0 : ContDiff ℝ (↑⊤) P0) (hν : 0 < ν) (hcut : ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisData.Z h j P0 η| ≤ ν → 99 / 100 < NaturalAxisData.chi h j σ η) : ∃ (B : ℝ) (M : ℝ), 1 < B ∧ 1 ≤ M ∧ ∀ (Λ : ℝ) (hΛ : 0 < Λ), M ≤ Λ → (∀ {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point), p.2 ∈ Set.Icc (-1) 1 → ReferenceBounds.logSlope P p = 3 / 5 → |Λ * (P.U p - NaturalAxisData.U j p.2)| ≤ B + 2 → |Λ * (P.Ubar p - NaturalAxisData.U j p.2)| ≤ B + 2 → |Λ * (ProfileHistories.average (ProfileHistories.parameterPartial P.U) p - 4)| ≤ B + 2 → |ProfileHistories.parameterPartial P.f p / P.f p - Λ * NaturalAxisCoefficients.realGradient h j σ p.2| ≤ B + 2 → 5 / 4 < ReferenceBounds.sourceQ P h p) ∧ ∃ (C0 : ℝ) (K : ℝ), 1 ≤ C0 ∧ 0 < K ∧ ∀ (C : ℝ), C0 ≤ C → ∃ (E : NaturalEntrance.EntranceProfile d Λ C), ∃ r > 0, ∀ (δ : ℝ) (hδ : 0 < δ), δ < r → ∃ (hδT : 2 * δ < ReferencePath.rampLimit), ReferenceBounds.ReferenceBoundsOnHold E.profile hΛ hδ hδT hP0 ∧ ReferenceJetBounds.JetBounds h j σ Λ C B K ((ReferencePath.Input.ofNatural hΛ E.profile.family).refF δ) ((ReferencePath.Input.ofNatural hΛ E.profile.family).refU δ)

The scale and pressure normalization are chosen before any small activation parameter. Both estimates concern the same actual REF fields.

theorem NavierStokes.ActivationContinuation.nearby_axial_bounds {D E : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles E) {h j σ Λ C B K : ℝ} (hΛ : 0 < Λ) (hj : ReferenceJetBounds.JetBounds h j σ Λ C B K Q.f Q.U) (hu : ∀ p ∈ ReferenceBounds.holdRegion, |P.U p - Q.U p| ≤ 1 / Λ) (huη : ∀ p ∈ ReferenceBounds.holdRegion, |ProfileHistories.parameterPartial P.U p - ProfileHistories.parameterPartial Q.U p| ≤ 1 / Λ) : (∀ p ∈ ReferenceBounds.holdRegion, |Λ * (P.U p - NaturalAxisData.U j p.2)| ≤ B + 1) ∧ ∀ p ∈ ReferenceBounds.holdRegion, |Λ * (ProfileHistories.parameterPartial P.U p - 4)| ≤ B + 1

First parameter derivatives are sufficient for all source histories.

theorem NavierStokes.ActivationContinuation.nearby_source_jets {D E : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles E) {h j σ Λ C B K : ℝ} (hΛ : 0 < Λ) (hj : ReferenceJetBounds.JetBounds h j σ Λ C B K Q.f Q.U) (hu : ∀ p ∈ ReferenceBounds.holdRegion, |P.U p - Q.U p| ≤ 1 / Λ) (huη : ∀ p ∈ ReferenceBounds.holdRegion, |ProfileHistories.parameterPartial P.U p - ProfileHistories.parameterPartial Q.U p| ≤ 1 / Λ) (hfη : ∀ p ∈ ReferenceBounds.holdRegion, |ProfileHistories.parameterPartial P.f p / P.f p - ProfileHistories.parameterPartial Q.f p / Q.f p| ≤ 1) {p : ProfileHistories.Point} (hp : p ∈ ReferenceBounds.holdRegion) (hpD : p ∈ D.carrier) : |Λ * (P.U p - NaturalAxisData.U j p.2)| ≤ B + 2 ∧ |Λ * (P.Ubar p - NaturalAxisData.U j p.2)| ≤ B + 2 ∧ |Λ * (ProfileHistories.average (ProfileHistories.parameterPartial P.U) p - 4)| ≤ B + 2 ∧ |ProfileHistories.parameterPartial P.f p / P.f p - Λ * NaturalAxisCoefficients.realGradient h j σ p.2| ≤ B + 2

noncomputable def NavierStokes.ActivationContinuation.continuationRegion (X0 : ℝ) : Set ProfileHistories.Point

A radius interval starting at the natural entrance.

Equations

• NavierStokes.ActivationContinuation.continuationRegion X0 = Set.Icc X0 110 ×ˢ Set.Icc (-1) 1

structure NavierStokes.ActivationContinuation.StockControl {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h M : ℝ) (S : Set ProfileHistories.Point) : Prop

Stock control data, collecting first_positive, first_bound, second_bound, ratio_bound.

• first_positive (p : ProfileHistories.Point) : p ∈ S → 0 < ReferenceBounds.p1 P h p
• first_bound (p : ProfileHistories.Point) : p ∈ S → ReferenceBounds.p1 P h p ≤ M
• second_bound (p : ProfileHistories.Point) : p ∈ S → |ReferenceBounds.p2 P h p| ≤ M
• ratio_bound (p : ProfileHistories.Point) : p ∈ S → |ReferenceBounds.p2 P h p / ReferenceBounds.p1 P h p| ≤ M

structure NavierStokes.ActivationContinuation.StockClose {D E : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles E) (h ε : ℝ) (p : ProfileHistories.Point) : Prop

Stock close data, collecting first, second, ratio.

• first : |ReferenceBounds.p1 P h p - ReferenceBounds.p1 Q h p| < ε
• second : |ReferenceBounds.p2 P h p - ReferenceBounds.p2 Q h p| < ε
• ratio : |Q.f p / P.f p - 1| < ε

structure NavierStokes.ActivationContinuation.ComparisonScales : Type

All constants in this record are selected before the REF cutoff.

• bound : ℝ

  Bound of ComparisonScales, of type ℝ.

• error : ℝ

  Error of ComparisonScales, of type ℝ.

• damping : ℝ

  Damping of ComparisonScales, of type ℝ.

• fieldTolerance : ℝ

  Field tolerance of ComparisonScales, of type ℝ.

• referenceRadius : ℝ

  Reference radius of ComparisonScales, of type ℝ.

• bound_pos : 0 < self.bound
• error_pos : 0 < self.error
• error_le_one : self.error ≤ 1
• damping_pos : 0 < self.damping
• damping_lt_one : self.damping < 1
• fieldTolerance_pos : 0 < self.fieldTolerance
• referenceRadius_pos : 0 < self.referenceRadius
• projection_error : self.error * projectionConstant self.bound ≤ 1 / 8
• speed_bound : self.damping * speedConstant self.bound ≤ 1
• angular_bound : self.damping * self.bound ≤ 4 / 5

theorem NavierStokes.ActivationContinuation.prepare_stock_comparison {h j σ Λ C B K : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) (hΛ : 0 < Λ) (hΛ1 : 1 ≤ Λ) (hC : 1 ≤ C) (hB : 0 ≤ B) (hK : 0 ≤ K) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hP0 : ContDiff ℝ (↑⊤) P0) : ∃ (c : ComparisonScales), ∀ (δ : ℝ) (hδ : 0 < δ), δ < c.referenceRadius → ∀ (hδT : 2 * δ < ReferencePath.rampLimit), ReferenceBounds.ReferenceBoundsOnHold E.profile hΛ hδ hδT hP0 → ReferenceJetBounds.JetBounds h j σ Λ C B K ((ReferencePath.Input.ofNatural hΛ E.profile.family).refF δ) ((ReferencePath.Input.ofNatural hΛ E.profile.family).refU δ) → have Q := ReferenceBounds.referenceProfiles E.profile hΛ hδ hδT hP0; StockControl Q h c.bound (continuationRegion (4 / Λ)) ∧ ∀ {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D), P.pressure0 = Q.pressure0 → ∀ p ∈ continuationRegion (4 / Λ), p ∈ D.carrier → (∀ t ∈ Set.Icc 0 p.1, ‖fieldJet P (t, p.2) - fieldJet Q (t, p.2)‖ < c.fieldTolerance) → StockClose P Q h c.error p

Compactness is applied to one bounded family of actual field/history jets. It does not select a cutoff first and then ask that cutoff to be smaller than its own continuity threshold.

The two terminal ramps preserve the actual relaxed inequality

theorem NavierStokes.ActivationContinuation.two_ramp_relaxed (c : ComparisonScales) {κ A B p q R b w₁ w₂ y : ℝ} (hκ : 0 < κ) (hκc : κ ≤ c.damping) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) (hA : 0 < A) (hAM : A ≤ c.bound) (hB : |B| ≤ c.bound) (hBA : |B / A| ≤ c.bound) (hp : |p - A| < c.error) (hq : |q - B| < c.error) (hR : |R - 1| < c.error) (hc : 9 / 4 ≤ A + B ^ 2 / A) (hbig : b ≤ y → 3 ≤ A) : Relaxed ((1 - TransitionRamp.step (b + w₁) w₂ y) * κ * A + 4 / 5 * TransitionRamp.step (b + w₁) w₂ y) (κ * (1 - TransitionRamp.step b w₁ y) * B * R) p q

Binding the constructed physical ramp to the cone coordinates

theorem NavierStokes.ActivationContinuation.physical_shear_equations {h j σ Λ C δ T κ w₁ w₂ : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (hT : 0 < T) (hb : δ ≤ (TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {p : ProfileHistories.Point} (hp : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 < p.1) (ht : T ≤ (TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0).logTime p.1) : have R := TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0; have P := TransitionRamp.physicalProfiles F hΛ hsmall hδ hδT hP0 hT hb hw₁ hw₂; shearA P p = (1 - TransitionRamp.step (R.bigTime + w₁) w₂ (R.logTime p.1)) * κ * ReferenceBounds.p1 R.profiles h p + 4 / 5 * TransitionRamp.step (R.bigTime + w₁) w₂ (R.logTime p.1) ∧ shearB P p = κ * (1 - TransitionRamp.step R.bigTime w₁ (R.logTime p.1)) * ReferenceBounds.p2 R.profiles h p * (R.profiles.f p / P.f p)

theorem NavierStokes.ActivationContinuation.physical_fieldJet_before {h j σ Λ C δ T κ w₁ w₂ : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (hT : 0 < T) (hb : δ ≤ (TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {p : ProfileHistories.Point} (hp : p ∈ (ReferencePath.Input.ofNatural hΛ F).radialDomain.carrier) (hx : p.1 ≤ (ReferencePath.Input.ofNatural hΛ F).endpoint) : have R := TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0; have P := TransitionRamp.physicalProfiles F hΛ hsmall hδ hδT hP0 hT hb hw₁ hw₂; fieldJet P p = fieldJet R.profiles p

The whole incoming field jet is exactly preserved, including the join at the natural endpoint.

theorem NavierStokes.ActivationContinuation.physical_endpoint_control {h j σ Λ C δ T κ w₁ w₂ : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (hT : 0 < T) (hb : δ ≤ (TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {ε : ℝ} (hc : (TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0).SmallPhysicalControl (Set.Icc (-1) 1) 1 ε T κ w₁ w₂) {p : ProfileHistories.Point} (hp : p ∈ continuationRegion (4 / Λ)) : have N := ReferencePath.Input.ofNatural hΛ F; have P := TransitionRamp.physicalProfiles F hΛ hsmall hδ hδT hP0 hT hb hw₁ hw₂; |P.U p - N.U (N.endpoint, p.2)| < ε ∧ |ProfileHistories.parameterPartial P.U p - ProfileHistories.parameterPartial N.U (N.endpoint, p.2)| < ε ∧ |ProfileHistories.parameterPartial P.f p / P.f p - ProfileHistories.parameterPartial N.f (N.endpoint, p.2) / N.f (N.endpoint, p.2)| < ε

Rewrite the endpoint in the physical error estimates as the original natural endpoint, whose bounds were fixed before the reference cutoff.

theorem NavierStokes.ActivationContinuation.physical_endpoint_log_value {h j σ Λ C δ T κ w₁ w₂ : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (hT : 0 < T) (hb : δ ≤ (TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {ε : ℝ} (hc : (TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0).SmallPhysicalControl (Set.Icc (-1) 1) 1 ε T κ w₁ w₂) {p : ProfileHistories.Point} (hη : p.2 ∈ Set.Icc (-1) 1) (hx : p.1 ∈ Set.Icc (4 / Λ) (StressActivation.radius (4 / Λ) ((TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0).bigTime + w₁ + w₂))) : have N := ReferencePath.Input.ofNatural hΛ F; have P := TransitionRamp.physicalProfiles F hΛ hsmall hδ hδT hP0 hT hb hw₁ hw₂; |Real.log (P.f p) - Real.log (N.f (N.endpoint, p.2))| < ε

Uniform logarithmic-to-physical jet conversion

theorem NavierStokes.ActivationContinuation.angular_endpoint_transfer (N : ReferencePath.Input) {ε : ℝ} (hε : 0 < ε) : ∃ τ > 0, ∀ {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point), p.2 ∈ Set.Icc (-1) 1 → 0 < P.f p → |Real.log (P.f p) - Real.log (N.f (N.endpoint, p.2))| < τ → |ProfileHistories.parameterPartial P.f p / P.f p - ProfileHistories.parameterPartial N.f (N.endpoint, p.2) / N.f (N.endpoint, p.2)| < τ → |P.f p - N.f (N.endpoint, p.2)| < ε ∧ |ProfileHistories.parameterPartial P.f p - ProfileHistories.parameterPartial N.f (N.endpoint, p.2)| < ε

theorem NavierStokes.ActivationContinuation.fieldJet_close {D E : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles E) {p : ProfileHistories.Point} {ε : ℝ} (hε : 0 < ε) (hf : |P.f p - Q.f p| < ε) (hu : |P.U p - Q.U p| < ε) (hfη : |ProfileHistories.parameterPartial P.f p - ProfileHistories.parameterPartial Q.f p| < ε) (huη : |ProfileHistories.parameterPartial P.U p - ProfileHistories.parameterPartial Q.U p| < ε) : ‖fieldJet P p - fieldJet Q p‖ < ε

theorem NavierStokes.ActivationContinuation.abs_sub_of_common_center {x y z a b : ℝ} (hx : |x - z| < a) (hy : |y - z| < b) : |x - y| < a + b

theorem NavierStokes.ActivationContinuation.physical_control_mono {J K : Set ℝ} (R : TransitionRamp.StockReference J) {N n : ℕ} {ε ε' T κ w₁ w₂ : ℝ} (hn : n ≤ N) (he : ε ≤ ε') (hc : R.SmallPhysicalControl K N ε T κ w₁ w₂) : R.SmallPhysicalControl K n ε' T κ w₁ w₂

Parameters and actual profiles of one common continuation

structure NavierStokes.ActivationContinuation.RampParameters {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hP0 : ContDiff ℝ (↑⊤) P0) : Type

Ramp parameters data, collecting refTime, actTime, kappa, widthU, widthA, refTime_pos and their compatibility conditions.

• refTime : ℝ

  Ref time of RampParameters, of type ℝ.

• actTime : ℝ

  Act time of RampParameters, of type ℝ.

• kappa : ℝ

  Kappa of RampParameters, of type ℝ.

• widthU : ℝ

  Width U of RampParameters, of type ℝ.

• widthA : ℝ

  Width A of RampParameters, of type ℝ.

• refTime_pos : 0 < self.refTime
• refTime_bound : 2 * self.refTime < ReferencePath.rampLimit
• actTime_pos : 0 < self.actTime
• actTime_le : self.actTime ≤ self.refTime
• kappa_pos : 0 < self.kappa
• kappa_lt_one : self.kappa < 1
• widthU_pos : 0 < self.widthU
• widthA_pos : 0 < self.widthA
• before_big : self.refTime ≤ (TransitionRamp.ofNatural F hΛ hsmall ⋯ ⋯ hP0).bigTime
• finish_before : (TransitionRamp.ofNatural F hΛ hsmall ⋯ ⋯ hP0).bigTime + self.widthU + self.widthA < (TransitionRamp.ofNatural F hΛ hsmall ⋯ ⋯ hP0).finalTime

noncomputable def NavierStokes.ActivationContinuation.RampParameters.reference {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : TransitionRamp.StockReference ReferencePath.parameterInterval

Reference, given by TransitionRamp.ofNatural F hΛ hsmall r.refTime_pos r.refTime_bound hP0.

Equations

• r.reference = NavierStokes.TransitionRamp.ofNatural F hΛ hsmall ⋯ ⋯ hP0

noncomputable def NavierStokes.ActivationContinuation.RampParameters.profiles {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : ProfileHistories.Profiles (ReferencePath.Input.ofNatural hΛ F).radialDomain

Profiles, constructed using TransitionRamp.physicalProfiles.

Equations

• r.profiles = NavierStokes.TransitionRamp.physicalProfiles F hΛ hsmall ⋯ ⋯ hP0 ⋯ ⋯ ⋯ ⋯

noncomputable def NavierStokes.ActivationContinuation.RampParameters.startRadius {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : ℝ

Start radius, given by radius r.reference.radius0 r.actTime.

Equations

• r.startRadius = NavierStokes.StressActivation.radius r.reference.radius0 r.actTime

noncomputable def NavierStokes.ActivationContinuation.RampParameters.holdTime {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : ℝ

Hold time, given by r.reference.bigTime + r.widthU + r.widthA.

Equations

• r.holdTime = r.reference.bigTime + r.widthU + r.widthA

noncomputable def NavierStokes.ActivationContinuation.RampParameters.holdRadius {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : ℝ

Hold radius, given by radius r.reference.radius0 r.holdTime.

Equations

• r.holdRadius = NavierStokes.StressActivation.radius r.reference.radius0 r.holdTime

theorem NavierStokes.ActivationContinuation.RampParameters.radius0_eq {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : r.reference.radius0 = 4 / Λ

theorem NavierStokes.ActivationContinuation.RampParameters.profiles_positive {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) {p : ProfileHistories.Point} (hp : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 ≤ p.1) : 0 < r.profiles.f p

theorem NavierStokes.ActivationContinuation.RampParameters.profiles_mem {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) {p : ProfileHistories.Point} (hp : p.2 ∈ Set.Icc (-1) 1) (hX : 0 ≤ p.1) : p ∈ r.reference.domain.carrier

theorem NavierStokes.ActivationContinuation.RampParameters.bigTime_pos {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : 0 < r.reference.bigTime

theorem NavierStokes.ActivationContinuation.RampParameters.holdTime_pos {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : 0 < r.holdTime

theorem NavierStokes.ActivationContinuation.RampParameters.startRadius_pos {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : 0 < r.startRadius

theorem NavierStokes.ActivationContinuation.RampParameters.holdRadius_pos {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : 0 < r.holdRadius

theorem NavierStokes.ActivationContinuation.RampParameters.radius0_lt_start {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : r.reference.radius0 < r.startRadius

theorem NavierStokes.ActivationContinuation.RampParameters.hundred_lt_hold {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : 100 < r.holdRadius

theorem NavierStokes.ActivationContinuation.RampParameters.hold_lt_final {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : r.holdRadius < 110

theorem NavierStokes.ActivationContinuation.RampParameters.start_le_hold {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : r.startRadius ≤ r.holdRadius

theorem NavierStokes.ActivationContinuation.RampParameters.logTime_start {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) {X : ℝ} (hx : r.startRadius ≤ X) : r.actTime ≤ r.reference.logTime X

theorem NavierStokes.ActivationContinuation.RampParameters.logTime_hold {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) {X : ℝ} (hx : r.holdRadius ≤ X) : r.holdTime ≤ r.reference.logTime X

theorem NavierStokes.ActivationContinuation.RampParameters.physical_shears {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) {p : ProfileHistories.Point} (hη : p.2 ∈ Set.Icc (-1) 1) (hx : r.startRadius ≤ p.1) : shearA r.profiles p = (1 - TransitionRamp.step (r.reference.bigTime + r.widthU) r.widthA (r.reference.logTime p.1)) * r.kappa * ReferenceBounds.p1 r.reference.profiles h p + 4 / 5 * TransitionRamp.step (r.reference.bigTime + r.widthU) r.widthA (r.reference.logTime p.1) ∧ shearB r.profiles p = r.kappa * (1 - TransitionRamp.step r.reference.bigTime r.widthU (r.reference.logTime p.1)) * ReferenceBounds.p2 r.reference.profiles h p * (r.reference.profiles.f p / r.profiles.f p)

theorem NavierStokes.ActivationContinuation.RampParameters.final_shears {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) {p : ProfileHistories.Point} (hη : p.2 ∈ Set.Icc (-1) 1) (hx : r.holdRadius ≤ p.1) : shearA r.profiles p = 4 / 5 ∧ shearB r.profiles p = 0

theorem NavierStokes.ActivationContinuation.RampParameters.final_logSlope {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) {p : ProfileHistories.Point} (hη : p.2 ∈ Set.Icc (-1) 1) (hx : r.holdRadius ≤ p.1) : ReferenceBounds.logSlope r.profiles p = 3 / 5

noncomputable def NavierStokes.ActivationContinuation.InitialActivationBound {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : Prop

The initial collar estimate is retained for the very same chosen activation width and damping, not for a separately chosen profile.

Equations

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

structure NavierStokes.ActivationContinuation.ComparableRamp {h j σ Λ C B K : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters E.profile.family hΛ hsmall hP0) (c : ComparisonScales) : Prop

Quantitative facts established for one actual constructed ramp. The existence theorem below supplies every field, including the stock errors.

• reference_bounds : ReferenceBounds.ReferenceBoundsOnHold E.profile hΛ ⋯ ⋯ hP0
• reference_jets : ReferenceJetBounds.JetBounds h j σ Λ C B K r.reference.profiles.f r.reference.profiles.U
• damping_le : r.kappa ≤ c.damping
• stock_bounds : StockControl r.reference.profiles h c.bound (continuationRegion (4 / Λ))
• stock_close (p : ProfileHistories.Point) : p ∈ continuationRegion (4 / Λ) → p.1 ≤ r.holdRadius → StockClose r.profiles r.reference.profiles h c.error p
• source_jets (p : ProfileHistories.Point) : p ∈ ReferenceBounds.holdRegion → |Λ * (r.profiles.U p - NaturalAxisData.U j p.2)| ≤ B + 2 ∧ |Λ * (r.profiles.Ubar p - NaturalAxisData.U j p.2)| ≤ B + 2 ∧ |Λ * (ProfileHistories.average (ProfileHistories.parameterPartial r.profiles.U) p - 4)| ≤ B + 2 ∧ |ProfileHistories.parameterPartial r.profiles.f p / r.profiles.f p - Λ * NaturalAxisCoefficients.realGradient h j σ p.2| ≤ B + 2

theorem NavierStokes.ActivationContinuation.log_control_mono {J K : Set ℝ} (R : TransitionRamp.StockReference J) {N n : ℕ} {ε ε' T κ w₁ w₂ : ℝ} (hn : n ≤ N) (he : ε ≤ ε') (hc : R.SmallLogControl K N ε T κ w₁ w₂) : R.SmallLogControl K n ε' T κ w₁ w₂

theorem NavierStokes.ActivationContinuation.exists_comparable_ramp {h j σ Λ C B K r0 : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) (hΛ : 0 < Λ) (hΛ1 : 1 ≤ Λ) (hC : 1 ≤ C) (hB : 0 ≤ B) (hK : 0 ≤ K) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hP0 : ContDiff ℝ (↑⊤) P0) (hr0 : 0 < r0) (href : ∀ (δ : ℝ) (hδ : 0 < δ), δ < r0 → ∃ (hδT : 2 * δ < ReferencePath.rampLimit), ReferenceBounds.ReferenceBoundsOnHold E.profile hΛ hδ hδT hP0 ∧ ReferenceJetBounds.JetBounds h j σ Λ C B K ((ReferencePath.Input.ofNatural hΛ E.profile.family).refF δ) ((ReferencePath.Input.ofNatural hΛ E.profile.family).refU δ)) (Nextra : ℕ) {εextra : ℝ} (hεextra : 0 < εextra) : ∃ (r : RampParameters E.profile.family hΛ hsmall hP0) (c : ComparisonScales), ComparableRamp E r c ∧ InitialActivationBound r ∧ r.reference.SmallPhysicalControl (Set.Icc (-1) 1) Nextra εextra r.actTime r.kappa r.widthU r.widthA ∧ r.reference.SmallLogControl (Set.Icc (-1) 1) Nextra εextra r.actTime r.kappa r.widthU r.widthA

Construct one shared cutoff, activation and two-ramp schedule. The extra finite-jet tolerance is intersected with the cone tolerances, so later matching does not need to replace this witness.

Cone comparison followed by the actual lag barrier

theorem NavierStokes.ActivationContinuation.comparable_relaxed_before_hold {h j σ Λ C B K : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (hσ : 0 < σ) (r : RampParameters E.profile.family hΛ hsmall hP0) (c : ComparisonScales) (hc : ComparableRamp E r c) {p : ProfileHistories.Point} (hp : p ∈ continuationRegion (4 / Λ)) (hstart : r.startRadius ≤ p.1) (hend : p.1 ≤ r.holdRadius) : IsRelaxed r.profiles h p

noncomputable def NavierStokes.ActivationContinuation.HoldSourceControl (h j σ Λ B : ℝ) : Prop

A reusable statement of the source estimate already proved by compact absorption before the scale is chosen.

Equations

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

theorem NavierStokes.ActivationContinuation.comparable_final_first {h j σ Λ C B K X η : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (hσ : 0 < σ) (r : RampParameters E.profile.family hΛ hsmall hP0) (c : ComparisonScales) (hc : ComparableRamp E r c) (hsource : HoldSourceControl h j σ Λ (B + 2)) (hη : η ∈ Set.Icc (-1) 1) (hX : X ∈ Set.Icc r.holdRadius 110) : 2 < ReferenceBounds.p1 r.profiles h (X, η)

theorem NavierStokes.ActivationContinuation.comparable_relaxed {h j σ Λ C B K : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (hσ : 0 < σ) (r : RampParameters E.profile.family hΛ hsmall hP0) (c : ComparisonScales) (hc : ComparableRamp E r c) (hsource : HoldSourceControl h j σ Λ (B + 2)) {p : ProfileHistories.Point} (hη : p.2 ∈ Set.Icc (-1) 1) (hX : p.1 ∈ Set.Icc r.startRadius 110) : IsRelaxed r.profiles h p

The complete ordered existence statement

structure NavierStokes.ActivationContinuation.ContinuationWitness {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hP0 : ContDiff ℝ (↑⊤) P0) (N : ℕ) (ε : ℝ) : Type

Continuation witness data, collecting parameters, initial_activation, relaxed, final_first, final_source, physical_control and their compatibility conditions.

• parameters : RampParameters E.profile.family hΛ hsmall hP0

  Parameters of ContinuationWitness, of type RampParameters E.profile.family hΛ hsmall hP0.

• initial_activation : InitialActivationBound self.parameters
• relaxed (p : ProfileHistories.Point) : p.2 ∈ Set.Icc (-1) 1 → p.1 ∈ Set.Icc self.parameters.startRadius 110 → IsRelaxed self.parameters.profiles h p
• final_first (X : ℝ) : X ∈ Set.Icc self.parameters.holdRadius 110 → ∀ η ∈ Set.Icc (-1) 1, 2 < ReferenceBounds.p1 self.parameters.profiles h (X, η)
• final_source (X : ℝ) : X ∈ Set.Icc self.parameters.holdRadius 110 → ∀ η ∈ Set.Icc (-1) 1, 5 / 4 < ReferenceBounds.sourceQ self.parameters.profiles h (X, η)
• physical_control : self.parameters.reference.SmallPhysicalControl (Set.Icc (-1) 1) N ε self.parameters.actTime self.parameters.kappa self.parameters.widthU self.parameters.widthA
• logarithmic_control : self.parameters.reference.SmallLogControl (Set.Icc (-1) 1) N ε self.parameters.actTime self.parameters.kappa self.parameters.widthU self.parameters.widthA

theorem NavierStokes.ActivationContinuation.exists_activation_continuation {h j σ ν : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hP0 : ContDiff ℝ (↑⊤) P0) (hν : 0 < ν) (hcut : ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisData.Z h j P0 η| ≤ ν → 99 / 100 < NaturalAxisData.chi h j σ η) : ∃ (M : ℝ), 1 ≤ M ∧ ∀ (Λ : ℝ) (hΛ : 0 < Λ), M ≤ Λ → ∃ (C0 : ℝ), 1 ≤ C0 ∧ ∀ (C : ℝ), C0 ≤ C → ∃ (E : NaturalEntrance.EntranceProfile d Λ C), ∀ (N : ℕ) (ε : ℝ), 0 < ε → Nonempty (ContinuationWitness E hΛ hsmall hP0 N ε)

The actual relaxed continuation through X = 110, with the order Λ, then C, then the small cutoff/activation/ramp parameters. No source, stock closeness or cone inequality is an input to this theorem.

Exact data passed to the shape transition

noncomputable def NavierStokes.ActivationContinuation.RampParameters.endpointAxial {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : ℝ → ℝ

Endpoint axial, given by r.reference.endpointU r.actTime r.kappa r.widthU.

Equations

• r.endpointAxial = r.reference.endpointU r.actTime r.kappa r.widthU

noncomputable def NavierStokes.ActivationContinuation.RampParameters.endpointLogarithm {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : ℝ → ℝ

Endpoint logarithm, given by r.reference.endpointLog r.actTime r.kappa r.widthU r.widthA C.

Equations

• r.endpointLogarithm = r.reference.endpointLog r.actTime r.kappa r.widthU r.widthA C

theorem NavierStokes.ActivationContinuation.RampParameters.endpointAxial_smooth {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : ContDiffOn ℝ (↑⊤) r.endpointAxial ReferencePath.parameterInterval

theorem NavierStokes.ActivationContinuation.RampParameters.endpointLogarithm_smooth {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) : ContDiffOn ℝ (↑⊤) r.endpointLogarithm ReferencePath.parameterInterval

theorem NavierStokes.ActivationContinuation.RampParameters.initial_fields {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : p.1 ≤ (ReferencePath.Input.ofNatural hΛ F).endpoint * Real.exp r.refTime) : r.profiles.f p = StressActivation.FromReference.f (ReferencePath.Input.ofNatural hΛ F) r.actTime r.kappa r.refTime p ∧ r.profiles.U p = StressActivation.FromReference.U (ReferencePath.Input.ofNatural hΛ F) r.actTime r.kappa r.refTime p

theorem NavierStokes.ActivationContinuation.RampParameters.terminal_fields {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) (hC : 0 < C) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 110 ≤ p.1) : r.profiles.f p = C⁻¹ * Real.exp (Real.log (p.1 / 110) / 10 + r.endpointLogarithm p.2) / √(2 * p.1) ∧ r.profiles.U p = r.endpointAxial p.2

theorem NavierStokes.ActivationContinuation.RampParameters.endpointLogarithm_eq_actual {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} {F : NaturalProfile.ProfileFamily d Λ C} {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : RampParameters F hΛ hsmall hP0) (hC : 0 < C) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : r.endpointLogarithm η = Real.log (C * r.profiles.E (110, η))