The actual restore and five-row repair interval

The interval has fixed logarithmic coordinates [-8,-5]. Endpoint drift and the actual repair coefficients are the only perturbation parameters. All histories are recovered from the exact five-row match at the right end.

@[reducible, inline]

abbrev NavierStokes.RepairConeBounds.Point : Type

Point: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.RepairConeBounds.Point = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.RepairConeBounds.Coeff : Type

Coefficient: an abbreviation for FiveProfileMoments.Coeff.

Equations

• NavierStokes.RepairConeBounds.Coeff = NavierStokes.FiveProfileMoments.Coeff

@[reducible, inline]

abbrev NavierStokes.RepairConeBounds.Parameter : Type

Parameter: an abbreviation for ℝ × Coeff.

Equations

• NavierStokes.RepairConeBounds.Parameter = (ℝ × NavierStokes.RepairConeBounds.Coeff)

@[reducible, inline]

abbrev NavierStokes.RepairConeBounds.Control : Type

Control: an abbreviation for Parameter × Parameter.

Equations

• NavierStokes.RepairConeBounds.Control = (NavierStokes.RepairConeBounds.Parameter × NavierStokes.RepairConeBounds.Parameter)

@[reducible, inline]

abbrev NavierStokes.RepairConeBounds.Raw : Type

Raw: an abbreviation for Parameter × Point.

Equations

• NavierStokes.RepairConeBounds.Raw = (NavierStokes.RepairConeBounds.Parameter × NavierStokes.RepairConeBounds.Point)

noncomputable def NavierStokes.RepairConeBounds.window : Set Point

Window, given by Icc (-8) (-5) ×ˢ Icc (-1) 1.

Equations

• NavierStokes.RepairConeBounds.window = Set.Icc (-8) (-5) ×ˢ Set.Icc (-1) 1

noncomputable def NavierStokes.RepairConeBounds.freeU (F : OutgoingProfile.Profile) (z : Raw) : ℝ

Free U, constructed using 4.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.freeE (F : OutgoingProfile.Profile) (z : Raw) : ℝ

Free E, constructed using NominalProfile.idealAmplitude.

Equations

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

theorem NavierStokes.RepairConeBounds.freeU_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freeU F)

theorem NavierStokes.RepairConeBounds.freeE_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freeE F)

@[simp]

theorem NavierStokes.RepairConeBounds.freeU_zero (F : OutgoingProfile.Profile) (p : Point) : freeU F (0, p) = 4 * p.2

@[simp]

theorem NavierStokes.RepairConeBounds.freeE_zero (F : OutgoingProfile.Profile) (p : Point) : freeE F (0, p) = NominalProfile.idealAmplitude F p.2 * Real.exp (p.1 / 10)

theorem NavierStokes.RepairConeBounds.freeU_zero_clean (F : OutgoingProfile.Profile) {p : Point} (hp : p.1 ≤ 0) : freeU F (0, p) = F.logU p

theorem NavierStokes.RepairConeBounds.freeE_zero_clean (F : OutgoingProfile.Profile) {p : Point} (hp : p.1 ≤ 0) : freeE F (0, p) = F.logE p

noncomputable def NavierStokes.RepairConeBounds.rawPoint (z : Control × Point) : Raw

Raw point, given by (z.1.1, z.2).

Equations

• NavierStokes.RepairConeBounds.rawPoint z = (z.1.1, z.2)

noncomputable def NavierStokes.RepairConeBounds.value (f : Raw → ℝ) (z : Control × Point) : ℝ

Value, given by f (rawPoint z).

Equations

• NavierStokes.RepairConeBounds.value f z = f (NavierStokes.RepairConeBounds.rawPoint z)

noncomputable def NavierStokes.RepairConeBounds.radialJet (f : Raw → ℝ) (z : Control × Point) : ℝ

Radial jet, given by fderiv ℝ f (rawPoint z) (0, (1, 0)).

Equations

• NavierStokes.RepairConeBounds.radialJet f z = (fderiv ℝ f (NavierStokes.RepairConeBounds.rawPoint z)) (0, 1, 0)

noncomputable def NavierStokes.RepairConeBounds.parameterJet (f : Raw → ℝ) (z : Control × Point) : ℝ

Parameter jet, given by fderiv ℝ f (rawPoint z) (z.1.2, (0, 1)).

