The same-radius reference continuation

The reference path integrates the natural slopes evaluated at the original radius. A smooth cutoff damps those slopes to zero; no radial reparametrization is substituted for the prescribed differential equation.

def NavierStokes.ReferencePath.fullStrip (J : Set ℝ) (hJ : IsOpen J) : ProfileHistories.RadialDomain

Full strip, bundling carrier, isOpen, scale_mem.

Equations

• NavierStokes.ReferencePath.fullStrip J hJ = { carrier := Set.univ ×ˢ J, isOpen := ⋯, scale_mem := ⋯ }

def NavierStokes.ReferencePath.earlyStrip (T : ℝ) (hT : 0 < T) (J : Set ℝ) (hJ : IsOpen J) : ProfileHistories.RadialDomain

Early strip, bundling carrier, isOpen, scale_mem.

Equations

• NavierStokes.ReferencePath.earlyStrip T hT J hJ = { carrier := Set.Iio T ×ˢ J, isOpen := ⋯, scale_mem := ⋯ }

noncomputable def NavierStokes.ReferencePath.slopeCutoff (δ t : ℝ) : ℝ

One until t=δ, smooth transition on (δ,2δ), and zero from 2δ onward.

Equations

• NavierStokes.ReferencePath.slopeCutoff δ t = 1 - ((t - δ) / δ).smoothTransition

theorem NavierStokes.ReferencePath.slopeCutoff_smooth (δ : ℝ) : ContDiff ℝ (↑⊤) (slopeCutoff δ)

theorem NavierStokes.ReferencePath.slopeCutoff_mem (δ t : ℝ) : slopeCutoff δ t ∈ Set.Icc 0 1

theorem NavierStokes.ReferencePath.slopeCutoff_one {δ t : ℝ} (hδ : 0 < δ) (ht : t ≤ δ) : slopeCutoff δ t = 1

theorem NavierStokes.ReferencePath.slopeCutoff_zero {δ t : ℝ} (hδ : 0 < δ) (ht : 2 * δ ≤ t) : slopeCutoff δ t = 0

noncomputable def NavierStokes.ReferencePath.dampedSlope (δ : ℝ) (G : ProfileHistories.Field) : ProfileHistories.Field

Damped slope, defined pointwise by slopeCutoff δ p.1 * radialPartial G p.

Equations

• NavierStokes.ReferencePath.dampedSlope δ G p = NavierStokes.ReferencePath.slopeCutoff δ p.1 * NavierStokes.ProfileHistories.radialPartial G p

noncomputable def NavierStokes.ReferencePath.continuation (δ : ℝ) (G : ProfileHistories.Field) : ProfileHistories.Field

The prescribed continuation, defined by an actual integral of the same-time natural derivative.

Equations

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

theorem NavierStokes.ReferencePath.dampedSlope_smooth {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < T) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (earlyStrip T hT J hJ).carrier) : ContDiffOn ℝ (↑⊤) (dampedSlope δ G) (fullStrip J hJ).carrier

theorem NavierStokes.ReferencePath.continuation_smooth {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < T) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (earlyStrip T hT J hJ).carrier) : ContDiffOn ℝ (↑⊤) (continuation δ G) (fullStrip J hJ).carrier

theorem NavierStokes.ReferencePath.continuation_hasDerivAt {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < T) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (earlyStrip T hT J hJ).carrier) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : HasDerivAt (fun (t : ℝ) => continuation δ G (t, p.2)) (slopeCutoff δ p.1 * ProfileHistories.radialPartial G p) p.1

theorem NavierStokes.ReferencePath.continuation_eq_natural {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < T) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (earlyStrip T hT J hJ).carrier) {p : ProfileHistories.Point} (hp : p.2 ∈ J) (ht : p.1 ≤ δ) : continuation δ G p = G p

