Ordered jet bounds for the actual reference path

Coefficient-space norm bounds first give constants independent of the normalization C. Only afterwards is the short REF transition chosen.

@[instance_reducible]

noncomputable def NavierStokes.ReferenceJetBounds.instReferenceJetBounds1 (ε : ℝ) : NormedAddCommGroup (NaturalEntrance.CoefficientPair ε)

Cache the standard NormedAddCommGroup (NaturalEntrance.CoefficientPair ε) instance to shorten typeclass synthesis.

Equations

• NavierStokes.ReferenceJetBounds.instReferenceJetBounds1 ε = inferInstance

theorem NavierStokes.ReferenceJetBounds.parameter_deriv {F : ProfileHistories.Field} {p : ProfileHistories.Point} (hF : ContDiffAt ℝ (↑⊤) F p) : HasDerivAt (fun (η : ℝ) => F (p.1, η)) (ProfileHistories.parameterPartial F p) p.2

theorem NavierStokes.ReferenceJetBounds.radial_deriv {F : ProfileHistories.Field} {p : ProfileHistories.Point} (hF : ContDiffAt ℝ (↑⊤) F p) : HasDerivAt (fun (X : ℝ) => F (X, p.2)) (ProfileHistories.radialPartial F p) p.1

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

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

noncomputable def NavierStokes.ReferenceJetBounds.jetConstant {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (k m : ℕ) : ℝ

Jet constant, given by AxisEvaluation.jetBound v.epsilon 5 k m * (‖referencePair v‖ + 1).

Equations

• NavierStokes.ReferenceJetBounds.jetConstant v k m = NavierStokes.AxisEvaluation.jetBound v.epsilon 5 k m * (‖NavierStokes.NaturalEntrance.referencePair v‖ + 1)

theorem NavierStokes.ReferenceJetBounds.jetConstant_nonneg {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (k m : ℕ) : 0 ≤ jetConstant v k m

theorem NavierStokes.ReferenceJetBounds.norm_pair_le {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (x : NaturalEntrance.CoefficientPair v.epsilon) (hx : ‖x - NaturalEntrance.referencePair v‖ ≤ 1) : ‖x‖ ≤ ‖NaturalEntrance.referencePair v‖ + 1

theorem NavierStokes.ReferenceJetBounds.coefficient_jet_bound {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (x : NaturalEntrance.CoefficientPair v.epsilon) (hx : ‖x - NaturalEntrance.referencePair v‖ ≤ 1) (k m : ℕ) {p : ProfileHistories.Point} (hp : |p.1| ≤ 5) : |AxisEvaluation.mixedSeries NaturalAxisCoefficients.window v.epsilon x.1 k m p| ≤ jetConstant v k m ∧ |AxisEvaluation.mixedSeries NaturalAxisCoefficients.window v.epsilon x.2 k m p| ≤ jetConstant v k m

theorem NavierStokes.ReferenceJetBounds.natural_U_value {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : Λ ≠ 0) (p : ProfileHistories.Point) : Λ * (F.family.U p - NaturalAxisData.U j p.2) = AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon F.coefficients.2 (NaturalProfile.rescalePoint Λ p)

theorem NavierStokes.ReferenceJetBounds.natural_U_parameter {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : Λ ≠ 0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : Λ * (ProfileHistories.parameterPartial F.family.U p - 4) = NaturalAxisBridge.partialEta (AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon F.coefficients.2) (NaturalProfile.rescalePoint Λ p)

theorem NavierStokes.ReferenceJetBounds.natural_U_radial {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : Λ ≠ 0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : Λ * p.1 * ProfileHistories.radialPartial F.family.U p = (NaturalProfile.rescalePoint Λ p).1 * NaturalAxisBridge.partialY (AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon F.coefficients.2) (NaturalProfile.rescalePoint Λ p)

theorem NavierStokes.ReferenceJetBounds.natural_log_parameter {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) : 0 < Λ → ∀ (hC : 0 < C) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) (hφ : AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon F.coefficients.1 (NaturalProfile.rescalePoint Λ p) ≠ 0), ProfileHistories.parameterPartial F.family.f p / F.family.f p - Λ * NaturalAxisCoefficients.realGradient h j σ p.2 = NaturalAxisBridge.partialEta (AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon F.coefficients.1) (NaturalProfile.rescalePoint Λ p) / AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon F.coefficients.1 (NaturalProfile.rescalePoint Λ p)

theorem NavierStokes.ReferenceJetBounds.natural_log_radial {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hC : 0 < C) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) (hφ : AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon F.coefficients.1 (NaturalProfile.rescalePoint Λ p) ≠ 0) : p.1 * ProfileHistories.radialPartial F.family.f p / F.family.f p = (NaturalProfile.rescalePoint Λ p).1 * NaturalAxisBridge.partialY (AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon F.coefficients.1) (NaturalProfile.rescalePoint Λ p) / AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon F.coefficients.1 (NaturalProfile.rescalePoint Λ p)

theorem NavierStokes.ReferenceJetBounds.natural_U_bounds {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {p : ProfileHistories.Point} (hp : NaturalProfile.rescalePoint Λ p ∈ NaturalEntrance.entranceSet) : |Λ * (F.family.U p - NaturalAxisData.U j p.2)| ≤ jetConstant d.coefficients 0 0 ∧ |Λ * (ProfileHistories.parameterPartial F.family.U p - 4)| ≤ jetConstant d.coefficients 0 1 ∧ |Λ * p.1 * ProfileHistories.radialPartial F.family.U p| ≤ 5 * jetConstant d.coefficients 1 0

theorem NavierStokes.ReferenceJetBounds.natural_log_bound {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hσ : 0 < σ) (hΛ : 0 < Λ) (hC : 0 < C) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) {p : ProfileHistories.Point} (hp : NaturalProfile.rescalePoint Λ p ∈ NaturalEntrance.entranceSet) : |ProfileHistories.parameterPartial F.family.f p / F.family.f p - Λ * NaturalAxisCoefficients.realGradient h j σ p.2| ≤ 8 * jetConstant d.coefficients 0 1

noncomputable def NavierStokes.ReferenceJetBounds.amplitudeConstant {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (Λ G : ℝ) : ℝ

Amplitude constant, given by d.normalizationThreshold Λ * jetConstant d.coefficients 0 0 * (1 + Λ * G + 8 * jetConstant d.coefficients 0 1).

Equations

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

theorem NavierStokes.ReferenceJetBounds.amplitudeConstant_nonneg {h j σ Λ : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 ≤ Λ) {G : ℝ} (hG : 0 ≤ G) : 0 ≤ amplitudeConstant d Λ G

theorem NavierStokes.ReferenceJetBounds.natural_amplitude_bounds {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hσ : 0 < σ) (hΛ : 0 < Λ) (hC : 0 < C) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) {G : ℝ} (hG : 0 ≤ G) {p : ProfileHistories.Point} (hp : NaturalProfile.rescalePoint Λ p ∈ NaturalEntrance.entranceSet) (hgrad : |NaturalAxisCoefficients.realGradient h j σ p.2| ≤ G) : |F.family.f p| ≤ amplitudeConstant d Λ G / C ∧ |ProfileHistories.parameterPartial F.family.f p| ≤ amplitudeConstant d Λ G / C

def NavierStokes.ReferenceJetBounds.holdSet : Set ProfileHistories.Point

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

Equations

• NavierStokes.ReferenceJetBounds.holdSet = Set.Icc 0 110 ×ˢ Set.Icc (-1) 1

theorem NavierStokes.ReferenceJetBounds.reference_mem (N : ReferencePath.Input) {p : ProfileHistories.Point} (hX : 0 ≤ p.1) (hη : p.2 ∈ Set.Icc (-1) 1) : p ∈ N.radialDomain.carrier

theorem NavierStokes.ReferenceJetBounds.endpoint_mem (N : ReferencePath.Input) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : (N.endpoint, η) ∈ NaturalProfile.domain N.scale

theorem NavierStokes.ReferenceJetBounds.first_parameter_difference {F G : ProfileHistories.Field} {x y η : ℝ} (hF : ContDiffAt ℝ (↑⊤) F (x, η)) (hG : ContDiffAt ℝ (↑⊤) G (y, η)) : iteratedDeriv 1 (fun (z : ℝ) => F (x, z) - G (y, z)) η = ProfileHistories.parameterPartial F (x, η) - ProfileHistories.parameterPartial G (y, η)

theorem NavierStokes.ReferenceJetBounds.first_log_difference {F G : ProfileHistories.Field} {x y η : ℝ} (hF : ContDiffAt ℝ (↑⊤) F (x, η)) (hG : ContDiffAt ℝ (↑⊤) G (y, η)) (hFn : F (x, η) ≠ 0) (hGn : G (y, η) ≠ 0) : iteratedDeriv 1 (fun (z : ℝ) => Real.log (F (x, z)) - Real.log (G (y, z))) η = ProfileHistories.parameterPartial F (x, η) / F (x, η) - ProfileHistories.parameterPartial G (y, η) / G (y, η)

structure NavierStokes.ReferenceJetBounds.TransitionControl (N : ReferencePath.Input) (δ εU εF : ℝ) : Prop

Transition control data, collecting length_pos, length_bound, U_value, U_parameter, log_parameter, f_value and their compatibility conditions.

• length_pos : 0 < δ
• length_bound : 2 * δ < ReferencePath.rampLimit
• U_value (p : ProfileHistories.Point) : N.endpoint ≤ p.1 → p.2 ∈ Set.Icc (-1) 1 → |N.refU δ p - N.U (N.endpoint, p.2)| < εU
• U_parameter (p : ProfileHistories.Point) : N.endpoint ≤ p.1 → p.2 ∈ Set.Icc (-1) 1 → |ProfileHistories.parameterPartial (N.refU δ) p - ProfileHistories.parameterPartial N.U (N.endpoint, p.2)| < εU
• log_parameter (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)| < 1
• f_value (p : ProfileHistories.Point) : N.endpoint ≤ p.1 → p.2 ∈ Set.Icc (-1) 1 → |N.refF δ p - N.f (N.endpoint, p.2)| < εF
• f_parameter (p : ProfileHistories.Point) : N.endpoint ≤ p.1 → p.2 ∈ Set.Icc (-1) 1 → |ProfileHistories.parameterPartial (N.refF δ) p - ProfileHistories.parameterPartial N.f (N.endpoint, p.2)| < εF

theorem NavierStokes.ReferenceJetBounds.exists_transition_control (N : ReferencePath.Input) {εU εF : ℝ} (hεU : 0 < εU) (hεF : 0 < εF) : ∃ r > 0, ∀ (δ : ℝ), 0 < δ → δ < r → TransitionControl N δ εU εF

One actual cutoff length works for all required low-order reference jets. The tolerances may be chosen only after the fixed input profile is known.

theorem NavierStokes.ReferenceJetBounds.reference_initial_eventually (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : ProfileHistories.Point} (hX : p.1 ≤ N.endpoint) (hη : p.2 ∈ Set.Icc (-1) 1) : N.refF δ =ᶠ[nhds p] N.f ∧ N.refU δ =ᶠ[nhds p] N.U

theorem NavierStokes.ReferenceJetBounds.reference_initial_partials (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : ProfileHistories.Point} (hX : p.1 ≤ N.endpoint) (hη : p.2 ∈ Set.Icc (-1) 1) : ProfileHistories.parameterPartial (N.refF δ) p = ProfileHistories.parameterPartial N.f p ∧ ProfileHistories.parameterPartial (N.refU δ) p = ProfileHistories.parameterPartial N.U p ∧ ProfileHistories.radialPartial (N.refU δ) p = ProfileHistories.radialPartial N.U p

theorem NavierStokes.ReferenceJetBounds.initial_entrance {Λ : ℝ} (hΛ : 0 < Λ) {p : ProfileHistories.Point} (hX : 0 ≤ p.1) (hupper : p.1 ≤ 4 / Λ) (hη : p.2 ∈ Set.Icc (-1) 1) : NaturalProfile.rescalePoint Λ p ∈ NaturalEntrance.entranceSet

theorem NavierStokes.ReferenceJetBounds.logtime_entrance (N : ReferencePath.Input) {p : ProfileHistories.Point} (hX : 0 < p.1) (hη : p.2 ∈ Set.Icc (-1) 1) (ht : N.logTime p.1 < ReferencePath.rampLimit) : NaturalProfile.rescalePoint N.scale p ∈ NaturalEntrance.entranceSet

noncomputable def NavierStokes.ReferenceJetBounds.uniformBound {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) : ℝ

Uniform bound, given by 2 + jetConstant v 0 0 + 9 * jetConstant v 0 1 + 5 * jetConstant v 1 0.

Equations

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

theorem NavierStokes.ReferenceJetBounds.uniformBound_controls {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) : 1 < uniformBound v ∧ 1 + jetConstant v 0 0 ≤ uniformBound v ∧ 1 + jetConstant v 0 1 ≤ uniformBound v ∧ 5 * jetConstant v 1 0 ≤ uniformBound v ∧ 1 + 8 * jetConstant v 0 1 ≤ uniformBound v

structure NavierStokes.ReferenceJetBounds.JetBounds (h j σ Λ C B K : ℝ) (f U : ProfileHistories.Field) : Prop

Jet bounds data, collecting axial_value, axial_parameter, axial_radial, log_parameter, angular_value, angular_parameter.

• axial_value (p : ProfileHistories.Point) : p ∈ holdSet → |Λ * (U p - NaturalAxisData.U j p.2)| ≤ B
• axial_parameter (p : ProfileHistories.Point) : p ∈ holdSet → |Λ * (ProfileHistories.parameterPartial U p - 4)| ≤ B
• axial_radial (p : ProfileHistories.Point) : p ∈ holdSet → |Λ * p.1 * ProfileHistories.radialPartial U p| ≤ B
• log_parameter (p : ProfileHistories.Point) : p ∈ holdSet → |ProfileHistories.parameterPartial f p / f p - Λ * NaturalAxisCoefficients.realGradient h j σ p.2| ≤ B
• angular_value (p : ProfileHistories.Point) : p ∈ holdSet → |f p| ≤ K / C
• angular_parameter (p : ProfileHistories.Point) : p ∈ holdSet → |ProfileHistories.parameterPartial f p| ≤ K / C

@[reducible, inline]

noncomputable abbrev NavierStokes.ReferenceJetBounds.referenceInput {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) : ReferencePath.Input

Reference input: an abbreviation for ReferencePath.Input.ofNatural hΛ F.family.

Equations

• NavierStokes.ReferenceJetBounds.referenceInput F hΛ = NavierStokes.ReferencePath.Input.ofNatural hΛ F.family

theorem NavierStokes.ReferenceJetBounds.reference_U_radial_bound {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : ProfileHistories.Point} (hp : p ∈ holdSet) : |Λ * p.1 * ProfileHistories.radialPartial ((referenceInput F hΛ).refU δ) p| ≤ 5 * jetConstant d.coefficients 1 0

theorem NavierStokes.ReferenceJetBounds.scaled_transfer {Λ : ℝ} (hpos : 0 < Λ) {a b c s : ℝ} (hclose : |a - b| ≤ 1 / Λ) (hbase : |Λ * (b - c)| ≤ s) : |Λ * (a - c)| ≤ 1 + s

theorem NavierStokes.ReferenceJetBounds.transfer_difference {a b c r s : ℝ} (hclose : |a - b| ≤ r) (hbase : |b - c| ≤ s) : |a - c| ≤ r + s

theorem NavierStokes.ReferenceJetBounds.transfer_absolute {a b r s : ℝ} (hclose : |a - b| ≤ r) (hbase : |b| ≤ s) : |a| ≤ r + s

theorem NavierStokes.ReferenceJetBounds.bounds_of_control {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hσ : 0 < σ) (hC : 0 < C) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) {G : ℝ} (hG : 0 ≤ G) (hgrad : ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisCoefficients.realGradient h j σ η| ≤ G) {δ : ℝ} (hc : TransitionControl (referenceInput F hΛ) δ (1 / Λ) (1 / C)) : JetBounds h j σ Λ C (uniformBound d.coefficients) (1 + amplitudeConstant d Λ G) ((referenceInput F hΛ).refF δ) ((referenceInput F hΛ).refU δ)

The qualitative REF convergence has now been used only after Λ and C were fixed, with explicit tolerances 1/Λ, 1, and 1/C.

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

Radial error constant, given by AxisEvaluation.jetBound d.coefficients.epsilon 5 1 0 * profileErrorConstant d.

Equations

• NavierStokes.ReferenceJetBounds.radialErrorConstant d = NavierStokes.AxisEvaluation.jetBound d.coefficients.epsilon 5 1 0 * NavierStokes.NaturalProfile.profileErrorConstant d

theorem NavierStokes.ReferenceJetBounds.radialErrorConstant_nonneg {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) : 0 ≤ radialErrorConstant d

theorem NavierStokes.ReferenceJetBounds.natural_radial_jet_error {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) {p : ProfileHistories.Point} (hp : p ∈ NaturalEntrance.entranceSet) : |NaturalAxisBridge.partialY (AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon F.coefficients.1) p - NaturalEntrance.sourceJets ⋯ (NaturalEntrance.referencePair d.coefficients) p 1| ≤ radialErrorConstant d / Λ

structure NavierStokes.ReferenceJetBounds.SlopeSample {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (Λ B Kerr : ℝ) (f : ProfileHistories.Field) (p : ProfileHistories.Point) : Type

A genuine finite-dimensional source sample, with the radial jet error still controlled by the coefficient norm.

• Y : ℝ

  Y of SlopeSample, of type ℝ.

• theta : ℝ

  Theta of SlopeSample, of type ℝ.

• phi : ℝ

  Phi of SlopeSample, of type ℝ.

• error : ℝ

  Error of SlopeSample, of type ℝ.

• point_mem : (self.Y, p.2) ∈ NaturalEntrance.entranceSet
• theta_mem : self.theta ∈ Set.Icc 0 1
• phi_lower : 1 / 8 ≤ self.phi
• phi_upper : self.phi ≤ B
• error_bound : |self.error| ≤ Kerr / Λ
• slope_eq : p.1 * ProfileHistories.radialPartial f p / f p = self.theta * self.Y * (NaturalEntrance.sourceJets ⋯ (NaturalEntrance.referencePair d.coefficients) (self.Y, p.2) 1 + self.error) / self.phi

theorem NavierStokes.ReferenceJetBounds.reference_slope_sample {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hσ : 0 < σ) (hC : 0 < C) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : ProfileHistories.Point} (hX : (referenceInput F hΛ).endpoint ≤ p.1) (hη : p.2 ∈ Set.Icc (-1) 1) : Nonempty (SlopeSample d Λ (uniformBound d.coefficients) (radialErrorConstant d) ((referenceInput F hΛ).refF δ) p)

theorem NavierStokes.ReferenceJetBounds.exists_gradient_bound (h j : ℝ) {σ : ℝ} (hσ : 0 < σ) : ∃ G > 0, ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisCoefficients.realGradient h j σ η| ≤ G

theorem NavierStokes.ReferenceJetBounds.ordered_reference_bounds {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hσ : 0 < σ) : ∃ (B : ℝ) (M : ℝ) (Kerr : ℝ), 1 < B ∧ 0 < M ∧ 0 ≤ Kerr ∧ ∀ (Λ : ℝ) (hΛ : 0 < Λ), M ≤ Λ → ∃ KΛ > 0, ∀ (C : ℝ), d.normalizationThreshold Λ ≤ C → ∀ (F : NaturalEntrance.CoefficientProfile d Λ C), ∃ r > 0, ∀ (δ : ℝ), 0 < δ → δ < r → TransitionControl (referenceInput F hΛ) δ (1 / Λ) (1 / C) ∧ JetBounds h j σ Λ C B KΛ ((referenceInput F hΛ).refF δ) ((referenceInput F hΛ).refU δ) ∧ ∀ p ∈ holdSet, (referenceInput F hΛ).endpoint ≤ p.1 → Nonempty (SlopeSample d Λ B Kerr ((referenceInput F hΛ).refF δ) p)

All constants used to choose C precede C. The actual short transition is selected only after C and the actual natural coefficient profile.