Equations

• NavierStokes.RepairConeBounds.parameterJet f z = (fderiv ℝ f (NavierStokes.RepairConeBounds.rawPoint z)) (z.1.2, 0, 1)

theorem NavierStokes.RepairConeBounds.rawPoint_contDiff : ContDiff ℝ (↑⊤) rawPoint

theorem NavierStokes.RepairConeBounds.value_contDiff {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (value f)

theorem NavierStokes.RepairConeBounds.radialJet_contDiff {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (radialJet f)

theorem NavierStokes.RepairConeBounds.parameterJet_contDiff {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (parameterJet f)

noncomputable def NavierStokes.RepairConeBounds.finitePrefix (f : Raw → ℝ) (z : Raw) : ℝ

Finite prefix, given by ∫ t in (-5 : ℝ)..z.2.1, f (z.1, (t, z.2.2)).

Equations

• NavierStokes.RepairConeBounds.finitePrefix f z = ∫ (t : ℝ) in -5..z.2.1, f (z.1, t, z.2.2)

theorem NavierStokes.RepairConeBounds.finitePrefix_contDiff {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (finitePrefix f)

noncomputable def NavierStokes.RepairConeBounds.freeM (F : OutgoingProfile.Profile) (z : Raw) : ℝ

Free M, given by OutgoingHistories.M F.data F.amp z.2 + finitePrefix (fun q => Real.exp q.2.1 * (freeU F q - F.logU q.2)) z.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.freeI (F : OutgoingProfile.Profile) (z : Raw) : ℝ

Free I, given by OutgoingHistories.I F.reset z.2 + finitePrefix (fun q => Real.exp (3 * q.2.1 / 2) * (freeE F q - F.logE q.2)) z.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.freeJ (F : OutgoingProfile.Profile) (z : Raw) : ℝ

Free J, constructed using OutgoingHistories.J.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.freeS (F : OutgoingProfile.Profile) (z : Raw) : ℝ

Free S, constructed using OutgoingHistories.S.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.freePi (F : OutgoingProfile.Profile) (z : Raw) : ℝ

Free pi, given by OutgoingHistories.Pi F.reset z.2 + (1 / 2 : ℝ) * finitePrefix (fun q => freeE F q ^ 2 - F.logE q.2 ^ 2) z.

Equations

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

theorem NavierStokes.RepairConeBounds.freeM_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freeM F)

theorem NavierStokes.RepairConeBounds.freeI_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freeI F)

theorem NavierStokes.RepairConeBounds.freeJ_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freeJ F)

theorem NavierStokes.RepairConeBounds.freeS_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freeS F)

theorem NavierStokes.RepairConeBounds.freePi_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freePi F)

theorem NavierStokes.RepairConeBounds.finitePrefix_zero {f : Raw → ℝ} {p : Point} (hp : p.1 ≤ 0) (hf : ∀ y ≤ 0, f (0, y, p.2) = 0) : finitePrefix f (0, p) = 0

theorem NavierStokes.RepairConeBounds.freeM_zero (F : OutgoingProfile.Profile) {p : Point} (hp : p.1 ≤ 0) : freeM F (0, p) = OutgoingHistories.M F.data F.amp p

theorem NavierStokes.RepairConeBounds.freeI_zero (F : OutgoingProfile.Profile) {p : Point} (hp : p.1 ≤ 0) : freeI F (0, p) = OutgoingHistories.I F.reset p

theorem NavierStokes.RepairConeBounds.freeJ_zero (F : OutgoingProfile.Profile) {p : Point} (hp : p.1 ≤ 0) : freeJ F (0, p) = OutgoingHistories.J F.reset F.amp p

theorem NavierStokes.RepairConeBounds.freeS_zero (F : OutgoingProfile.Profile) {p : Point} (hp : p.1 ≤ 0) : freeS F (0, p) = OutgoingHistories.S F.reset F.amp p

theorem NavierStokes.RepairConeBounds.freePi_zero (F : OutgoingProfile.Profile) {p : Point} (hp : p.1 ≤ 0) : freePi F (0, p) = OutgoingHistories.Pi F.reset p

theorem NavierStokes.RepairConeBounds.radialJet_hasDerivAt {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) (v : Control) (p : Point) : HasDerivAt (fun (y : ℝ) => value f (v, y, p.2)) (radialJet f (v, p)) p.1