theorem NavierStokes.ReferencePath.continuation_frozen {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < T) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (earlyStrip T hT J hJ).carrier) {p : ProfileHistories.Point} (hp : p.2 ∈ J) (ht : 2 * δ ≤ p.1) : continuation δ G p = continuation δ G (2 * δ, p.2)

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

@[reducible, inline]

abbrev NavierStokes.ReferencePath.MasterPoint : Type

Master point: an abbreviation for (ℝ × ℝ) × ℝ.

Equations

• NavierStokes.ReferencePath.MasterPoint = ((ℝ × ℝ) × ℝ)

def NavierStokes.ReferencePath.masterDomain (T : ℝ) (J : Set ℝ) : Set MasterPoint

Master domain, given by {p | |p.1.1 * p.1.2| < T ∧ p.2 ∈ J}.

Equations

• NavierStokes.ReferencePath.masterDomain T J = {p : NavierStokes.ReferencePath.MasterPoint | |p.1.1 * p.1.2| < T ∧ p.2 ∈ J}

theorem NavierStokes.ReferencePath.masterDomain_open (T : ℝ) {J : Set ℝ} (hJ : IsOpen J) : IsOpen (masterDomain T J)

noncomputable def NavierStokes.ReferencePath.master (G : ProfileHistories.Field) (p : MasterPoint) : ℝ

The rescaled transition on a fixed parameter interval, smooth even at δ=0.

Equations

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

theorem NavierStokes.ReferencePath.master_at_zero (G : ProfileHistories.Field) (u η : ℝ) : master G ((0, u), η) = G (0, η)

theorem NavierStokes.ReferencePath.slopeCutoff_scaled {δ : ℝ} (hδ : δ ≠ 0) (u : ℝ) : slopeCutoff δ (δ * u) = slopeCutoff 1 u

theorem NavierStokes.ReferencePath.continuation_rescaled (G : ProfileHistories.Field) {δ : ℝ} (hδ : δ ≠ 0) (u η : ℝ) : continuation δ G (δ * u, η) = master G ((δ, u), η)

theorem NavierStokes.ReferencePath.master_smooth {T : ℝ} (hT : 0 < T) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (earlyStrip T hT J hJ).carrier) : ContDiffOn ℝ (↑⊤) (master G) (masterDomain T J)

noncomputable def NavierStokes.ReferencePath.holdTime (δ t : ℝ) : ℝ

The master representation covers the entire hold by saturating its rescaled time at two. This does not change the natural slope's evaluation point.

Equations

• NavierStokes.ReferencePath.holdTime δ t = min (t / δ) 2

theorem NavierStokes.ReferencePath.holdTime_mem {δ t : ℝ} (hδ : 0 < δ) (ht : 0 ≤ t) : holdTime δ t ∈ Set.Icc 0 2

theorem NavierStokes.ReferencePath.continuation_eq_master_hold {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < T) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (earlyStrip T hT J hJ).carrier) {t η : ℝ} (hη : η ∈ J) : 0 ≤ t → continuation δ G (t, η) = master G ((δ, holdTime δ t), η)

noncomputable def NavierStokes.ReferencePath.parameterJet (k : ℕ) (F : MasterPoint → ℝ) (p : MasterPoint) : ℝ

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

Equations

• NavierStokes.ReferencePath.parameterJet k F p = iteratedDeriv k (fun (η : ℝ) => F (p.1, η)) p.2

theorem NavierStokes.ReferencePath.parameterJet_continuousAt {F : MasterPoint → ℝ} {p : MasterPoint} (hF : ContDiffAt ℝ (↑⊤) F p) (k : ℕ) : ContinuousAt (parameterJet k F) p

