The same compensated histories and the terminal backward stress

All forward histories in this file use the supplied compensation witness. The base outgoing energy identity is kept explicit; zero changes alone do not imply a zero total energy moment.

Derivatives of the actual compensated heat histories

The first radial identities come from the actual finite integrals. Joint smoothness and parameter differentiation of those integrals then give the mixed identities on the open physical parameter band.

noncomputable def NavierStokes.HeatSwitchHistoryDerivatives.interiorDomain : ProfileHistories.RadialDomain

Interior domain, bundling carrier, isOpen, scale_mem.

Equations

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

theorem NavierStokes.HeatSwitchHistoryDerivatives.interior_to_band {eta : ℝ} (heta : eta ∈ Set.Ioo (-1) 1) : eta ∈ HeatedOutgoing.parameterDomain

theorem NavierStokes.HeatSwitchHistoryDerivatives.realize_contDiffOn {f : HeatSwitchCone.Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) (delta : ℝ) {c : ℝ → HeatSwitchCone.Coeff} (hc : ContDiffOn ℝ (↑⊤) c HeatedOutgoing.parameterDomain) : ContDiffOn ℝ (↑⊤) (HeatSwitchCone.realize f delta c) interiorDomain.carrier

theorem NavierStokes.HeatSwitchHistoryDerivatives.logE_contDiffOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContDiffOn ℝ (↑⊤) (HeatSwitchCone.logE F XR w.coefficients) interiorDomain.carrier

theorem NavierStokes.HeatSwitchHistoryDerivatives.logI_contDiffOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContDiffOn ℝ (↑⊤) (HeatSwitchCone.logI F XR w.coefficients) interiorDomain.carrier

theorem NavierStokes.HeatSwitchHistoryDerivatives.logS_contDiffOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContDiffOn ℝ (↑⊤) (HeatSwitchCone.logS F XR w.coefficients) interiorDomain.carrier

theorem NavierStokes.HeatSwitchHistoryDerivatives.logPi_contDiffOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContDiffOn ℝ (↑⊤) (HeatSwitchCone.logPi F XR w.coefficients) interiorDomain.carrier

theorem NavierStokes.HeatSwitchHistoryDerivatives.integral_hasDerivAt {f : ℝ → ℝ} (hf : Continuous f) (a y : ℝ) : HasDerivAt (fun (y : ℝ) => ∫ (t : ℝ) in a..y, f t) (f y) y