theorem NavierStokes.RepairConeBounds.parameterJet_hasDerivAt {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) {g : ℝ → Parameter} {g' : Parameter} {eta : ℝ} (hg : HasDerivAt g g' eta) (y : ℝ) : HasDerivAt (fun (e : ℝ) => f (g e, y, e)) (parameterJet f ((g eta, g'), y, eta)) eta

theorem NavierStokes.RepairConeBounds.parameterJet_zero {f : Raw → ℝ} {g : Point → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) {p : Point} (he : ∀ (eta : ℝ), f (0, p.1, eta) = g (p.1, eta)) : parameterJet f (0, p) = OutgoingHistories.dEta g p

theorem NavierStokes.RepairConeBounds.radialJet_freeU_zero (F : OutgoingProfile.Profile) (p : Point) : radialJet (freeU F) (0, p) = 0

theorem NavierStokes.RepairConeBounds.radialJet_freeE_zero (F : OutgoingProfile.Profile) (p : Point) : radialJet (freeE F) (0, p) = value (freeE F) (0, p) / 10

noncomputable def NavierStokes.RepairConeBounds.endpointError {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (eta : ℝ) : ℝ

Endpoint error, given by c.initialAxial eta - 4 * eta.

Equations

• NavierStokes.RepairConeBounds.endpointError c eta = c.initialAxial eta - 4 * eta

noncomputable def NavierStokes.RepairConeBounds.dataParameter {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (eta : ℝ) : Parameter

Data parameter, given by (endpointError c eta, NominalProfile.resetCoefficients F c.debt eta).

Equations

• NavierStokes.RepairConeBounds.dataParameter c eta = (NavierStokes.RepairConeBounds.endpointError c eta, NavierStokes.NominalProfile.resetCoefficients F c.debt eta)

noncomputable def NavierStokes.RepairConeBounds.controls {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (eta : ℝ) : Control

Controls, given by (dataParameter c eta, (deriv (endpointError c) eta, deriv (NominalProfile.resetCoefficients F c.debt) eta)).

Equations

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

theorem NavierStokes.RepairConeBounds.dataParameter_hasDerivAt {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {eta : ℝ} (heta : eta ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt eta) : HasDerivAt (dataParameter c) (controls c eta).2 eta

theorem NavierStokes.RepairConeBounds.controls_norm {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {eps : ℝ} (hG : JetBounds.FiniteJetBound 1 (endpointError c) (Set.Icc (-1) 1) eps) (hc : JetBounds.FiniteJetBound 1 (NominalProfile.resetCoefficients F c.debt) (Set.Icc (-1) 1) eps) {eta : ℝ} (heta : eta ∈ Set.Icc (-1) 1) : ‖controls c eta‖ ≤ eps

theorem NavierStokes.RepairConeBounds.actual_fields {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) : c.normalizedU (Real.exp p.1, p.2) = freeU F (dataParameter c p.2, p) ∧ c.normalizedE (Real.exp p.1, p.2) = freeE F (dataParameter c p.2, p)

theorem NavierStokes.RepairConeBounds.integral_exp_Iic (f : ℝ → ℝ) (y : ℝ) : ∫ (x : ℝ) in Set.Ioc 0 (Real.exp y), f x = ∫ (t : ℝ) in Set.Iic y, Real.exp t * f (Real.exp t)

theorem NavierStokes.RepairConeBounds.image_exp_Ioc (a b : ℝ) : Real.exp '' Set.Ioc a b = Set.Ioc (Real.exp a) (Real.exp b)

theorem NavierStokes.RepairConeBounds.integral_exp_Ioc (f : ℝ → ℝ) {a b : ℝ} (hab : a ≤ b) : ∫ (x : ℝ) in Set.Ioc (Real.exp a) (Real.exp b), f x = ∫ (t : ℝ) in a..b, Real.exp t * f (Real.exp t)

noncomputable def NavierStokes.RepairConeBounds.logRows (F : OutgoingProfile.Profile) (p : Point) : Fin 5 → ℝ

Log rows as an element of Fin 5 → ℝ.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.freeRows (F : OutgoingProfile.Profile) (z : Raw) : Fin 5 → ℝ

Free rows, given by ![freeM F z, Real.sqrt 2 * freeI F z, Real.sqrt 2 * freeJ F z, freeS F z, freePi F z - F.axisDatum z.2.2].

Equations

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

theorem NavierStokes.RepairConeBounds.outgoing_moments_log (F : OutgoingProfile.Profile) (p : Point) : NominalProfile.moments F.U F.E (Real.exp p.1) p.2 = logRows F p

noncomputable def NavierStokes.RepairConeBounds.logDensity (U E y : ℝ) : Fin 5 → ℝ

Log density as an element of Fin 5 → ℝ.

Equations

• NavierStokes.RepairConeBounds.logDensity U E y = ![Real.exp y * U, √2 * Real.exp (3 * y / 2) * E, √2 * Real.exp (3 * y / 2) * E * U, Real.exp y * (U ^ 2 - E ^ 2 / 2), E ^ 2 / 2]

theorem NavierStokes.RepairConeBounds.density_comp_exp (U E : NominalProfile.Field) (y eta : ℝ) (i : Fin 5) : Real.exp y * NominalProfile.density (fun (x : ℝ) => U (x, eta)) (fun (x : ℝ) => E (x, eta)) (Real.exp y) i = logDensity (U (Real.exp y, eta)) (E (Real.exp y, eta)) y i

theorem NavierStokes.RepairConeBounds.freeRows_sub_logRows (F : OutgoingProfile.Profile) (z : Raw) (i : Fin 5) : freeRows F z i - logRows F z.2 i = ∫ (t : ℝ) in -5..z.2.1, logDensity (freeU F (z.1, t, z.2.2)) (freeE F (z.1, t, z.2.2)) t i - logDensity (F.logU (t, z.2.2)) (F.logE (t, z.2.2)) t i

theorem NavierStokes.RepairConeBounds.prefix_difference {f g : ℝ → ℝ} {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hf : MeasureTheory.IntegrableOn f (Set.Ioc 0 b) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (Set.Ioc 0 b) MeasureTheory.volume) (hmatch : ∫ (x : ℝ) in Set.Ioc 0 b, f x = ∫ (x : ℝ) in Set.Ioc 0 b, g x) : (∫ (x : ℝ) in Set.Ioc 0 a, f x) - ∫ (x : ℝ) in Set.Ioc 0 a, g x = -∫ (x : ℝ) in Set.Ioc a b, f x - g x

theorem NavierStokes.RepairConeBounds.normalized_density_integrable {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {eta : ℝ} (heta : eta ∈ ReferencePath.parameterInterval) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (x : ℝ) => NominalProfile.density (fun (t : ℝ) => c.normalizedU (t, eta)) (fun (t : ℝ) => c.normalizedE (t, eta)) x i) (Set.Ioc 0 NominalProfile.matchFraction) MeasureTheory.volume

theorem NavierStokes.RepairConeBounds.actual_moments {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : NominalProfile.moments c.normalizedU c.normalizedE (Real.exp p.1) p.2 = freeRows F (dataParameter c p.2, p)

Every stock is recovered backwards from the actual five-row match at the right endpoint. No estimate for the stocks is an input.

noncomputable def NavierStokes.RepairConeBounds.familyW (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family W as an element of ℝ.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.angularNumerator (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Angular numerator as an element of ℝ.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.familyQ (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family Q, given by angularNumerator F z / (Real.exp (3 * z.2.1 / 2) * value (freeE F) z).

Equations

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

noncomputable def NavierStokes.RepairConeBounds.familyN (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family N as an element of ℝ.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.radialNumerator (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Radial numerator, given by value (freeE F) z - 2 * radialJet (freeE F) z.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.familyA (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family A, given by radialNumerator F z / value (freeE F) z.

Equations

• NavierStokes.RepairConeBounds.familyA F z = NavierStokes.RepairConeBounds.radialNumerator F z / NavierStokes.RepairConeBounds.value (NavierStokes.RepairConeBounds.freeE F) z

noncomputable def NavierStokes.RepairConeBounds.familyB (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family B, given by -2 * radialJet (freeU F) z / value (freeE F) z.

Equations

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

noncomputable def NavierStokes.RepairConeBounds.familyP1 (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family P1, given by Real.exp z.2.1 * familyQ F z / NaturalAxisData.L F.data.h z.2.2.

Equations

• NavierStokes.RepairConeBounds.familyP1 F z = Real.exp z.2.1 * NavierStokes.RepairConeBounds.familyQ F z / NavierStokes.NaturalAxisData.L F.data.h z.2.2

noncomputable def NavierStokes.RepairConeBounds.familyP2 (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family P2, given by Real.exp z.2.1 * familyN F z / (NaturalAxisData.L F.data.h z.2.2 * value (freeE F) z).

Equations

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

noncomputable def NavierStokes.RepairConeBounds.familySpeed (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family speed, given by ActivationContinuation.shearSize (familyA F z) (familyB F z).

Equations

• NavierStokes.RepairConeBounds.familySpeed F z = NavierStokes.ActivationContinuation.shearSize (NavierStokes.RepairConeBounds.familyA F z) (NavierStokes.RepairConeBounds.familyB F z)

noncomputable def NavierStokes.RepairConeBounds.familyProjection (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family projection, given by ActivationContinuation.projection (familyP1 F z) (familyP2 F z) (familyA F z) (familyB F z).

Equations

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

theorem NavierStokes.RepairConeBounds.coordinateFactor_contDiff : ContDiff ℝ ↑⊤ fun (z : Control × Point) => StressAlgebra.coordinateFactor z.2.2

theorem NavierStokes.RepairConeBounds.L_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ ↑⊤ fun (z : Control × Point) => NaturalAxisData.L F.data.h z.2.2

theorem NavierStokes.RepairConeBounds.familyW_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (familyW F)

theorem NavierStokes.RepairConeBounds.angularNumerator_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (angularNumerator F)

theorem NavierStokes.RepairConeBounds.familyN_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (familyN F)

theorem NavierStokes.RepairConeBounds.radialNumerator_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (radialNumerator F)

noncomputable def NavierStokes.RepairConeBounds.regular (F : OutgoingProfile.Profile) : Set (Control × Point)

Regular, given by {z | value (freeE F) z ≠ 0 ∧ radialNumerator F z ≠ 0 ∧ NaturalAxisData.L F.data.h z.2.2 ≠ 0}.

Equations

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

theorem NavierStokes.RepairConeBounds.regular_isOpen (F : OutgoingProfile.Profile) : IsOpen (regular F)

theorem NavierStokes.RepairConeBounds.familyA_ne (F : OutgoingProfile.Profile) {z : Control × Point} (hz : z ∈ regular F) : familyA F z ≠ 0

theorem NavierStokes.RepairConeBounds.familyA_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyA F) (regular F)

theorem NavierStokes.RepairConeBounds.familyB_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyB F) (regular F)

theorem NavierStokes.RepairConeBounds.familyQ_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyQ F) (regular F)

theorem NavierStokes.RepairConeBounds.familyP1_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyP1 F) (regular F)

theorem NavierStokes.RepairConeBounds.familyP2_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyP2 F) (regular F)

theorem NavierStokes.RepairConeBounds.familySpeed_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familySpeed F) (regular F)

theorem NavierStokes.RepairConeBounds.familyProjection_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyProjection F) (regular F)

theorem NavierStokes.RepairConeBounds.familyW_zero (F : OutgoingProfile.Profile) {p : Point} (hp : p.1 ≤ 0) : familyW F (0, p) = OutgoingHistories.W F.data F.amp p

theorem NavierStokes.RepairConeBounds.familyQ_zero (F : OutgoingProfile.Profile) {p : Point} (hp : p.1 ≤ 0) : familyQ F (0, p) = OutgoingHistories.Qs F.reset F.amp p

theorem NavierStokes.RepairConeBounds.familyA_zero (F : OutgoingProfile.Profile) (p : Point) : familyA F (0, p) = 4 / 5

theorem NavierStokes.RepairConeBounds.familyB_zero (F : OutgoingProfile.Profile) (p : Point) : familyB F (0, p) = 0

theorem NavierStokes.RepairConeBounds.familySpeed_zero (F : OutgoingProfile.Profile) (p : Point) : familySpeed F (0, p) = 4 / 5

theorem NavierStokes.RepairConeBounds.familyProjection_zero (F : OutgoingProfile.Profile) {p : Point} (hp : p.1 ≤ 0) : familyProjection F (0, p) = Real.exp p.1 * OutgoingHistories.Qs F.reset F.amp p / NaturalAxisData.L F.data.h p.2

theorem NavierStokes.RepairConeBounds.zero_regular (F : OutgoingProfile.Profile) {p : Point} (hp : p ∈ window) : (0, p) ∈ regular F

theorem NavierStokes.RepairConeBounds.zero_projection_lower (F : OutgoingProfile.Profile) (hh : F.data.h ≤ 1 / 100) {p : Point} (hp : p ∈ window) : Real.exp (-8) ≤ familyProjection F (0, p)

noncomputable def NavierStokes.RepairConeBounds.observations (F : OutgoingProfile.Profile) (z : Control × Point) : Fin 22 → ℝ

All field jets and stock jets used in the actual integrated stresses.

Equations

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

theorem NavierStokes.RepairConeBounds.observations_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (observations F) (regular F)

theorem NavierStokes.RepairConeBounds.model_estimate (F : OutgoingProfile.Profile) : ∃ (r : ℝ) (L : ℝ), 0 < r ∧ 0 ≤ L ∧ ∀ (v : Control), ‖v‖ ≤ r → ∀ p ∈ window, (v, p) ∈ regular F ∧ ‖observations F (v, p) - observations F (0, p)‖ ≤ L * ‖v‖

theorem NavierStokes.RepairConeBounds.model_margins (F : OutgoingProfile.Profile) (hh : F.data.h ≤ 1 / 100) : ∃ (delta : ℝ), 0 < delta ∧ ∀ (v : Control), ‖v‖ ≤ delta → ∀ p ∈ window, 3 / 5 ≤ familyA F (v, p) ∧ familySpeed F (v, p) ≤ 1 ∧ Real.exp (-8) / 2 ≤ familyProjection F (v, p)

The tolerance depends on the fixed outgoing data. Neither an incoming axis stage nor its controls occur before this tolerance is chosen.

noncomputable def NavierStokes.RepairConeBounds.chart (R : ℝ) (p : Point) : Point

Chart, given by (R * Real.exp p.1, p.2).

Equations

• NavierStokes.RepairConeBounds.chart R p = (R * Real.exp p.1, p.2)

noncomputable def NavierStokes.RepairConeBounds.angularScale (R : ℝ) : ℝ

Angular scale, given by R * Real.sqrt R * Real.sqrt 2.

Equations

• NavierStokes.RepairConeBounds.angularScale R = R * √R * √2

theorem NavierStokes.RepairConeBounds.chart_mem {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {p : Point} (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : chart c.radius p ∈ c.admissibleDomain.carrier

theorem NavierStokes.RepairConeBounds.parameter_admissible_eventually {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {eta : ℝ} (heta : eta ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt eta) : ∀ᶠ (e : ℝ) in nhds eta, e ∈ ReferencePath.parameterInterval ∧ NominalProfile.SmallDebt F c.debt e

theorem NavierStokes.RepairConeBounds.physical_rows {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) (i : Fin 5) : ProfileHistories.primitive (fun (q : ProfileHistories.Point) => NominalProfile.regularDensity (c.profiles hsep) q i) (chart c.radius p) = NominalProfile.dilationFactor c.radius i * freeRows F (dataParameter c p.2, p) i

theorem NavierStokes.RepairConeBounds.physical_stock_values {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : (c.profiles hsep).M (chart c.radius p) = c.radius * value (freeM F) (controls c p.2, p) ∧ (c.profiles hsep).I (chart c.radius p) = angularScale c.radius * value (freeI F) (controls c p.2, p) ∧ (c.profiles hsep).J (chart c.radius p) = angularScale c.radius * value (freeJ F) (controls c p.2, p) ∧ (c.profiles hsep).S (chart c.radius p) = c.radius * value (freeS F) (controls c p.2, p) ∧ (c.profiles hsep).pressure (chart c.radius p) = value (freePi F) (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.parameter_of_germ {D : ProfileHistories.RadialDomain} {H : Point → ℝ} (hH : ContDiffOn ℝ (↑⊤) H D.carrier) {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {p : Point} (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) (s X : ℝ) (hp : (X, p.2) ∈ D.carrier) (he : (fun (eta : ℝ) => H (X, eta)) =ᶠ[nhds p.2] fun (eta : ℝ) => s * f (dataParameter c eta, p.1, eta)) : ProfileHistories.parameterPartial H (X, p.2) = s * parameterJet f (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.physical_stock_parameters {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : ProfileHistories.parameterPartial (c.profiles hsep).M (chart c.radius p) = c.radius * parameterJet (freeM F) (controls c p.2, p) ∧ ProfileHistories.parameterPartial (c.profiles hsep).I (chart c.radius p) = angularScale c.radius * parameterJet (freeI F) (controls c p.2, p) ∧ ProfileHistories.parameterPartial (c.profiles hsep).J (chart c.radius p) = angularScale c.radius * parameterJet (freeJ F) (controls c p.2, p) ∧ ProfileHistories.parameterPartial (c.profiles hsep).S (chart c.radius p) = c.radius * parameterJet (freeS F) (controls c p.2, p) ∧ ProfileHistories.parameterPartial (c.profiles hsep).pressure (chart c.radius p) = parameterJet (freePi F) (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.physical_field_values {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) : (c.profiles hsep).U (chart c.radius p) = value (freeU F) (controls c p.2, p) ∧ (c.profiles hsep).E (chart c.radius p) = value (freeE F) (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.sqrt_chart {R : ℝ} (hR : 0 < R) (y : ℝ) : √(2 * (R * Real.exp y)) = √(2 * R) * Real.exp (y / 2)

theorem NavierStokes.RepairConeBounds.angularScale_pos {R : ℝ} (hR : 0 < R) : 0 < angularScale R

theorem NavierStokes.RepairConeBounds.angular_weight_chart {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {R : ℝ} (hR : 0 < R) (p : Point) : (chart R p).1 * P.H (chart R p) = angularScale R * (Real.exp (3 * p.1 / 2) * P.E (chart R p))

theorem NavierStokes.RepairConeBounds.physical_transport {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : (c.profiles hsep).W F.data.h (chart c.radius p) = familyW F (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.physical_lags {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : (c.profiles hsep).angularLag F.data.h (chart c.radius p) = familyQ F (controls c p.2, p) ∧ (c.profiles hsep).axialLag F.data.h (chart c.radius p) = familyN F (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.physical_stocks {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : ReferenceBounds.p1 (c.profiles hsep) F.data.h (chart c.radius p) = c.radius * familyP1 F (controls c p.2, p) ∧ ReferenceBounds.p2 (c.profiles hsep) F.data.h (chart c.radius p) = c.radius * familyP2 F (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.physicalE_smoothAt {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) : ContDiffAt ℝ (↑⊤) P.E p

theorem NavierStokes.RepairConeBounds.derivative_eq_on_interval {f g : ℝ → ℝ} {dg a b y : ℝ} (hab : a < b) (hy : y ∈ Set.Icc a b) (hf : DifferentiableAt ℝ f y) (hg : HasDerivAt g dg y) (he : Set.EqOn f g (Set.Icc a b)) : deriv f y = dg

theorem NavierStokes.RepairConeBounds.physical_field_radials {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : deriv (fun (y : ℝ) => (c.profiles hsep).U (c.radius * Real.exp y, p.2)) p.1 = radialJet (freeU F) (controls c p.2, p) ∧ deriv (fun (y : ℝ) => (c.profiles hsep).E (c.radius * Real.exp y, p.2)) p.1 = radialJet (freeE F) (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.physical_field_parameters {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : ProfileHistories.parameterPartial (c.profiles hsep).U (chart c.radius p) = parameterJet (freeU F) (controls c p.2, p) ∧ ProfileHistories.parameterPartial (c.profiles hsep).E (chart c.radius p) = parameterJet (freeE F) (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.shear_dilation_cancel {r z f : ℝ} (hr : r ≠ 0) (hz : z ≠ 0) (hf : f ≠ 0) (X df : ℝ) : -2 * X * df / f = 1 - 2 * (r * (z * (1 / 2)) * f + r * z * (df * X)) / (r * z * f)

theorem NavierStokes.RepairConeBounds.physical_log_shears {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {R : ℝ} (hR : 0 < R) (p : Point) (hp : chart R p ∈ D.carrier) (hf : P.f (chart R p) ≠ 0) : ActivationContinuation.shearA P (chart R p) = 1 - 2 * deriv (fun (y : ℝ) => P.E (R * Real.exp y, p.2)) p.1 / P.E (chart R p) ∧ ActivationContinuation.shearB P (chart R p) = -2 * deriv (fun (y : ℝ) => P.U (R * Real.exp y, p.2)) p.1 / P.E (chart R p)

This chart identity uses actual radial derivatives and the square-root relation between the regular angular profile and the physical angular field.

theorem NavierStokes.RepairConeBounds.physical_shears {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : ActivationContinuation.shearA (c.profiles hsep) (chart c.radius p) = familyA F (controls c p.2, p) ∧ ActivationContinuation.shearB (c.profiles hsep) (chart c.radius p) = familyB F (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.physical_projection {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : ActivationContinuation.projection (ReferenceBounds.p1 (c.profiles hsep) F.data.h (chart c.radius p)) (ReferenceBounds.p2 (c.profiles hsep) F.data.h (chart c.radius p)) (ActivationContinuation.shearA (c.profiles hsep) (chart c.radius p)) (ActivationContinuation.shearB (c.profiles hsep) (chart c.radius p)) = c.radius * familyProjection F (controls c p.2, p)

noncomputable def NavierStokes.RepairConeBounds.actualObservations {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) (p : Point) : Fin 22 → ℝ

These are actual field values, first radial and parameter jets, five normalized histories and their parameter derivatives, and integrated cone coordinates. The projection is divided by the physical matching radius.

Equations

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

theorem NavierStokes.RepairConeBounds.actualObservations_eq {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hy : p.1 ∈ Set.Icc (-8) (-5)) (heta : p.2 ∈ ReferencePath.parameterInterval) (hs : NominalProfile.SmallDebt F c.debt p.2) : actualObservations c hsep p = observations F (controls c p.2, p)

theorem NavierStokes.RepairConeBounds.actual_observation_estimate (F : OutgoingProfile.Profile) : ∃ (r : ℝ) (L : ℝ), 0 < r ∧ 0 ≤ L ∧ ∀ (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)), ∀ eps ≤ r, JetBounds.FiniteJetBound 1 (endpointError c) (Set.Icc (-1) 1) eps → JetBounds.FiniteJetBound 1 (NominalProfile.resetCoefficients F c.debt) (Set.Icc (-1) 1) eps → ∀ p ∈ window, NominalProfile.SmallDebt F c.debt p.2 → ‖actualObservations c hsep p - observations F (0, p)‖ ≤ L * eps

A genuine uniform bound for the actual jets and stocks. Its constants are chosen before the incoming axis stage and before its controls.

theorem NavierStokes.RepairConeBounds.exists_repair_cone_log (F : OutgoingProfile.Profile) : ∃ (delta : ℝ) (R0 : ℝ), 0 < delta ∧ 0 < R0 ∧ ∀ (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)), JetBounds.FiniteJetBound 1 (endpointError c) (Set.Icc (-1) 1) delta → JetBounds.FiniteJetBound 1 (NominalProfile.resetCoefficients F c.debt) (Set.Icc (-1) 1) delta → R0 ≤ c.radius → ∀ p ∈ window, NominalProfile.SmallDebt F c.debt p.2 → ActivationContinuation.IsRelaxed (c.profiles hsep) F.data.h (chart c.radius p)

The radius and first-jet tolerance are fixed before every incoming axis stage and its matching controls. The input stocks are not hypotheses: they have already been reconstructed from exact five-row matching.

theorem NavierStokes.RepairConeBounds.exists_repair_cone (F : OutgoingProfile.Profile) : ∃ (delta : ℝ) (R0 : ℝ), 0 < delta ∧ 0 < R0 ∧ ∀ (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)), JetBounds.FiniteJetBound 1 (endpointError c) (Set.Icc (-1) 1) delta → JetBounds.FiniteJetBound 1 (NominalProfile.resetCoefficients F c.debt) (Set.Icc (-1) 1) delta → R0 ≤ c.radius → ∀ (p : Point), p.1 ∈ Set.Icc (c.radius * Real.exp (-8)) (c.radius * Real.exp (-5)) → p.2 ∈ Set.Icc (-1) 1 → NominalProfile.SmallDebt F c.debt p.2 → ActivationContinuation.IsRelaxed (c.profiles hsep) F.data.h p

Actual relaxed cone on the complete closed physical restore/repair annulus, with a tolerance and radius floor depending only on F.