theorem NavierStokes.ReferencePath.master_parameter_jet_close {T : ℝ} (hT : 0 < T) {J : Set ℝ} (hJ : IsOpen J) {F : MasterPoint → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (masterDomain T J)) (base : ℝ → ℝ) (hzero : ∀ (u η : ℝ), F ((0, u), η) = base η) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ J) (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ δ₀ > 0, ∀ (δ : ℝ), |δ| < δ₀ → ∀ u ∈ Set.Icc 0 2, ∀ η ∈ K, |parameterJet k F ((δ, u), η) - iteratedDeriv k base η| < ε

Compactness supplies uniform control of every fixed genuine parameter jet of a smooth master family at δ=0.

noncomputable def NavierStokes.ReferencePath.transformedMaster (Φ : ℝ × ℝ → ℝ) (G : ProfileHistories.Field) (p : MasterPoint) : ℝ

Transformed master, given by Φ (master G p, G (0, p.2)).

Equations

• NavierStokes.ReferencePath.transformedMaster Φ G p = Φ (NavierStokes.ReferencePath.master G p, G (0, p.2))

theorem NavierStokes.ReferencePath.transformedMaster_smooth {T : ℝ} (hT : 0 < T) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (earlyStrip T hT J hJ).carrier) {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiff ℝ (↑⊤) Φ) : ContDiffOn ℝ (↑⊤) (transformedMaster Φ G) (masterDomain T J)