theorem NavierStokes.HeatSwitchHistoryDerivatives.logI_hasDerivAt (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (p : HeatSwitchCone.Point) (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : HasDerivAt (fun (y : ℝ) => HeatSwitchCone.logI F XR w.coefficients (y, p.2)) (Real.exp (3 * p.1 / 2) * HeatSwitchCone.logE F XR w.coefficients p) p.1

theorem NavierStokes.HeatSwitchHistoryDerivatives.logS_hasDerivAt (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (p : HeatSwitchCone.Point) (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : HasDerivAt (fun (y : ℝ) => HeatSwitchCone.logS F XR w.coefficients (y, p.2)) (Real.exp p.1 * (F.logU p ^ 2 - HeatSwitchCone.logE F XR w.coefficients p ^ 2 / 2)) p.1

theorem NavierStokes.HeatSwitchHistoryDerivatives.logPi_hasDerivAt (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (p : HeatSwitchCone.Point) (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : HasDerivAt (fun (y : ℝ) => HeatSwitchCone.logPi F XR w.coefficients (y, p.2)) (HeatSwitchCone.logE F XR w.coefficients p ^ 2 / 2) p.1

noncomputable def NavierStokes.HeatSwitchHistoryDerivatives.angularWeight (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatSwitchCone.Coeff) (p : HeatSwitchCone.Point) : ℝ

Angular weight, given by Real.exp (3 * p.1 / 2) * logE F XR c p.

Equations

• NavierStokes.HeatSwitchHistoryDerivatives.angularWeight F XR c p = Real.exp (3 * p.1 / 2) * NavierStokes.HeatSwitchCone.logE F XR c p

noncomputable def NavierStokes.HeatSwitchHistoryDerivatives.energyWeight (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatSwitchCone.Coeff) (p : HeatSwitchCone.Point) : ℝ

Energy weight, given by Real.exp p.1 * (F.logU p ^ 2 - logE F XR c p ^ 2 / 2).

Equations

• NavierStokes.HeatSwitchHistoryDerivatives.energyWeight F XR c p = Real.exp p.1 * (F.logU p ^ 2 - NavierStokes.HeatSwitchCone.logE F XR c p ^ 2 / 2)

noncomputable def NavierStokes.HeatSwitchHistoryDerivatives.pressureWeight (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatSwitchCone.Coeff) (p : HeatSwitchCone.Point) : ℝ

Pressure weight, given by logE F XR c p ^ 2 / 2.

Equations

• NavierStokes.HeatSwitchHistoryDerivatives.pressureWeight F XR c p = NavierStokes.HeatSwitchCone.logE F XR c p ^ 2 / 2

theorem NavierStokes.HeatSwitchHistoryDerivatives.angularWeight_contDiffOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContDiffOn ℝ (↑⊤) (angularWeight F XR w.coefficients) interiorDomain.carrier

theorem NavierStokes.HeatSwitchHistoryDerivatives.energyWeight_contDiffOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContDiffOn ℝ (↑⊤) (energyWeight F XR w.coefficients) interiorDomain.carrier

theorem NavierStokes.HeatSwitchHistoryDerivatives.pressureWeight_contDiffOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContDiffOn ℝ (↑⊤) (pressureWeight F XR w.coefficients) interiorDomain.carrier

theorem NavierStokes.HeatSwitchHistoryDerivatives.history_primitive_representation {H G : HeatSwitchCone.Point → ℝ} (hG : ContDiffOn ℝ (↑⊤) G interiorDomain.carrier) (hH : ∀ p ∈ interiorDomain.carrier, HasDerivAt (fun (y : ℝ) => H (y, p.2)) (G p) p.1) {p : HeatSwitchCone.Point} (hp : p ∈ interiorDomain.carrier) : H p = H (0, p.2) + ProfileHistories.primitive G p

theorem NavierStokes.HeatSwitchHistoryDerivatives.history_parameter_mixed {H G : HeatSwitchCone.Point → ℝ} (hH : ContDiffOn ℝ (↑⊤) H interiorDomain.carrier) (hG : ContDiffOn ℝ (↑⊤) G interiorDomain.carrier) (hODE : ∀ p ∈ interiorDomain.carrier, HasDerivAt (fun (y : ℝ) => H (y, p.2)) (G p) p.1) {p : HeatSwitchCone.Point} (hp : p ∈ interiorDomain.carrier) : HasDerivAt (fun (y : ℝ) => ProfileHistories.parameterPartial H (y, p.2)) (ProfileHistories.parameterPartial G p) p.1

Mixed differentiation of a genuine smooth history. The radial identity in this helper is supplied below by the just-proved fundamental-theorem identities for the actual three histories.

theorem NavierStokes.HeatSwitchHistoryDerivatives.within_parameter_eq {H : HeatSwitchCone.Point → ℝ} (hH : ContDiffOn ℝ (↑⊤) H interiorDomain.carrier) {p : HeatSwitchCone.Point} (hp : p ∈ interiorDomain.carrier) : derivWithin (fun (eta : ℝ) => H (p.1, eta)) HeatedOutgoing.parameterDomain p.2 = ProfileHistories.parameterPartial H p

theorem NavierStokes.HeatSwitchHistoryDerivatives.ordinary_parameter_eq {H : HeatSwitchCone.Point → ℝ} (hH : ContDiffOn ℝ (↑⊤) H interiorDomain.carrier) {p : HeatSwitchCone.Point} (hp : p ∈ interiorDomain.carrier) : deriv (fun (eta : ℝ) => H (p.1, eta)) p.2 = ProfileHistories.parameterPartial H p

theorem NavierStokes.HeatSwitchHistoryDerivatives.history_parameter_mixed_within {H G : HeatSwitchCone.Point → ℝ} (hH : ContDiffOn ℝ (↑⊤) H interiorDomain.carrier) (hG : ContDiffOn ℝ (↑⊤) G interiorDomain.carrier) (hODE : ∀ p ∈ interiorDomain.carrier, HasDerivAt (fun (y : ℝ) => H (y, p.2)) (G p) p.1) {p : HeatSwitchCone.Point} (hp : p ∈ interiorDomain.carrier) : HasDerivAt (fun (y : ℝ) => derivWithin (fun (eta : ℝ) => H (y, eta)) HeatedOutgoing.parameterDomain p.2) (ProfileHistories.parameterPartial G p) p.1

theorem NavierStokes.HeatSwitchHistoryDerivatives.angularWeight_parameter (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : HeatSwitchCone.Point} (hp : p ∈ interiorDomain.carrier) : ProfileHistories.parameterPartial (angularWeight F XR w.coefficients) p = Real.exp (3 * p.1 / 2) * derivWithin (fun (eta : ℝ) => HeatSwitchCone.logE F XR w.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2

theorem NavierStokes.HeatSwitchHistoryDerivatives.energyWeight_parameter (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : HeatSwitchCone.Point} (hp : p ∈ interiorDomain.carrier) : ProfileHistories.parameterPartial (energyWeight F XR w.coefficients) p = Real.exp p.1 * (2 * F.logU p * OutgoingHistories.dEta F.logU p - HeatSwitchCone.logE F XR w.coefficients p * derivWithin (fun (eta : ℝ) => HeatSwitchCone.logE F XR w.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2)

theorem NavierStokes.HeatSwitchHistoryDerivatives.pressureWeight_parameter (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : HeatSwitchCone.Point} (hp : p ∈ interiorDomain.carrier) : ProfileHistories.parameterPartial (pressureWeight F XR w.coefficients) p = HeatSwitchCone.logE F XR w.coefficients p * derivWithin (fun (eta : ℝ) => HeatSwitchCone.logE F XR w.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2

theorem NavierStokes.HeatSwitchHistoryDerivatives.logI_eta_hasDerivAt (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (p : HeatSwitchCone.Point) (hp : p.2 ∈ Set.Ioo (-1) 1) : HasDerivAt (fun (y : ℝ) => derivWithin (fun (eta : ℝ) => HeatSwitchCone.logI F XR w.coefficients (y, eta)) HeatedOutgoing.parameterDomain p.2) (Real.exp (3 * p.1 / 2) * derivWithin (fun (eta : ℝ) => HeatSwitchCone.logE F XR w.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2) p.1

The mixed derivative uses the actual parameter derivative already appearing in the stress formula.

theorem NavierStokes.HeatSwitchHistoryDerivatives.logS_eta_hasDerivAt (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (p : HeatSwitchCone.Point) (hp : p.2 ∈ Set.Ioo (-1) 1) : HasDerivAt (fun (y : ℝ) => derivWithin (fun (eta : ℝ) => HeatSwitchCone.logS F XR w.coefficients (y, eta)) HeatedOutgoing.parameterDomain p.2) (Real.exp p.1 * (2 * F.logU p * OutgoingHistories.dEta F.logU p - HeatSwitchCone.logE F XR w.coefficients p * derivWithin (fun (eta : ℝ) => HeatSwitchCone.logE F XR w.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2)) p.1

theorem NavierStokes.HeatSwitchHistoryDerivatives.logPi_eta_hasDerivAt (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (p : HeatSwitchCone.Point) (hp : p.2 ∈ Set.Ioo (-1) 1) : HasDerivAt (fun (y : ℝ) => derivWithin (fun (eta : ℝ) => HeatSwitchCone.logPi F XR w.coefficients (y, eta)) HeatedOutgoing.parameterDomain p.2) (HeatSwitchCone.logE F XR w.coefficients p * derivWithin (fun (eta : ℝ) => HeatSwitchCone.logE F XR w.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2) p.1

noncomputable def NavierStokes.TerminalHistoryBridge.angularHistory (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (η X : ℝ) : ℝ

Angular history, given by ∫ u in Ioc 0 X, HeatedOutgoing.H F XR c (u,η).

Equations

• NavierStokes.TerminalHistoryBridge.angularHistory F XR c η X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.HeatedOutgoing.H F XR c (u, η)

noncomputable def NavierStokes.TerminalHistoryBridge.energyHistory (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (η X : ℝ) : ℝ

Energy history, given by ∫ u in Ioc 0 X, HeatedOutgoing.energyDensity F XR c η u.

Equations

• NavierStokes.TerminalHistoryBridge.energyHistory F XR c η X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.HeatedOutgoing.energyDensity F XR c η u

noncomputable def NavierStokes.TerminalHistoryBridge.powerHistory (F : OutgoingProfile.Profile) (XR X : ℝ) : ℝ

Power history, given by ∫ u in Ioc 0 X, OutgoingDilation.powerH F XR u.

Equations

• NavierStokes.TerminalHistoryBridge.powerHistory F XR X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.OutgoingDilation.powerH F XR u

theorem NavierStokes.TerminalHistoryBridge.split_positive_integral {f : ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) {X : ℝ} (hX : 0 ≤ X) : (∫ (u : ℝ) in Set.Ioc 0 X, f u) + ∫ (u : ℝ) in Set.Ioi X, f u = ∫ (u : ℝ) in Set.Ioi 0, f u

theorem NavierStokes.TerminalHistoryBridge.angularHistory_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : 0 < X) : MeasureTheory.IntegrableOn (fun (u : ℝ) => HeatedOutgoing.H F XR w.coefficients (u, η)) (Set.Ioc 0 X) MeasureTheory.volume

theorem NavierStokes.TerminalHistoryBridge.angularHistory_eq_power_sub_future {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : 0 < X) : angularHistory F XR w.coefficients η X = powerHistory F XR X - ∫ (u : ℝ) in Set.Ioi X, HeatedOutgoing.H F XR w.coefficients (u, η) - OutgoingDilation.powerH F XR u

The exact renormalized angular moment determines the forward history from the future, for the very same supplied compensation coefficients.

theorem NavierStokes.TerminalHistoryBridge.energyHistory_eq_neg_future {F : OutgoingProfile.Profile} {XR C B : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : 0 ≤ X) : energyHistory F XR w.coefficients η X = -∫ (u : ℝ) in Set.Ioi X, HeatedOutgoing.energyDensity F XR w.coefficients η u

theorem NavierStokes.TerminalHistoryBridge.square_integrable_after_switch {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : OutgoingDilation.switchRadius F XR ≤ X) : MeasureTheory.IntegrableOn (fun (u : ℝ) => HeatedOutgoing.E F XR w.coefficients (u, η) ^ 2) (Set.Ioi X) MeasureTheory.volume

theorem NavierStokes.TerminalHistoryBridge.energyHistory_eq_square_future {F : OutgoingProfile.Profile} {XR C B : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : OutgoingDilation.switchRadius F XR ≤ X) : energyHistory F XR w.coefficients η X = 1 / 2 * ∫ (u : ℝ) in Set.Ioi X, HeatedOutgoing.E F XR w.coefficients (u, η) ^ 2

theorem NavierStokes.TerminalHistoryBridge.transport_histories_zero_after_switch {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (η : ℝ) {X : ℝ} (hX : OutgoingDilation.switchRadius F XR ≤ X) : HeatedOutgoing.U F XR (X, η) = 0 ∧ HeatedOutgoing.M F XR η X = 0 ∧ HeatedOutgoing.J F XR w.coefficients η X = 0

noncomputable def NavierStokes.TerminalHistoryBridge.normalization (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Normalization, given by TerminalPressure.releasedNormalization F.data (OutgoingDilation.switchRadius F XR).

Equations

• NavierStokes.TerminalHistoryBridge.normalization F XR = NavierStokes.TerminalPressure.releasedNormalization F.data (NavierStokes.OutgoingDilation.switchRadius F XR)

noncomputable def NavierStokes.TerminalHistoryBridge.shift (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Shift, given by Real.log (OutgoingDilation.switchRadius F XR) - 1/5.

Equations

• NavierStokes.TerminalHistoryBridge.shift F XR = Real.log (NavierStokes.OutgoingDilation.switchRadius F XR) - 1 / 5

noncomputable def NavierStokes.TerminalHistoryBridge.physicalAngular (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) : SimilarityProfile.PhysicalProfile

Physical angular, given by SimilarityProfile.pullback F.data.h (-TerminalPressure.amplitudeExponent F.data.h) (HeatedOutgoing.E F XR c).

Equations

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

noncomputable def NavierStokes.TerminalHistoryBridge.physicalPressure (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) : SimilarityProfile.PhysicalProfile

Physical pressure, given by SimilarityProfile.pullback F.data.h (-2*TerminalPressure.amplitudeExponent F.data.h) (HeatedOutgoing.Pi F XR c).

Equations

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

theorem NavierStokes.TerminalHistoryBridge.physicalAngular_eq_terminal (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hfull : 1 / 2 ≤ Real.log (SimilarityProfile.X F.data.h p / OutgoingDilation.switchRadius F XR) + 1 / 5) : physicalAngular F XR c p = TerminalStress.physicalHeat (normalization F XR) (1 + F.data.h) p * TerminalPressure.outgoingTaper F.data (shift F XR) (Real.log (SimilarityProfile.X F.data.h p))

theorem NavierStokes.TerminalHistoryBridge.full_switch_radial {F : OutgoingProfile.Profile} {XR : ℝ} (hXR : 0 < XR) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hfull : 1 / 2 ≤ Real.log (SimilarityProfile.X F.data.h p / OutgoingDilation.switchRadius F XR) + 1 / 5) {u : ℝ} (hu : p.2.1 ≤ u) : 1 / 2 ≤ Real.log (SimilarityProfile.X F.data.h (p.1, u, p.2.2) / OutgoingDilation.switchRadius F XR) + 1 / 5

theorem NavierStokes.TerminalHistoryBridge.physicalPressure_eq_terminal (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hfull : 1 / 2 ≤ Real.log (SimilarityProfile.X F.data.h p / OutgoingDilation.switchRadius F XR) + 1 / 5) : physicalPressure F XR c p = TerminalPressure.outgoingPressure (normalization F XR) F.data (shift F XR) p

Exact physical canonical pressure, with its required q^(-2A) factor. This is a change of variables in the actual improper integral.

The actual forward stress on the switched tail

noncomputable def NavierStokes.TerminalHistoryBridge.forwardTheta (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (p : ℝ × ℝ) : ℝ

Forward theta, constructed using HeatSwitchCone.logE.

Equations

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

noncomputable def NavierStokes.TerminalHistoryBridge.forwardAxial (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (p : ℝ × ℝ) : ℝ

Forward axial, given by XR * Real.exp p.1 * HeatSwitchCone.Ns F XR c p / (CoordinateAlgebra.L F.data.h p.2 * Real.sqrt (2 * XR * Real.exp p.1)).

Equations

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

theorem NavierStokes.TerminalHistoryBridge.terminalStart_after_endpoint (F : OutgoingProfile.Profile) : F.data.core.endpoint < TerminalCone.terminalStart F.data

theorem NavierStokes.TerminalHistoryBridge.Qs_after_endpoint (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) {p : ℝ × ℝ} (hp : F.data.core.endpoint ≤ p.1) : HeatSwitchCone.Qs F XR c p = -1 + ((1 - F.data.h) * HeatSwitchCone.logI F XR c p - StressAlgebra.axialExponent F.data.h * p.2 * derivWithin (fun (η : ℝ) => HeatSwitchCone.logI F XR c (p.1, η)) HeatedOutgoing.parameterDomain p.2) / (Real.exp (3 * p.1 / 2) * HeatSwitchCone.logE F XR c p)

theorem NavierStokes.TerminalHistoryBridge.Ns_after_endpoint (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) {p : ℝ × ℝ} (hp : F.data.core.endpoint ≤ p.1) : HeatSwitchCone.Ns F XR c p = (4 * F.data.h * p.2 * HeatSwitchCone.logS F XR c p - StressAlgebra.coordinateFactor p.2 * derivWithin (fun (η : ℝ) => HeatSwitchCone.logS F XR c (p.1, η)) HeatedOutgoing.parameterDomain p.2) / Real.exp p.1 + 4 * StressAlgebra.velocityExponent F.data.h * p.2 * HeatSwitchCone.logPi F XR c p - StressAlgebra.coordinateFactor p.2 * derivWithin (fun (η : ℝ) => HeatSwitchCone.logPi F XR c (p.1, η)) HeatedOutgoing.parameterDomain p.2

theorem NavierStokes.TerminalHistoryBridge.radialB_after_endpoint (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) {p : ℝ × ℝ} (hp : F.data.core.endpoint < p.1) : HeatSwitchCone.radialB F XR c p = 0

theorem NavierStokes.TerminalHistoryBridge.radialA_eq_profileSpeed (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {y η : ℝ} (hy : TerminalCone.terminalStart F.data < y) (hη : η ∈ HeatedOutgoing.parameterDomain) : HeatSwitchCone.radialA F XR w.coefficients (y, η) = TerminalEdgeFactor.profileSpeed (normalization F XR) F.data (shift F XR) (TerminalCone.profilePoint F y η)

theorem NavierStokes.TerminalHistoryBridge.forward_normalization (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : ℝ × ℝ} (hp : F.data.core.endpoint < p.1) (hη : p.2 ∈ HeatedOutgoing.parameterDomain) (hQ : HeatSwitchCone.Qs F XR w.coefficients p ≠ 0) : HeatSwitchCone.normalP F XR w.coefficients p = HeatSwitchCone.radialA F XR w.coefficients p + forwardTheta F XR w.coefficients p / (HeatSwitchCone.logE F XR w.coefficients p / √(2 * XR * Real.exp p.1)) ∧ HeatSwitchCone.normalJ F XR w.coefficients p = forwardAxial F XR w.coefficients p / (HeatSwitchCone.logE F XR w.coefficients p / √(2 * XR * Real.exp p.1))

Exact change from logarithmic to physical histories

theorem NavierStokes.TerminalHistoryBridge.integral_log_radius (f : ℝ → ℝ) {XR : ℝ} (hXR : 0 < XR) (y : ℝ) : ∫ (u : ℝ) in Set.Ioc 0 (XR * Real.exp y), f u = XR * ∫ (t : ℝ) in Set.Iic y, Real.exp t * f (XR * Real.exp t)

theorem NavierStokes.TerminalHistoryBridge.sqrt_radius_exp {XR : ℝ} (hXR : 0 < XR) (y : ℝ) : √(2 * (XR * Real.exp y)) = √(2 * XR) * Real.exp (y / 2)

theorem NavierStokes.TerminalHistoryBridge.angularHistory_eq_logI (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (y : ℝ) : angularHistory F XR c η (XR * Real.exp y) = XR * √(2 * XR) * HeatSwitchCone.logI F XR c (y, η)

theorem NavierStokes.TerminalHistoryBridge.energyHistory_eq_logS (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (y : ℝ) : energyHistory F XR c η (XR * Real.exp y) = XR * HeatSwitchCone.logS F XR c (y, η)

noncomputable def NavierStokes.TerminalHistoryBridge.etaDerivative (G : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Eta derivative, given by derivWithin (fun η => G (p.1,η)) HeatedOutgoing.parameterDomain p.2.

Equations

• NavierStokes.TerminalHistoryBridge.etaDerivative G p = derivWithin (fun (η : ℝ) => G (p.1, η)) NavierStokes.HeatedOutgoing.parameterDomain p.2

noncomputable def NavierStokes.TerminalHistoryBridge.thetaStock (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (p : ℝ × ℝ) : ℝ

Theta stock as an element of ℝ.

Equations

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

noncomputable def NavierStokes.TerminalHistoryBridge.thetaWeight (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (p : ℝ × ℝ) : ℝ

Theta weight as an element of ℝ.

Equations

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

noncomputable def NavierStokes.TerminalHistoryBridge.axialWeight (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (p : ℝ × ℝ) : ℝ

Axial weight as an element of ℝ.

Equations

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

noncomputable def NavierStokes.TerminalHistoryBridge.angularResidual (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (p : ℝ × ℝ) : ℝ

Angular residual as an element of ℝ.

Equations

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

noncomputable def NavierStokes.TerminalHistoryBridge.axialResidual (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (p : ℝ × ℝ) : ℝ

Axial residual as an element of ℝ.

Equations

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

theorem NavierStokes.TerminalHistoryBridge.thetaStock_hasDerivAt (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : ℝ × ℝ} (hp : p.2 ∈ Set.Ioo (-1) 1) : HasDerivAt (fun (y : ℝ) => thetaStock F XR w.coefficients (y, p.2)) (-Real.exp (3 * p.1 / 2) * (StressAlgebra.velocityExponent F.data.h * HeatSwitchCone.logE F XR w.coefficients p + StressAlgebra.axialExponent F.data.h * p.2 * etaDerivative (HeatSwitchCone.logE F XR w.coefficients) p + ProfileHistories.radialPartial (HeatSwitchCone.logE F XR w.coefficients) p)) p.1

theorem NavierStokes.TerminalHistoryBridge.thetaWeight_hasDerivAt (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : ℝ × ℝ} (hp : p.2 ∈ Set.Ioo (-1) 1) : HasDerivAt (fun (y : ℝ) => thetaWeight F XR w.coefficients (y, p.2)) (-(XR * Real.exp p.1) * √(2 * (XR * Real.exp p.1)) * angularResidual F XR w.coefficients p) p.1

theorem NavierStokes.TerminalHistoryBridge.axialWeight_hasDerivAt (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : ℝ × ℝ} (hp : p.2 ∈ Set.Ioo (-1) 1) (hy : F.data.core.endpoint ≤ p.1) : HasDerivAt (fun (y : ℝ) => axialWeight F XR w.coefficients (y, p.2)) (-(XR * Real.exp p.1) * axialResidual F XR w.coefficients p) p.1

theorem NavierStokes.TerminalHistoryBridge.thetaWeight_eq_forward (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : ℝ × ℝ} (hp : p.2 ∈ Set.Ioo (-1) 1) (hy : F.data.core.endpoint ≤ p.1) : thetaWeight F XR w.coefficients p = 2 * (XR * Real.exp p.1) * forwardTheta F XR w.coefficients p

theorem NavierStokes.TerminalHistoryBridge.axialWeight_eq_forward (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : ℝ × ℝ} (hy : F.data.core.endpoint ≤ p.1) : axialWeight F XR w.coefficients p = √(2 * XR * Real.exp p.1) * forwardAxial F XR w.coefficients p

Genuine physical derivatives of logarithmic profiles

noncomputable def NavierStokes.TerminalHistoryBridge.logPoint (XR : ℝ) (p : ℝ × ℝ) : ℝ × ℝ

Log point, given by (Real.log (p.1/XR),p.2).

Equations

• NavierStokes.TerminalHistoryBridge.logPoint XR p = (Real.log (p.1 / XR), p.2)

noncomputable def NavierStokes.TerminalHistoryBridge.radialLift (XR : ℝ) (G : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Radial lift, given by G (logPoint XR p).

Equations

• NavierStokes.TerminalHistoryBridge.radialLift XR G p = G (NavierStokes.TerminalHistoryBridge.logPoint XR p)

theorem NavierStokes.TerminalHistoryBridge.logPoint_contDiffAt {XR : ℝ} (hXR : 0 < XR) {p : ℝ × ℝ} (hp : 0 < p.1) : ContDiffAt ℝ (↑⊤) (logPoint XR) p

theorem NavierStokes.TerminalHistoryBridge.radialLift_contDiffAt {XR : ℝ} (hXR : 0 < XR) {G : ℝ × ℝ → ℝ} (hG : ContDiffOn ℝ (↑⊤) G HeatSwitchHistoryDerivatives.interiorDomain.carrier) {p : ℝ × ℝ} (hp : 0 < p.1) (hη : p.2 ∈ Set.Ioo (-1) 1) : ContDiffAt ℝ (↑⊤) (radialLift XR G) p

theorem NavierStokes.TerminalHistoryBridge.log_radius_hasDerivAt {XR X : ℝ} (hXR : 0 < XR) (hX : 0 < X) : HasDerivAt (fun (x : ℝ) => Real.log (x / XR)) (1 / X) X

theorem NavierStokes.TerminalHistoryBridge.radialLift_partialX {XR : ℝ} (hXR : 0 < XR) {G : ℝ × ℝ → ℝ} (hG : ContDiffOn ℝ (↑⊤) G HeatSwitchHistoryDerivatives.interiorDomain.carrier) {p : ℝ × ℝ} (hp : 0 < p.1) (hη : p.2 ∈ Set.Ioo (-1) 1) : SimilarityProfile.partialX (radialLift XR G) p = ProfileHistories.radialPartial G (logPoint XR p) / p.1

theorem NavierStokes.TerminalHistoryBridge.radialLift_partialEta {XR : ℝ} (hXR : 0 < XR) {G : ℝ × ℝ → ℝ} (hG : ContDiffOn ℝ (↑⊤) G HeatSwitchHistoryDerivatives.interiorDomain.carrier) {p : ℝ × ℝ} (hp : 0 < p.1) (hη : p.2 ∈ Set.Ioo (-1) 1) : SimilarityProfile.partialEta (radialLift XR G) p = ProfileHistories.parameterPartial G (logPoint XR p)

theorem NavierStokes.TerminalHistoryBridge.radialLift_partialXX {XR : ℝ} (hXR : 0 < XR) {G : ℝ × ℝ → ℝ} (hG : ContDiffOn ℝ (↑⊤) G HeatSwitchHistoryDerivatives.interiorDomain.carrier) {p : ℝ × ℝ} (hp : 0 < p.1) (hη : p.2 ∈ Set.Ioo (-1) 1) : SimilarityProfile.partialX (SimilarityProfile.partialX (radialLift XR G)) p = (ProfileHistories.radialPartial (ProfileHistories.radialPartial G) (logPoint XR p) - ProfileHistories.radialPartial G (logPoint XR p)) / p.1 ^ 2

theorem NavierStokes.TerminalHistoryBridge.logE_radialLift (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {p : ℝ × ℝ} (hp : 0 < p.1) : radialLift XR (HeatSwitchCone.logE F XR c) p = HeatedOutgoing.E F XR c p

theorem NavierStokes.TerminalHistoryBridge.logPi_radialLift (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : ℝ × ℝ} (hp : 0 < p.1) (hη : p.2 ∈ HeatedOutgoing.parameterDomain) : radialLift XR (HeatSwitchCone.logPi F XR w.coefficients) p = HeatedOutgoing.Pi F XR w.coefficients p

noncomputable def NavierStokes.TerminalHistoryBridge.physicalLog (h b XR : ℝ) (G : ℝ × ℝ → ℝ) : SimilarityProfile.PhysicalProfile

Physical log, given by SimilarityProfile.pullback h b (radialLift XR G).

Equations

• NavierStokes.TerminalHistoryBridge.physicalLog h b XR G = NavierStokes.SimilarityProfile.pullback h b (NavierStokes.TerminalHistoryBridge.radialLift XR G)

noncomputable def NavierStokes.TerminalHistoryBridge.amplitudeOperator (V : SimilarityProfile.PhysicalProfile) (p : SimilarityProfile.PhysicalPoint) : ℝ

Amplitude operator, constructed using SimilarityProfile.partialT.

Equations

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

theorem NavierStokes.TerminalHistoryBridge.physicalLog_amplitudeOperator {h b XR : ℝ} (hh : 0 < h) (hh' : h < 1 / 2) (hXR : 0 < XR) {G : ℝ × ℝ → ℝ} (hG : ContDiffOn ℝ (↑⊤) G HeatSwitchHistoryDerivatives.interiorDomain.carrier) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : amplitudeOperator (physicalLog h b XR G) p = SimilarityProfile.q h p ^ (b - 1) * ((-b * G (logPoint XR (SimilarityProfile.inner h p)) + CoordinateAlgebra.D h * SimilarityProfile.eta h p * ProfileHistories.parameterPartial G (logPoint XR (SimilarityProfile.inner h p)) + ProfileHistories.radialPartial G (logPoint XR (SimilarityProfile.inner h p))) / CoordinateAlgebra.L h (SimilarityProfile.eta h p) - (2 * ProfileHistories.radialPartial (ProfileHistories.radialPartial G) (logPoint XR (SimilarityProfile.inner h p)) - G (logPoint XR (SimilarityProfile.inner h p)) / 2) / SimilarityProfile.X h p)

theorem NavierStokes.TerminalHistoryBridge.physicalLog_angularResidual (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : amplitudeOperator (physicalLog F.data.h (-TerminalPressure.amplitudeExponent F.data.h) XR (HeatSwitchCone.logE F XR w.coefficients)) p = SimilarityProfile.q F.data.h p ^ (-TerminalPressure.amplitudeExponent F.data.h - 1) * angularResidual F XR w.coefficients (logPoint XR (SimilarityProfile.inner F.data.h p))

theorem NavierStokes.TerminalHistoryBridge.physicalLog_axialResidual (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : SimilarityProfile.partialZ (physicalLog F.data.h (-2 * TerminalPressure.amplitudeExponent F.data.h) XR (HeatSwitchCone.logPi F XR w.coefficients)) p = SimilarityProfile.q F.data.h p ^ (-TerminalPressure.amplitudeExponent F.data.h - 1) * axialResidual F XR w.coefficients (logPoint XR (SimilarityProfile.inner F.data.h p))

theorem NavierStokes.TerminalHistoryBridge.amplitudeOperator_congr {V W : SimilarityProfile.PhysicalProfile} {p : SimilarityProfile.PhysicalPoint} (he : V =ᶠ[nhds p] W) : amplitudeOperator V p = amplitudeOperator W p

noncomputable def NavierStokes.TerminalHistoryBridge.terminalAmplitude (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : SimilarityProfile.PhysicalPoint) : ℝ

Terminal amplitude, given by TerminalStress.physicalHeat C (1+d.h) p * TerminalStress.flattening d.h (TerminalPressure.outgoingTaper d y0) p.

Equations

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

theorem NavierStokes.TerminalHistoryBridge.terminalAmplitude_operator (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {t r z : ℝ} (ht : t < 1) (hr : 0 < r) : amplitudeOperator (terminalAmplitude C d y0) (TerminalStress.radiusPoint t r z) = TerminalStress.leadingResidual C d.h (TerminalPressure.outgoingTaper d y0) t r z

theorem NavierStokes.TerminalHistoryBridge.terminal_germs (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h p / OutgoingDilation.switchRadius F XR) + 1 / 5) : physicalLog F.data.h (-TerminalPressure.amplitudeExponent F.data.h) XR (HeatSwitchCone.logE F XR w.coefficients) =ᶠ[nhds p] terminalAmplitude (normalization F XR) F.data (shift F XR) ∧ physicalLog F.data.h (-2 * TerminalPressure.amplitudeExponent F.data.h) XR (HeatSwitchCone.logPi F XR w.coefficients) =ᶠ[nhds p] TerminalPressure.outgoingPressure (normalization F XR) F.data (shift F XR)

theorem NavierStokes.TerminalHistoryBridge.terminal_angularResidual (F : OutgoingProfile.Profile) {XR C t r z : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (ht : t < 1) (hr : 0 < r) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h (TerminalStress.radiusPoint t r z) / OutgoingDilation.switchRadius F XR) + 1 / 5) : TerminalStress.leadingResidual (normalization F XR) F.data.h (TerminalPressure.outgoingTaper F.data (shift F XR)) t r z = SimilarityProfile.q F.data.h (TerminalStress.radiusPoint t r z) ^ (-TerminalPressure.amplitudeExponent F.data.h - 1) * angularResidual F XR w.coefficients (logPoint XR (SimilarityProfile.inner F.data.h (TerminalStress.radiusPoint t r z)))

theorem NavierStokes.TerminalHistoryBridge.terminal_axialResidual (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h p / OutgoingDilation.switchRadius F XR) + 1 / 5) : SimilarityProfile.partialZ (TerminalPressure.outgoingPressure (normalization F XR) F.data (shift F XR)) p = SimilarityProfile.q F.data.h p ^ (-TerminalPressure.amplitudeExponent F.data.h - 1) * axialResidual F XR w.coefficients (logPoint XR (SimilarityProfile.inner F.data.h p))

Vanishing constants at infinity, obtained from the actual moments

theorem NavierStokes.TerminalHistoryBridge.powerHistory_identity (F : OutgoingProfile.Profile) {XR X : ℝ} (hXR : 0 < XR) (hX : 0 < X) : (1 - F.data.h) * powerHistory F XR X = X * OutgoingDilation.powerH F XR X

theorem NavierStokes.TerminalHistoryBridge.logPoint_radius {XR : ℝ} (hXR : 0 < XR) (y η : ℝ) : logPoint XR (XR * Real.exp y, η) = (y, η)

theorem NavierStokes.TerminalHistoryBridge.angularHistory_eta_eq_logI (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) (y : ℝ) : deriv (fun (t : ℝ) => angularHistory F XR w.coefficients t (XR * Real.exp y)) η = XR * √(2 * XR) * etaDerivative (HeatSwitchCone.logI F XR w.coefficients) (y, η)

theorem NavierStokes.TerminalHistoryBridge.energyHistory_eta_eq_logS (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) (y : ℝ) : deriv (fun (t : ℝ) => energyHistory F XR w.coefficients t (XR * Real.exp y)) η = XR * etaDerivative (HeatSwitchCone.logS F XR w.coefficients) (y, η)

theorem NavierStokes.TerminalHistoryBridge.pressure_eta_eq_logPi (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) (y : ℝ) : deriv (fun (t : ℝ) => HeatedOutgoing.Pi F XR w.coefficients (XR * Real.exp y, t)) η = etaDerivative (HeatSwitchCone.logPi F XR w.coefficients) (y, η)

theorem NavierStokes.TerminalHistoryBridge.H_log_derivative (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) (y : ℝ) : XR * Real.exp y * deriv (fun (u : ℝ) => HeatedOutgoing.H F XR w.coefficients (u, η)) (XR * Real.exp y) = √(2 * XR) * Real.exp (y / 2) * (ProfileHistories.radialPartial (HeatSwitchCone.logE F XR w.coefficients) (y, η) + HeatSwitchCone.logE F XR w.coefficients (y, η) / 2)

theorem NavierStokes.TerminalHistoryBridge.thetaWeight_eq_moments (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) (y : ℝ) : thetaWeight F XR w.coefficients (y, η) = ((1 - F.data.h) * (angularHistory F XR w.coefficients η (XR * Real.exp y) - powerHistory F XR (XR * Real.exp y)) - StressAlgebra.axialExponent F.data.h * η * deriv (fun (t : ℝ) => angularHistory F XR w.coefficients t (XR * Real.exp y)) η - XR * Real.exp y * (HeatedOutgoing.H F XR w.coefficients (XR * Real.exp y, η) - OutgoingDilation.powerH F XR (XR * Real.exp y))) / CoordinateAlgebra.L F.data.h η - 2 * HeatedOutgoing.H F XR w.coefficients (XR * Real.exp y, η) + 2 * (XR * Real.exp y * deriv (fun (u : ℝ) => HeatedOutgoing.H F XR w.coefficients (u, η)) (XR * Real.exp y))

theorem NavierStokes.TerminalHistoryBridge.axialWeight_eq_moments (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) (y : ℝ) : axialWeight F XR w.coefficients (y, η) = (4 * F.data.h * η * energyHistory F XR w.coefficients η (XR * Real.exp y) - StressAlgebra.coordinateFactor η * deriv (fun (t : ℝ) => energyHistory F XR w.coefficients t (XR * Real.exp y)) η + 4 * StressAlgebra.velocityExponent F.data.h * η * (XR * Real.exp y * HeatedOutgoing.Pi F XR w.coefficients (XR * Real.exp y, η)) - StressAlgebra.coordinateFactor η * (XR * Real.exp y * deriv (fun (t : ℝ) => HeatedOutgoing.Pi F XR w.coefficients (XR * Real.exp y, t)) η)) / CoordinateAlgebra.L F.data.h η

theorem NavierStokes.TerminalHistoryBridge.thetaWeight_tendsto_zero (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) : Filter.Tendsto (fun (y : ℝ) => thetaWeight F XR w.coefficients (y, η)) Filter.atTop (nhds 0)

theorem NavierStokes.TerminalHistoryBridge.axialWeight_tendsto_zero (F : OutgoingProfile.Profile) {XR C B : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) : Filter.Tendsto (fun (y : ℝ) => axialWeight F XR w.coefficients (y, η)) Filter.atTop (nhds 0)

theorem NavierStokes.TerminalHistoryBridge.eta_mem_interior {h : ℝ} (hh : 0 < h) (hh' : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) : SimilarityProfile.eta h p ∈ Set.Ioo (-1) 1

theorem NavierStokes.TerminalHistoryBridge.full_switch_late (F : OutgoingProfile.Profile) {XR X : ℝ} (hXR : 0 < XR) (hX : 0 < X) (hfull : 1 / 2 ≤ Real.log (X / OutgoingDilation.switchRadius F XR) + 1 / 5) : TerminalCone.terminalStart F.data ≤ Real.log (X / XR)

theorem NavierStokes.TerminalHistoryBridge.full_switch_radial_strict {F : OutgoingProfile.Profile} {XR : ℝ} (hXR : 0 < XR) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h p / OutgoingDilation.switchRadius F XR) + 1 / 5) {u : ℝ} (hu : p.2.1 ≤ u) : 1 / 2 < Real.log (SimilarityProfile.X F.data.h (p.1, u, p.2.2) / OutgoingDilation.switchRadius F XR) + 1 / 5

noncomputable def NavierStokes.TerminalHistoryBridge.regularClock (q XR s : ℝ) : ℝ

Regular clock, given by Real.log ((s/q)/XR).

Equations

• NavierStokes.TerminalHistoryBridge.regularClock q XR s = Real.log (s / q / XR)

noncomputable def NavierStokes.TerminalHistoryBridge.radiusClock (q XR r : ℝ) : ℝ

Radius clock, given by regularClock q XR (r^2/2).

Equations

• NavierStokes.TerminalHistoryBridge.radiusClock q XR r = NavierStokes.TerminalHistoryBridge.regularClock q XR (r ^ 2 / 2)

theorem NavierStokes.TerminalHistoryBridge.regularClock_hasDerivAt {q XR s : ℝ} (hq : 0 < q) (hXR : 0 < XR) (hs : 0 < s) : HasDerivAt (regularClock q XR) (1 / s) s

theorem NavierStokes.TerminalHistoryBridge.radiusClock_hasDerivAt {q XR r : ℝ} (hq : 0 < q) (hXR : 0 < XR) (hr : 0 < r) : HasDerivAt (radiusClock q XR) (2 / r) r

theorem NavierStokes.TerminalHistoryBridge.exp_regularClock {q XR s : ℝ} (hq : 0 < q) (hXR : 0 < XR) (hs : 0 < s) : XR * Real.exp (regularClock q XR s) = s / q

theorem NavierStokes.TerminalHistoryBridge.regularClock_tendsto {q XR : ℝ} (hq : 0 < q) (hXR : 0 < XR) : Filter.Tendsto (regularClock q XR) Filter.atTop Filter.atTop

theorem NavierStokes.TerminalHistoryBridge.radiusClock_tendsto {q XR : ℝ} (hq : 0 < q) (hXR : 0 < XR) : Filter.Tendsto (radiusClock q XR) Filter.atTop Filter.atTop

theorem NavierStokes.TerminalHistoryBridge.sqrt_radius_quotient {q r : ℝ} (_hq : 0 < q) (hr : 0 < r) : √(2 * (r ^ 2 / 2 / q)) = r / √q

theorem NavierStokes.TerminalHistoryBridge.theta_power_identity {q : ℝ} (hq : 0 < q) (h : ℝ) : q ^ (-h) = q ^ (-TerminalPressure.amplitudeExponent h - 1) * q * √q

noncomputable def NavierStokes.TerminalHistoryBridge.physicalThetaWeight (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (t z r : ℝ) : ℝ

Physical theta weight as an element of ℝ.

Equations

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

noncomputable def NavierStokes.TerminalHistoryBridge.physicalAxialWeight (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (t z s : ℝ) : ℝ

Physical axial weight as an element of ℝ.

Equations

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

theorem NavierStokes.TerminalHistoryBridge.physicalThetaWeight_hasDerivAt (F : OutgoingProfile.Profile) {XR C t r z : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (ht : t < 1) (hr : 0 < r) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h (TerminalStress.radiusPoint t r z) / OutgoingDilation.switchRadius F XR) + 1 / 5) : HasDerivAt (physicalThetaWeight F XR w.coefficients t z) (-(r ^ 2 * TerminalStress.leadingResidual (normalization F XR) F.data.h (TerminalPressure.outgoingTaper F.data (shift F XR)) t r z)) r

theorem NavierStokes.TerminalHistoryBridge.physicalAxialWeight_hasDerivAt (F : OutgoingProfile.Profile) {XR C t s z : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (ht : t < 1) (hs : 0 < s) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h (t, s, z) / OutgoingDilation.switchRadius F XR) + 1 / 5) : HasDerivAt (physicalAxialWeight F XR w.coefficients t z) (-SimilarityProfile.partialZ (TerminalPressure.outgoingPressure (normalization F XR) F.data (shift F XR)) (t, s, z)) s

theorem NavierStokes.TerminalHistoryBridge.physicalThetaWeight_tendsto_zero (F : OutgoingProfile.Profile) {XR C t z : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (ht : t < 1) : Filter.Tendsto (physicalThetaWeight F XR w.coefficients t z) Filter.atTop (nhds 0)

theorem NavierStokes.TerminalHistoryBridge.physicalAxialWeight_tendsto_zero (F : OutgoingProfile.Profile) {XR C B t z : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) (ht : t < 1) : Filter.Tendsto (physicalAxialWeight F XR w.coefficients t z) Filter.atTop (nhds 0)

theorem NavierStokes.TerminalHistoryBridge.terminal_angular_integrable (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {t r z : ℝ} (ht : t < 1) (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * TerminalStress.leadingResidual C d.h (TerminalPressure.outgoingTaper d y0) t u z) (Set.Ioi r) MeasureTheory.volume

theorem NavierStokes.TerminalHistoryBridge.terminal_axial_integrable {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {t s z : ℝ} (ht : t < 1) (hs : 0 < s) : MeasureTheory.IntegrableOn (fun (u : ℝ) => SimilarityProfile.partialZ (TerminalPressure.outgoingPressure C d y0) (t, u, z)) (Set.Ioi s) MeasureTheory.volume

theorem NavierStokes.TerminalHistoryBridge.physicalThetaWeight_eq_tail (F : OutgoingProfile.Profile) {XR C t r z : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (ht : t < 1) (hr : 0 < r) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h (TerminalStress.radiusPoint t r z) / OutgoingDilation.switchRadius F XR) + 1 / 5) : physicalThetaWeight F XR w.coefficients t z r = ∫ (u : ℝ) in Set.Ioi r, u ^ 2 * TerminalStress.leadingResidual (normalization F XR) F.data.h (TerminalPressure.outgoingTaper F.data (shift F XR)) t u z

theorem NavierStokes.TerminalHistoryBridge.physicalAxialWeight_eq_tail (F : OutgoingProfile.Profile) {XR C B t s z : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) (ht : t < 1) (hs : 0 < s) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h (t, s, z) / OutgoingDilation.switchRadius F XR) + 1 / 5) : physicalAxialWeight F XR w.coefficients t z s = ∫ (u : ℝ) in Set.Ioi s, SimilarityProfile.partialZ (TerminalPressure.outgoingPressure (normalization F XR) F.data (shift F XR)) (t, u, z)

theorem NavierStokes.TerminalHistoryBridge.physical_forwardTheta_eq_terminal (F : OutgoingProfile.Profile) {XR C t r z : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (ht : t < 1) (hr : 0 < r) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h (TerminalStress.radiusPoint t r z) / OutgoingDilation.switchRadius F XR) + 1 / 5) : SimilarityProfile.q F.data.h (TerminalStress.radiusPoint t r z) ^ (-TerminalPressure.amplitudeExponent F.data.h - 1 / 2) * forwardTheta F XR w.coefficients (logPoint XR (SimilarityProfile.inner F.data.h (TerminalStress.radiusPoint t r z))) = TerminalStress.terminalStress (normalization F XR) F.data.h (TerminalPressure.outgoingTaper F.data (shift F XR)) t z r

The actual forward angular stress equals the independently defined backward physical stress. Its similarity factor is q^(-A-1/2).

theorem NavierStokes.TerminalHistoryBridge.physical_forwardAxial_eq_terminal (F : OutgoingProfile.Profile) {XR C B t r z : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) (ht : t < 1) (hr : 0 < r) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h (TerminalStress.radiusPoint t r z) / OutgoingDilation.switchRadius F XR) + 1 / 5) : SimilarityProfile.q F.data.h (TerminalStress.radiusPoint t r z) ^ (-TerminalPressure.amplitudeExponent F.data.h - 1 / 2) * forwardAxial F XR w.coefficients (logPoint XR (SimilarityProfile.inner F.data.h (TerminalStress.radiusPoint t r z))) = TerminalPressure.axialBackwardStress (normalization F XR) F.data.h (TerminalPressure.outgoingTaper F.data (shift F XR)) t z r

The same witness and the original zero-energy identity also fix the axial integration constant; the pressure is the actual canonical pressure.

theorem NavierStokes.TerminalHistoryBridge.normalized_inner (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (y : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : SimilarityProfile.q F.data.h (TerminalStress.radiusPoint (η ^ 2) (TerminalEdgeFactor.profileRadius (shift F XR) (TerminalCone.edgeDistance F y)) η) = 1 ∧ SimilarityProfile.inner F.data.h (TerminalStress.radiusPoint (η ^ 2) (TerminalEdgeFactor.profileRadius (shift F XR) (TerminalCone.edgeDistance F y)) η) = (XR * Real.exp y, η)

theorem NavierStokes.TerminalHistoryBridge.forward_stresses_eq_profile_interior (F : OutgoingProfile.Profile) {XR C B y η : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) (hy : TerminalCone.terminalStart F.data < y) (hη : η ∈ Set.Ioo (-1) 1) : forwardTheta F XR w.coefficients (y, η) = TerminalEdgeFactor.profileAngularStress (normalization F XR) F.data (shift F XR) (TerminalCone.profilePoint F y η) ∧ forwardAxial F XR w.coefficients (y, η) = TerminalEdgeFactor.profileAxialStress (normalization F XR) F.data (shift F XR) (TerminalCone.profilePoint F y η)

Exact profile stress agreement on the open parameter interval. The closed endpoints are handled below by the actual continuous representatives.

noncomputable def NavierStokes.TerminalHistoryBridge.closedLogDomain : Set (ℝ × ℝ)

Closed log domain, given by univ ×ˢ HeatedOutgoing.parameterDomain.

Equations

• NavierStokes.TerminalHistoryBridge.closedLogDomain = Set.univ ×ˢ NavierStokes.HeatedOutgoing.parameterDomain

theorem NavierStokes.TerminalHistoryBridge.controls_continuousOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContinuousOn (HeatSwitchCone.controls F w) HeatedOutgoing.parameterDomain

theorem NavierStokes.TerminalHistoryBridge.scalar_fields_continuousOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContinuousOn (HeatSwitchCone.logE F XR w.coefficients) closedLogDomain ∧ ContinuousOn (HeatSwitchCone.Qs F XR w.coefficients) closedLogDomain ∧ ContinuousOn (HeatSwitchCone.Ns F XR w.coefficients) closedLogDomain ∧ ContinuousOn (HeatSwitchCone.radialA F XR w.coefficients) closedLogDomain

theorem NavierStokes.TerminalHistoryBridge.forward_fields_continuousOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContinuousOn (forwardTheta F XR w.coefficients) closedLogDomain ∧ ContinuousOn (forwardAxial F XR w.coefficients) closedLogDomain

noncomputable def NavierStokes.TerminalHistoryBridge.terminalMap (F : OutgoingProfile.Profile) (p : ℝ × ℝ) : ℝ × ℝ

Terminal map, given by (p.2,OutgoingTail.tailEnd F.data-p.1).

Equations

• NavierStokes.TerminalHistoryBridge.terminalMap F p = (p.2, NavierStokes.OutgoingTail.tailEnd F.data - p.1)

theorem NavierStokes.TerminalHistoryBridge.terminalMap_continuous (F : OutgoingProfile.Profile) : Continuous (terminalMap F)

theorem NavierStokes.TerminalHistoryBridge.terminal_speed_continuousOn (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) : ContinuousOn (fun (p : ℝ × ℝ) => TerminalEdgeFactor.profileSpeed (normalization F XR) F.data (shift F XR) (terminalMap F p)) closedLogDomain

theorem NavierStokes.TerminalHistoryBridge.forward_stresses_eq_profile (F : OutgoingProfile.Profile) {XR C B y η : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) (hy : TerminalCone.terminalStart F.data ≤ y) (hη : η ∈ HeatedOutgoing.parameterDomain) : forwardTheta F XR w.coefficients (y, η) = TerminalEdgeFactor.profileAngularStress (normalization F XR) F.data (shift F XR) (TerminalCone.profilePoint F y η) ∧ forwardAxial F XR w.coefficients (y, η) = TerminalEdgeFactor.profileAxialStress (normalization F XR) F.data (shift F XR) (TerminalCone.profilePoint F y η) ∧ HeatSwitchCone.radialA F XR w.coefficients (y, η) = TerminalEdgeFactor.profileSpeed (normalization F XR) F.data (shift F XR) (TerminalCone.profilePoint F y η)

Joint closure in log radius and parameter includes the switch-attachment point and both parameter endpoints, without evaluating physical coordinates at the singular time t=1.

theorem NavierStokes.TerminalHistoryBridge.logSwirl_eq_profile (F : OutgoingProfile.Profile) {XR C y η : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (hy : TerminalCone.terminalStart F.data ≤ y) (hη : η ∈ HeatedOutgoing.parameterDomain) : HeatSwitchCone.logE F XR w.coefficients (y, η) / √(2 * XR * Real.exp y) = TerminalEdgeFactor.profileSwirlCoefficient (normalization F XR) F.data (shift F XR) (TerminalCone.profilePoint F y η)

theorem NavierStokes.TerminalHistoryBridge.normalP_eq_profile (F : OutgoingProfile.Profile) {XR C B y η : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) (hy : TerminalCone.terminalStart F.data ≤ y) (hη : η ∈ HeatedOutgoing.parameterDomain) : HeatSwitchCone.normalP F XR w.coefficients (y, η) = TerminalEdgeFactor.profileP (normalization F XR) F.data (shift F XR) (TerminalCone.profilePoint F y η)

theorem NavierStokes.TerminalHistoryBridge.terminal_forward_cone (F : OutgoingProfile.Profile) {XR C B y η : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) (hsmall : TerminalCone.SmallTail F.data) (hXR : TerminalCone.radiusThreshold F ≤ XR) (hy : TerminalCone.terminalStart F.data ≤ y) (hy' : y < OutgoingTail.tailEnd F.data) (hη : η ∈ HeatedOutgoing.parameterDomain) : HeatSwitchCone.TrueAt F XR w.coefficients (y, η) ∧ HeatSwitchCone.normalP F XR w.coefficients (y, η) = TerminalEdgeFactor.profileP (normalization F XR) F.data (shift F XR) (TerminalCone.profilePoint F y η) ∧ HeatSwitchCone.normalJ F XR w.coefficients (y, η) = TerminalEdgeFactor.profileJ (normalization F XR) F.data (shift F XR) (TerminalCone.profilePoint F y η)