theorem NavierStokes.ReferencePath.continuation_parameter_jet_close {T : ℝ} (hT : 0 < T) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (earlyStrip T hT J hJ).carrier) {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiff ℝ (↑⊤) Φ) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ J) (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ δ₀ > 0, ∀ (δ : ℝ), 0 < δ → δ < δ₀ → ∀ (t : ℝ), 0 ≤ t → ∀ η ∈ K, |iteratedDeriv k (fun (y : ℝ) => Φ (continuation δ G (t, y), G (0, y))) η - iteratedDeriv k (fun (y : ℝ) => Φ (G (0, y), G (0, y))) η| < ε

All fixed parameter jets of any smooth transformation of the path and its endpoint converge uniformly on the whole nonnegative-time hold. Applying Φ to x, exp x, x-b, or exp(x-b) gives field, log-field, and relative-field jets.

def NavierStokes.ReferencePath.parameterInterval : Set ℝ

Parameter interval, given by Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right.

Equations

• NavierStokes.ReferencePath.parameterInterval = Set.Ioo NavierStokes.NaturalAxisCoefficients.window.left NavierStokes.NaturalAxisCoefficients.window.right

theorem NavierStokes.ReferencePath.parameterInterval_open : IsOpen parameterInterval

noncomputable def NavierStokes.ReferencePath.rampLimit : ℝ

Ramp limit, given by Real.log (41 / 40 : ℝ).

Equations

• NavierStokes.ReferencePath.rampLimit = Real.log (41 / 40)

theorem NavierStokes.ReferencePath.rampLimit_pos : 0 < rampLimit

theorem NavierStokes.ReferencePath.exists_small_length {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ 2 * δ < rampLimit ∧ δ < ε

structure NavierStokes.ReferencePath.Input : Type

Only the proved natural-profile regularity and positivity are used in constructing REF. The natural ODE is not replaced by a surrogate assumption.

• scale : ℝ

  Scale of Input, of type ℝ.

• scale_pos : 0 < self.scale
• f : ProfileHistories.Field

  F of Input, of type Field.

• U : ProfileHistories.Field

  U of Input, of type Field.

• f_smooth : ContDiffOn ℝ (↑⊤) self.f (NaturalProfile.domain self.scale)
• U_smooth : ContDiffOn ℝ (↑⊤) self.U (NaturalProfile.domain self.scale)
• positive (p : ℝ × ℝ) : p ∈ NaturalProfile.domain self.scale → 0 ≤ self.scale * p.1 → self.scale * p.1 ≤ 41 / 10 → 0 < self.f p

noncomputable def NavierStokes.ReferencePath.Input.ofNatural {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (F : NaturalProfile.ProfileFamily d Λ C) : Input

Of natural, bundling scale, scale_pos, f, U and the required compatibility proofs.

Equations

• NavierStokes.ReferencePath.Input.ofNatural hΛ F = { scale := Λ, scale_pos := hΛ, f := F.f, U := F.U, f_smooth := ⋯, U_smooth := ⋯, positive := ⋯ }

noncomputable def NavierStokes.ReferencePath.Input.endpoint (N : Input) : ℝ

Endpoint, given by 4 / N.scale.

Equations

• N.endpoint = 4 / N.scale

theorem NavierStokes.ReferencePath.Input.endpoint_pos (N : Input) : 0 < N.endpoint

theorem NavierStokes.ReferencePath.Input.scale_endpoint (N : Input) : N.scale * N.endpoint = 4

noncomputable def NavierStokes.ReferencePath.Input.fromLog (N : Input) (p : ProfileHistories.Point) : ProfileHistories.Point

From log, given by (N.endpoint * Real.exp p.1, p.2).

Equations

• N.fromLog p = (N.endpoint * Real.exp p.1, p.2)

noncomputable def NavierStokes.ReferencePath.Input.logTime (N : Input) (X : ℝ) : ℝ

Log time, given by Real.log (X / N.endpoint).

Equations

• N.logTime X = Real.log (X / N.endpoint)

noncomputable def NavierStokes.ReferencePath.Input.logF (N : Input) : ProfileHistories.Field

Log F, defined pointwise by Real.log (N.f (N.fromLog p)).

Equations

• N.logF p = Real.log (N.f (N.fromLog p))

noncomputable def NavierStokes.ReferencePath.Input.logU (N : Input) : ProfileHistories.Field

Log U, defined pointwise by N.U (N.fromLog p).

Equations

• N.logU p = N.U (N.fromLog p)

theorem NavierStokes.ReferencePath.Input.fromLog_smooth (N : Input) : ContDiff ℝ (↑⊤) N.fromLog

theorem NavierStokes.ReferencePath.Input.fromLog_scaled (N : Input) (p : ProfileHistories.Point) : N.scale * (N.fromLog p).1 = 4 * Real.exp p.1

theorem NavierStokes.ReferencePath.Input.fromLog_mem (N : Input) {p : ProfileHistories.Point} (hp : p ∈ (earlyStrip rampLimit rampLimit_pos parameterInterval parameterInterval_open).carrier) : N.fromLog p ∈ NaturalProfile.domain N.scale

theorem NavierStokes.ReferencePath.Input.fromLog_f_pos (N : Input) {p : ProfileHistories.Point} (hp : p ∈ (earlyStrip rampLimit rampLimit_pos parameterInterval parameterInterval_open).carrier) : 0 < N.f (N.fromLog p)

theorem NavierStokes.ReferencePath.Input.logF_smooth (N : Input) : ContDiffOn ℝ (↑⊤) N.logF (earlyStrip rampLimit rampLimit_pos parameterInterval parameterInterval_open).carrier

theorem NavierStokes.ReferencePath.Input.logU_smooth (N : Input) : ContDiffOn ℝ (↑⊤) N.logU (earlyStrip rampLimit rampLimit_pos parameterInterval parameterInterval_open).carrier

theorem NavierStokes.ReferencePath.Input.fromLog_logTime (N : Input) {X η : ℝ} (hX : 0 < X) : N.fromLog (N.logTime X, η) = (X, η)

theorem NavierStokes.ReferencePath.Input.logTime_fromLog (N : Input) (t : ℝ) : N.logTime (N.endpoint * Real.exp t) = t

theorem NavierStokes.ReferencePath.Input.logTime_le_iff (N : Input) {X t : ℝ} (hX : 0 < X) : N.logTime X ≤ t ↔ X ≤ N.endpoint * Real.exp t

theorem NavierStokes.ReferencePath.Input.le_logTime_iff (N : Input) {X t : ℝ} (hX : 0 < X) : t ≤ N.logTime X ↔ N.endpoint * Real.exp t ≤ X

def NavierStokes.ReferencePath.Input.radialDomain (N : Input) : ProfileHistories.RadialDomain

The radial domain of the extended profiles has no upper radial endpoint.

Equations

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

theorem NavierStokes.ReferencePath.Input.natural_mem_of_le_endpoint (N : Input) {p : ProfileHistories.Point} (hp : p ∈ N.radialDomain.carrier) (hX : p.1 ≤ N.endpoint) : p ∈ NaturalProfile.domain N.scale

noncomputable def NavierStokes.ReferencePath.Input.refF (N : Input) (δ : ℝ) : ProfileHistories.Field

Ref F, defined pointwise by if p.1 ≤ N.endpoint then N.f p else Real.exp (continuation δ N.logF (N.logTime p.1, p.2)).

Equations

• N.refF δ p = if p.1 ≤ N.endpoint then N.f p else Real.exp (NavierStokes.ReferencePath.continuation δ N.logF (N.logTime p.1, p.2))

noncomputable def NavierStokes.ReferencePath.Input.refU (N : Input) (δ : ℝ) : ProfileHistories.Field

Ref U, defined pointwise by if p.1 ≤ N.endpoint then N.U p else continuation δ N.logU (N.logTime p.1, p.2).

Equations

• N.refU δ p = if p.1 ≤ N.endpoint then N.U p else NavierStokes.ReferencePath.continuation δ N.logU (N.logTime p.1, p.2)

theorem NavierStokes.ReferencePath.Input.refF_eq_natural_initial (N : Input) (δ : ℝ) {p : ProfileHistories.Point} (hp : p.1 ≤ N.endpoint) : N.refF δ p = N.f p

theorem NavierStokes.ReferencePath.Input.refU_eq_natural_initial (N : Input) (δ : ℝ) {p : ProfileHistories.Point} (hp : p.1 ≤ N.endpoint) : N.refU δ p = N.U p

theorem NavierStokes.ReferencePath.Input.refF_pos (N : Input) (δ : ℝ) {p : ProfileHistories.Point} (hp : p ∈ N.radialDomain.carrier) (hX : 0 ≤ p.1) : 0 < N.refF δ p

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

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

theorem NavierStokes.ReferencePath.Input.refF_eq_logtime (N : Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ parameterInterval) (hX : 0 < p.1) : N.refF δ p = Real.exp (continuation δ N.logF (N.logTime p.1, p.2))

theorem NavierStokes.ReferencePath.Input.refU_eq_logtime (N : Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ parameterInterval) (hX : 0 < p.1) : N.refU δ p = continuation δ N.logU (N.logTime p.1, p.2)

theorem NavierStokes.ReferencePath.Input.logtime_smoothAt (N : Input) {p : ProfileHistories.Point} (hX : 0 < p.1) : ContDiffAt ℝ (↑⊤) (fun (q : ProfileHistories.Point) => (N.logTime q.1, q.2)) p

theorem NavierStokes.ReferencePath.Input.refF_smooth (N : Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) : ContDiffOn ℝ (↑⊤) (N.refF δ) N.radialDomain.carrier

theorem NavierStokes.ReferencePath.Input.refU_smooth (N : Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) : ContDiffOn ℝ (↑⊤) (N.refU δ) N.radialDomain.carrier

theorem NavierStokes.ReferencePath.Input.refF_frozen (N : Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ parameterInterval) (hX : N.endpoint * Real.exp (2 * δ) ≤ p.1) : N.refF δ p = Real.exp (continuation δ N.logF (2 * δ, p.2))

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

noncomputable def NavierStokes.ReferencePath.Input.histories (N : Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) : ProfileHistories.Profiles N.radialDomain

Actual pressure, moments, and lag variables are recomputed from REF.

Equations

• N.histories hδ hδT P0 hP0 = { f := N.refF δ, U := N.refU δ, f_smooth := ⋯, U_smooth := ⋯, pressure0 := P0, pressure0_smooth := ⋯ }

theorem NavierStokes.ReferencePath.Input.logTime_hasDerivAt (N : Input) {X : ℝ} (hX : 0 < X) : HasDerivAt N.logTime (1 / X) X

theorem NavierStokes.ReferencePath.Input.log_refF_hasDerivAt (N : Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ parameterInterval) (hX : 0 < p.1) : HasDerivAt (fun (X : ℝ) => Real.log (N.refF δ (X, p.2))) (slopeCutoff δ (N.logTime p.1) * ProfileHistories.radialPartial N.logF (N.logTime p.1, p.2) / p.1) p.1

theorem NavierStokes.ReferencePath.Input.refU_hasDerivAt (N : Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ parameterInterval) (hX : 0 < p.1) : HasDerivAt (fun (X : ℝ) => N.refU δ (X, p.2)) (slopeCutoff δ (N.logTime p.1) * ProfileHistories.radialPartial N.logU (N.logTime p.1, p.2) / p.1) p.1

theorem NavierStokes.ReferencePath.Input.natural_logtime_deriv (N : Input) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (NaturalProfile.domain N.scale)) {p : ProfileHistories.Point} (hp : p ∈ (earlyStrip rampLimit rampLimit_pos parameterInterval parameterInterval_open).carrier) : HasDerivAt (fun (t : ℝ) => F (N.fromLog (t, p.2))) ((N.fromLog p).1 * ProfileHistories.radialPartial F (N.fromLog p)) p.1

theorem NavierStokes.ReferencePath.Input.radialPartial_logF (N : Input) {p : ProfileHistories.Point} (hp : p ∈ (earlyStrip rampLimit rampLimit_pos parameterInterval parameterInterval_open).carrier) : ProfileHistories.radialPartial N.logF p = (N.fromLog p).1 * ProfileHistories.radialPartial N.f (N.fromLog p) / N.f (N.fromLog p)

theorem NavierStokes.ReferencePath.Input.radialPartial_logU (N : Input) {p : ProfileHistories.Point} (hp : p ∈ (earlyStrip rampLimit rampLimit_pos parameterInterval parameterInterval_open).carrier) : ProfileHistories.radialPartial N.logU p = (N.fromLog p).1 * ProfileHistories.radialPartial N.U (N.fromLog p)

theorem NavierStokes.ReferencePath.Input.same_radius_log_slope (N : Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ parameterInterval) (hX : 0 < p.1) (ht : N.logTime p.1 < rampLimit) : p.1 * deriv (fun (X : ℝ) => Real.log (N.refF δ (X, p.2))) p.1 = slopeCutoff δ (N.logTime p.1) * (p.1 * ProfileHistories.radialPartial N.f p / N.f p)

Exact same-X damping of the natural logarithmic slope on the natural region.

theorem NavierStokes.ReferencePath.Input.same_radius_U_slope (N : Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ parameterInterval) (hX : 0 < p.1) (ht : N.logTime p.1 < rampLimit) : p.1 * deriv (fun (X : ℝ) => N.refU δ (X, p.2)) p.1 = slopeCutoff δ (N.logTime p.1) * (p.1 * ProfileHistories.radialPartial N.U p)

Exact same-X damping of the natural axial slope.

theorem NavierStokes.ReferencePath.Input.endpoint_f_pos (N : Input) {η : ℝ} (hη : η ∈ parameterInterval) : 0 < N.f (N.endpoint, η)

theorem NavierStokes.ReferencePath.Input.ref_log_transformed_jet_close (N : Input) {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiff ℝ (↑⊤) Φ) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ parameterInterval) (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ δ₀ > 0, ∀ (δ : ℝ), 0 < δ → δ < δ₀ → ∀ (X : ℝ), N.endpoint ≤ X → ∀ η ∈ K, |iteratedDeriv k (fun (y : ℝ) => Φ (Real.log (N.refF δ (X, y)), Real.log (N.f (N.endpoint, y)))) η - iteratedDeriv k (fun (y : ℝ) => Φ (Real.log (N.f (N.endpoint, y)), Real.log (N.f (N.endpoint, y)))) η| < ε

theorem NavierStokes.ReferencePath.Input.ref_U_transformed_jet_close (N : Input) {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiff ℝ (↑⊤) Φ) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ parameterInterval) (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ δ₀ > 0, ∀ (δ : ℝ), 0 < δ → δ < δ₀ → ∀ (X : ℝ), N.endpoint ≤ X → ∀ η ∈ K, |iteratedDeriv k (fun (y : ℝ) => Φ (N.refU δ (X, y), N.U (N.endpoint, y))) η - iteratedDeriv k (fun (y : ℝ) => Φ (N.U (N.endpoint, y), N.U (N.endpoint, y))) η| < ε

theorem NavierStokes.ReferencePath.Input.iteratedDeriv_zero_function (k : ℕ) : (iteratedDeriv k fun (x : ℝ) => 0) = fun (x : ℝ) => 0

theorem NavierStokes.ReferencePath.Input.ref_log_error_jet_close (N : Input) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ parameterInterval) (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ δ₀ > 0, ∀ (δ : ℝ), 0 < δ → δ < δ₀ → ∀ (X : ℝ), N.endpoint ≤ X → ∀ η ∈ K, |iteratedDeriv k (fun (y : ℝ) => Real.log (N.refF δ (X, y)) - Real.log (N.f (N.endpoint, y))) η| < ε

theorem NavierStokes.ReferencePath.Input.ref_U_error_jet_close (N : Input) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ parameterInterval) (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ δ₀ > 0, ∀ (δ : ℝ), 0 < δ → δ < δ₀ → ∀ (X : ℝ), N.endpoint ≤ X → ∀ η ∈ K, |iteratedDeriv k (fun (y : ℝ) => N.refU δ (X, y) - N.U (N.endpoint, y)) η| < ε

theorem NavierStokes.ReferencePath.Input.ref_relative_error_jet_close (N : Input) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ parameterInterval) (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ δ₀ > 0, ∀ (δ : ℝ), 0 < δ → δ < δ₀ → ∀ (X : ℝ), N.endpoint ≤ X → ∀ η ∈ K, |iteratedDeriv k (fun (y : ℝ) => N.refF δ (X, y) / N.f (N.endpoint, y) - 1) η| < ε

theorem NavierStokes.ReferencePath.Input.ref_field_error_jet_close (N : Input) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ parameterInterval) (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ δ₀ > 0, ∀ (δ : ℝ), 0 < δ → δ < δ₀ → ∀ (X : ℝ), N.endpoint ≤ X → ∀ η ∈ K, |iteratedDeriv k (fun (y : ℝ) => N.refF δ (X, y) - N.f (N.endpoint, y)) η| < ε

def NavierStokes.ReferencePath.Input.Xbig : ℝ

Xbig, given by 100.

Equations

• NavierStokes.ReferencePath.Input.Xbig = 100

def NavierStokes.ReferencePath.Input.Xi : ℝ

Xi, given by 110.

Equations

• NavierStokes.ReferencePath.Input.Xi = 110

theorem NavierStokes.ReferencePath.Input.freeze_before_Xbig (N : Input) (hscale : 1 ≤ N.scale) {δ : ℝ} (hδT : 2 * δ < rampLimit) : N.endpoint * Real.exp (2 * δ) < Xbig

theorem NavierStokes.ReferencePath.Input.frozen_through_Xi (N : Input) (hscale : 1 ≤ N.scale) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < rampLimit) {p : ProfileHistories.Point} (hη : p.2 ∈ parameterInterval) (hX : p.1 ∈ Set.Icc Xbig Xi) : N.refF δ p = Real.exp (continuation δ N.logF (2 * δ, p.2)) ∧ N.refU δ p = continuation δ N.logU (2 * δ, p.2)

In particular the reference is already frozen throughout [100,110].