The true cone after radial modulation

The error estimates below concern the genuine derivatives of the realized profiles. Their constants are obtained from the constructed periodic primitives on compact sets, independently of the modulation frequency.

Quantitative stock bounds from actual field and history data

The two stock maps below are the exact integrated lag formulas. Their Lipschitz constants are derived from smoothness and compactness on sets with positive angular field and radius. No stock error estimate is assumed.

@[reducible, inline]

abbrev NavierStokes.ModulatedStockBounds.StockData : Type

Stock data: an abbreviation for Fin 12 → ℝ.

Equations

• NavierStokes.ModulatedStockBounds.StockData = (Fin 12 → ℝ)

@[reducible, inline]

abbrev NavierStokes.ModulatedStockBounds.StockArgument : Type

Stock argument: an abbreviation for Point × StockData.

Equations

• NavierStokes.ModulatedStockBounds.StockArgument = (NavierStokes.ProfileHistories.Point × NavierStokes.ModulatedStockBounds.StockData)

noncomputable def NavierStokes.ModulatedStockBounds.profileData {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) : StockData

The field values followed by the actual five histories and their first parameter derivatives. Pressure includes its prescribed value on the axis.

Equations

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

noncomputable def NavierStokes.ModulatedStockBounds.stockMap (h : ℝ) (q : StockArgument) : ℝ × ℝ

Stock map as an element of ℝ × ℝ.

Equations

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

theorem NavierStokes.ModulatedStockBounds.profileData_coordinates {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (hf : P.f p ≠ 0) : stockMap h (p, profileData P p) = (ActivationStocks.profileStockOne P h p, ActivationStocks.profileStockTwo P h p)

theorem NavierStokes.ModulatedStockBounds.profileData_smooth {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) : ContDiffOn ℝ (↑⊤) (profileData P) D.carrier

noncomputable def NavierStokes.ModulatedStockBounds.stockDomain (h : ℝ) : Set StockArgument

Stock domain, given by {q | 0 < q.1.1 ∧ NaturalAxisData.L h q.1.2 ≠ 0 ∧ 0 < q.2 0}.

Equations

• NavierStokes.ModulatedStockBounds.stockDomain h = {q : NavierStokes.ModulatedStockBounds.StockArgument | 0 < q.1.1 ∧ NavierStokes.NaturalAxisData.L h q.1.2 ≠ 0 ∧ 0 < q.2 0}

theorem NavierStokes.ModulatedStockBounds.isOpen_stockDomain (h : ℝ) : IsOpen (stockDomain h)

theorem NavierStokes.ModulatedStockBounds.stockMap_smooth (h : ℝ) : ContDiffOn ℝ (↑⊤) (stockMap h) (stockDomain h)

noncomputable def NavierStokes.ModulatedStockBounds.dataSet (μ R : ℝ) : Set StockData

Data set, given by Metric.closedBall 0 R ∩ {z | μ ≤ z 0}.

Equations

• NavierStokes.ModulatedStockBounds.dataSet μ R = Metric.closedBall 0 R ∩ {z : NavierStokes.ModulatedStockBounds.StockData | μ ≤ z 0}

theorem NavierStokes.ModulatedStockBounds.isCompact_dataSet (μ R : ℝ) : IsCompact (dataSet μ R)

theorem NavierStokes.ModulatedStockBounds.convex_dataSet (μ R : ℝ) : Convex ℝ (dataSet μ R)

theorem NavierStokes.ModulatedStockBounds.stockMap_lipschitz_on_dataSet (h μ R : ℝ) (hμ : 0 < μ) {S : Set ProfileHistories.Point} (hS : IsCompact S) (hX : ∀ p ∈ S, 0 < p.1) (hL : ∀ p ∈ S, NaturalAxisData.L h p.2 ≠ 0) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ p ∈ S, ∀ z ∈ dataSet μ R, ∀ w ∈ dataSet μ R, ‖stockMap h (p, w) - stockMap h (p, z)‖ ≤ C * ‖w - z‖

Uniform Lipschitz continuity in all field/history data on a compact positive-radius set. Only the reference coefficients depend on position.

theorem NavierStokes.ModulatedStockBounds.stockMap_small_perturbation (h μ B : ℝ) (hμ : 0 < μ) {S : Set ProfileHistories.Point} (hS : IsCompact S) (hX : ∀ p ∈ S, 0 < p.1) (hL : ∀ p ∈ S, NaturalAxisData.L h p.2 ≠ 0) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ p ∈ S, ∀ (z w : StockData), ‖z‖ ≤ B → 2 * μ ≤ z 0 → ‖w - z‖ ≤ min 1 μ → μ ≤ w 0 ∧ ‖stockMap h (p, w) - stockMap h (p, z)‖ ≤ C * ‖w - z‖

A small data perturbation automatically retains a positive angular field, and its exact stock error is bounded linearly by the data error.

theorem NavierStokes.ModulatedStockBounds.profileData_error_bound {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (p : ProfileHistories.Point) {ε : ℝ} (hε : 0 ≤ ε) (hf : |P.f p - Q.f p| ≤ ε) (hU : |P.U p - Q.U p| ≤ ε) (hH : ∀ (r : StressActivation.HistoryRow), |StressActivation.profileHistory P r p - StressActivation.profileHistory Q r p| ≤ ε ∧ |ProfileHistories.parameterPartial (StressActivation.profileHistory P r) p - ProfileHistories.parameterPartial (StressActivation.profileHistory Q r) p| ≤ ε) : ‖profileData P p - profileData Q p‖ ≤ ε

Coordinatewise bounds on genuine field/history data give the required norm bound; all first history derivatives are actual parameter derivatives.

theorem NavierStokes.ModulatedStockBounds.profile_stocks_lipschitz {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) (h : ℝ) {S : Set ProfileHistories.Point} (hS : IsCompact S) (hSD : S ⊆ D.carrier) (hX : ∀ p ∈ S, 0 < p.1) (hL : ∀ p ∈ S, NaturalAxisData.L h p.2 ≠ 0) (hpos : ∀ p ∈ S, 0 < Q.f p) : ∃ (δ : ℝ) (C : ℝ), 0 < δ ∧ 0 ≤ C ∧ ∀ {D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D'), ∀ p ∈ S, p ∈ D'.carrier → ‖profileData P p - profileData Q p‖ ≤ δ → 0 < P.f p ∧ |ActivationStocks.profileStockOne P h p - ActivationStocks.profileStockOne Q h p| ≤ C * ‖profileData P p - profileData Q p‖ ∧ |ActivationStocks.profileStockTwo P h p - ActivationStocks.profileStockTwo Q h p| ≤ C * ‖profileData P p - profileData Q p‖

Uniform quantitative stability of both actual profile stocks, around a fixed smooth positive nominal profile on a compact set.

theorem NavierStokes.ModulatedStockBounds.profile_stocks_from_history_bounds {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) (h : ℝ) {S : Set ProfileHistories.Point} (hS : IsCompact S) (hSD : S ⊆ D.carrier) (hX : ∀ p ∈ S, 0 < p.1) (hL : ∀ p ∈ S, NaturalAxisData.L h p.2 ≠ 0) (hpos : ∀ p ∈ S, 0 < Q.f p) : ∃ (δ : ℝ) (C : ℝ), 0 < δ ∧ 0 ≤ C ∧ ∀ {D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D'), ∀ p ∈ S, p ∈ D'.carrier → ∀ (ε : ℝ), 0 ≤ ε → ε ≤ δ → |P.f p - Q.f p| ≤ ε → |P.U p - Q.U p| ≤ ε → (∀ (r : StressActivation.HistoryRow), |StressActivation.profileHistory P r p - StressActivation.profileHistory Q r p| ≤ ε ∧ |ProfileHistories.parameterPartial (StressActivation.profileHistory P r) p - ProfileHistories.parameterPartial (StressActivation.profileHistory Q r) p| ≤ ε) → 0 < P.f p ∧ |ActivationStocks.profileStockOne P h p - ActivationStocks.profileStockOne Q h p| ≤ C * ε ∧ |ActivationStocks.profileStockTwo P h p - ActivationStocks.profileStockTwo Q h p| ≤ C * ε

The actual stock difference is bounded linearly by a common bound for the two field values and the five history values/first parameter derivatives.

theorem NavierStokes.ModulatedStockBounds.profileHistory_first_jet_bound {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (r : StressActivation.HistoryRow) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hp' : p ∈ D'.carrier) {J : Set ℝ} {ε : ℝ} (hjet : JetBounds.FiniteJetBound 1 (fun (η : ℝ) => StressActivation.profileHistory P r (p.1, η) - StressActivation.profileHistory Q r (p.1, η)) J ε) (hη : p.2 ∈ J) : |StressActivation.profileHistory P r p - StressActivation.profileHistory Q r p| ≤ ε ∧ |ProfileHistories.parameterPartial (StressActivation.profileHistory P r) p - ProfileHistories.parameterPartial (StressActivation.profileHistory Q r) p| ≤ ε

A first parameter-jet bound on an actual history difference supplies exactly the value/derivative estimates used by the stock adapter.

theorem NavierStokes.ModulatedStockBounds.profile_stocks_rate {D D' : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) (h : ℝ) (P : ℝ → ProfileHistories.Profiles D') {S : Set ProfileHistories.Point} (hS : IsCompact S) (hSD : S ⊆ D.carrier) (hSD' : S ⊆ D'.carrier) (hX : ∀ p ∈ S, 0 < p.1) (hL : ∀ p ∈ S, NaturalAxisData.L h p.2 ≠ 0) (hpos : ∀ p ∈ S, 0 < Q.f p) (n₀ Cdata : ℝ) (hCdata : 0 ≤ Cdata) (hdata : ∀ (n : ℝ), n₀ ≤ n → 1 ≤ n → ∀ p ∈ S, |(P n).f p - Q.f p| ≤ Cdata / n ∧ |(P n).U p - Q.U p| ≤ Cdata / n ∧ ∀ (r : StressActivation.HistoryRow), |StressActivation.profileHistory (P n) r p - StressActivation.profileHistory Q r p| ≤ Cdata / n ∧ |ProfileHistories.parameterPartial (StressActivation.profileHistory (P n) r) p - ProfileHistories.parameterPartial (StressActivation.profileHistory Q r) p| ≤ Cdata / n) : ∃ (N : ℕ) (C : ℝ), 0 < N ∧ 0 ≤ C ∧ ∀ (n : ℝ), ↑N ≤ n → ∀ p ∈ S, 0 < (P n).f p ∧ |ActivationStocks.profileStockOne (P n) h p - ActivationStocks.profileStockOne Q h p| ≤ C / n ∧ |ActivationStocks.profileStockTwo (P n) h p - ActivationStocks.profileStockTwo Q h p| ≤ C / n

Actual field and five-row history estimates of order 1/n imply an eventual uniform 1/n estimate for both actual lag stocks. The integer threshold and the stock constant are conclusions.

noncomputable def NavierStokes.ModulatedCone.angularShear (E : ParametricModulation.RadialParameter → ℝ) (p : ParametricModulation.RadialParameter) : ℝ

The actual angular shear of an angular profile E.

Equations

• NavierStokes.ModulatedCone.angularShear E p = 1 - 2 * p.1 * deriv (fun (X : ℝ) => E (X, p.2)) p.1 / E p

noncomputable def NavierStokes.ModulatedCone.signedAxialShear (E U : ParametricModulation.RadialParameter → ℝ) (p : ParametricModulation.RadialParameter) : ℝ

The signed axial shear, in the C = -b convention of TrueConeLoop.

Equations

• NavierStokes.ModulatedCone.signedAxialShear E U p = -(2 * p.1 * deriv (fun (X : ℝ) => U (X, p.2)) p.1 / E p)

theorem NavierStokes.ModulatedCone.compact_periodic_bound {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (F : X × ℝ → ℝ) (hF : ContinuousOn F (K ×ˢ Set.univ)) (hperiod : ∀ x ∈ K, Function.Periodic (fun (θ : ℝ) => F (x, θ)) 1) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ x ∈ K, ∀ (θ : ℝ), |F (x, θ)| ≤ M

Compactness bounds a continuous periodic family at all real phases.

noncomputable def NavierStokes.ModulatedCone.slowRadial (Q : ParametricModulation.RadialParameter × ℝ → ℝ) (z : ParametricModulation.RadialParameter × ℝ) : ℝ

The slow radial derivative of a periodic primitive, with the phase held fixed.

Equations

• NavierStokes.ModulatedCone.slowRadial Q z = NavierStokes.RadialModulation.partialX (NavierStokes.ParametricModulation.asRadialPrimitive Q) (z.1.1, z.1.2, z.2)

theorem NavierStokes.ModulatedCone.slowRadial_smooth (Q : ParametricModulation.RadialParameter × ℝ → ℝ) (hQ : ContDiff ℝ (↑⊤) Q) : ContDiff ℝ (↑⊤) (slowRadial Q)

theorem NavierStokes.ModulatedCone.slowRadial_eq_deriv (Q : ParametricModulation.RadialParameter × ℝ → ℝ) (hQ : ContDiff ℝ (↑⊤) Q) (X η θ : ℝ) : slowRadial Q ((X, η), θ) = deriv (fun (x : ℝ) => Q ((x, η), θ)) X

theorem NavierStokes.ModulatedCone.slowRadial_periodic (Q : ParametricModulation.RadialParameter × ℝ → ℝ) (hQ : ContDiff ℝ (↑⊤) Q) (hperiod : ∀ (p : ParametricModulation.RadialParameter), Function.Periodic (fun (θ : ℝ) => Q (p, θ)) 1) (p : ParametricModulation.RadialParameter) : Function.Periodic (fun (θ : ℝ) => slowRadial Q (p, θ)) 1

Differentiation in the slow radius preserves phase periodicity.

noncomputable def NavierStokes.ModulatedCone.angularErrorFactor {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (z : ParametricModulation.RadialParameter × ℝ) : ℝ

Angular error factor, given by -2 * z.1.1 * slowRadial r.angularPrimitive z.

Equations

• NavierStokes.ModulatedCone.angularErrorFactor r z = -2 * z.1.1 * NavierStokes.ModulatedCone.slowRadial r.angularPrimitive z

noncomputable def NavierStokes.ModulatedCone.axialErrorFactor {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (E : ParametricModulation.RadialParameter → ℝ) (z : (ℝ × ParametricModulation.RadialParameter) × ℝ) : ℝ

A smooth error factor at inverse frequency zero.

Equations

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

theorem NavierStokes.ModulatedCone.signed_shear_factor (C D A n : ℝ) : -((-C + D / n) / Real.exp (A / n)) - C = 1 / n * (-C * A * StressActivation.meanExp (-(1 / n) * A) - D * Real.exp (-(1 / n) * A))

theorem NavierStokes.ModulatedCone.realized_shears_factor {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (E U : ParametricModulation.RadialParameter → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (n : ℝ) (hn : n ≠ 0) (p : ParametricModulation.RadialParameter) (hp : p ∈ K) (hX : p.1 ≠ 0) (hE0 : E p ≠ 0) (haNom : a p = angularShear E p) (hbNom : a p * m p = signedAxialShear E U p) : angularShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E n q.1 q.2) p - r.angularLoop (p, n * Real.log p.1) = 1 / n * angularErrorFactor r (p, n * Real.log p.1) ∧ signedAxialShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E n q.1 q.2) (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedU r E U n q.1 q.2) p - r.signedAxialLoop (p, n * Real.log p.1) = 1 / n * axialErrorFactor r E ((1 / n, p), n * Real.log p.1)

Exact factorization of both errors in genuine realized shears.

theorem NavierStokes.ModulatedCone.axialErrorFactor_continuousOn {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (E : ParametricModulation.RadialParameter → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) (haK : ∀ p ∈ K, 0 < a p) (hE0 : ∀ p ∈ K, E p ≠ 0) : ContinuousOn (axialErrorFactor r E) ((Set.Icc 0 1 ×ˢ K) ×ˢ Set.univ)

The axial error factor is continuous even at inverse frequency zero.

theorem NavierStokes.ModulatedCone.realized_shears_uniform_bound {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (E U : ParametricModulation.RadialParameter → ℝ) (hK : IsCompact K) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (haK : ∀ p ∈ K, 0 < a p) (hX : ∀ p ∈ K, p.1 ≠ 0) (hE0 : ∀ p ∈ K, E p ≠ 0) (haNom : ∀ p ∈ K, a p = angularShear E p) (hbNom : ∀ p ∈ K, a p * m p = signedAxialShear E U p) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℝ), 1 ≤ n → ∀ p ∈ K, |angularShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E n q.1 q.2) p - r.angularLoop (p, n * Real.log p.1)| ≤ C / n ∧ |signedAxialShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E n q.1 q.2) (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedU r E U n q.1 q.2) p - r.signedAxialLoop (p, n * Real.log p.1)| ≤ C / n

Both actual shears differ from their prescribed loop values by C/n. No derivative estimate for the modulated profiles is assumed.

@[reducible, inline]

abbrev NavierStokes.ModulatedCone.StockShearDatum : Type

The two stocks and two signed shears before conversion to (P,J,v).

Equations

• NavierStokes.ModulatedCone.StockShearDatum = ((ℝ × ℝ) × ℝ × ℝ)

noncomputable def NavierStokes.ModulatedCone.coneCoordinates (z : StockShearDatum) : UniformCone.ConeDatum

Cone coordinates, given by (z.1.1 + z.1.2 * (z.2.2 / z.2.1), z.1.2 - z.1.1 * (z.2.2 / z.2.1), z.2.1 * (1 + (z.2.2 / z.2.1) ^ 2)).

Equations

• NavierStokes.ModulatedCone.coneCoordinates z = (z.1.1 + z.1.2 * (z.2.2 / z.2.1), z.1.2 - z.1.1 * (z.2.2 / z.2.1), z.2.1 * (1 + (z.2.2 / z.2.1) ^ 2))

noncomputable def NavierStokes.ModulatedCone.stockShearCone : Set StockShearDatum

Stock shear cone, given by {z | TrueConeLoop.InTrueCone z.1.1 z.1.2 z.2.1 z.2.2}.

Equations

• NavierStokes.ModulatedCone.stockShearCone = {z : NavierStokes.ModulatedCone.StockShearDatum | NavierStokes.TrueConeLoop.InTrueCone z.1.1 z.1.2 z.2.1 z.2.2}

theorem NavierStokes.ModulatedCone.coneCoordinates_continuousAt {z : StockShearDatum} (hz : z.2.1 ≠ 0) : ContinuousAt coneCoordinates z

theorem NavierStokes.ModulatedCone.isOpen_stockShearCone : IsOpen stockShearCone

Openness is inherited from the already verified exact root cone.

theorem NavierStokes.ModulatedCone.compact_periodic_stockShear_stable {X : Type u_1} [TopologicalSpace X] (p₁ p₂ : X → ℝ) (A C : X × ℝ → ℝ) {K : Set X} (hK : IsCompact K) (hp₁ : ContinuousOn p₁ K) (hp₂ : ContinuousOn p₂ K) (hA : ContinuousOn A (K ×ˢ Set.univ)) (hC : ContinuousOn C (K ×ˢ Set.univ)) (hAp : ∀ x ∈ K, Function.Periodic (fun (θ : ℝ) => A (x, θ)) 1) (hCp : ∀ x ∈ K, Function.Periodic (fun (θ : ℝ) => C (x, θ)) 1) (hcone : ∀ x ∈ K, ∀ (θ : ℝ), TrueConeLoop.InTrueCone (p₁ x) (p₂ x) (A (x, θ)) (C (x, θ))) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ x ∈ K, ∀ (θ q₁ q₂ A' C' : ℝ), |q₁ - p₁ x| ≤ ρ → |q₂ - p₂ x| ≤ ρ → |A' - A (x, θ)| ≤ ρ → |C' - C (x, θ)| ≤ ρ → TrueConeLoop.InTrueCone q₁ q₂ A' C'

A compact periodic loop has a single tolerance in the original four coordinates, including stock errors and both shear errors.

theorem NavierStokes.ModulatedCone.realized_loop_stable {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (hK : IsCompact K) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₁ : ContDiff ℝ (↑⊤) p₁) (hp₂ : ContDiff ℝ (↑⊤) p₂) (haK : ∀ p ∈ K, 0 < a p) (hrelaxed : ∀ p ∈ K, TrueConeLoop.nominalSpeed (a p) (m p) < ConeAlgebra.coneBound (p₁ p + p₂ p * m p) (p₂ p - p₁ p * m p)) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ p ∈ K, ∀ (θ q₁ q₂ A' C' : ℝ), |q₁ - p₁ p| ≤ ρ → |q₂ - p₂ p| ≤ ρ → |A' - r.angularLoop (p, θ)| ≤ ρ → |C' - r.signedAxialLoop (p, θ)| ≤ ρ → TrueConeLoop.InTrueCone q₁ q₂ A' C'

The tolerance is available for the actual loop selected from nominal relaxed-cone data, without a true-cone assumption on those nominal shears.

theorem NavierStokes.ModulatedCone.exists_integer_frequency (C ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), 0 < N ∧ ∀ (n : ℕ), N ≤ n → 1 ≤ ↑n ∧ C / ↑n ≤ ε

One finite integer controls every later frequency.

theorem NavierStokes.ModulatedCone.realized_trueCone_of_stock_bound {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (E U : ParametricModulation.RadialParameter → ℝ) (hK : IsCompact K) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₁ : ContDiff ℝ (↑⊤) p₁) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (haK : ∀ p ∈ K, 0 < a p) (hX : ∀ p ∈ K, p.1 ≠ 0) (hE0 : ∀ p ∈ K, E p ≠ 0) (haNom : ∀ p ∈ K, a p = angularShear E p) (hbNom : ∀ p ∈ K, a p * m p = signedAxialShear E U p) (hrelaxed : ∀ p ∈ K, TrueConeLoop.nominalSpeed (a p) (m p) < ConeAlgebra.coneBound (p₁ p + p₂ p * m p) (p₂ p - p₁ p * m p)) (q₁ q₂ : ℝ → ParametricModulation.RadialParameter → ℝ) (Cstock : ℝ) (hstock : ∀ (n : ℝ), 1 ≤ n → ∀ p ∈ K, |q₁ n p - p₁ p| ≤ Cstock / n ∧ |q₂ n p - p₂ p| ≤ Cstock / n) : ∃ (N : ℕ), 0 < N ∧ ∀ (n : ℕ), N ≤ n → ∀ p ∈ K, TrueConeLoop.InTrueCone (q₁ (↑n) p) (q₂ (↑n) p) (angularShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E (↑n) q.1 q.2) p) (signedAxialShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E (↑n) q.1 q.2) (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedU r E U (↑n) q.1 q.2) p)

Interface for combining the derived shear bound with derived stock estimates. The actual history construction supplies hstock below.

theorem NavierStokes.ModulatedCone.quotient_perturbation_bound {μ M ε x y e f : ℝ} (hμ : 0 < μ) (hM : 0 ≤ M) (hε : 0 ≤ ε) (he : μ ≤ e) (hf : μ ≤ f) (hx : |x| ≤ M) (hxy : |y - x| ≤ ε) (hef : |f - e| ≤ ε) : |y / f - x / e| ≤ (1 / μ + M / (μ * μ)) * ε

Quotient perturbations controlled by a common positive denominator.

theorem NavierStokes.ModulatedCone.shear_perturbation_bound {μ R M ε X E₀ E₁ EX₀ EX₁ UX₀ UX₁ : ℝ} (hμ : 0 < μ) (hR : 0 ≤ R) (hM : 0 ≤ M) (hε : 0 ≤ ε) (hE₀ : μ ≤ E₀) (hE₁ : μ ≤ E₁) (hX : |X| ≤ R) (hEX : |EX₀| ≤ M) (hUX : |UX₀| ≤ M) (hEedit : |E₁ - E₀| ≤ ε) (hEXedit : |EX₁ - EX₀| ≤ ε) (hUXedit : |UX₁ - UX₀| ≤ ε) : |1 - 2 * X * EX₁ / E₁ - (1 - 2 * X * EX₀ / E₀)| ≤ 2 * R * (1 / μ + M / (μ * μ)) * ε ∧ |-(2 * X * UX₁ / E₁) - -(2 * X * UX₀ / E₀)| ≤ 2 * R * (1 / μ + M / (μ * μ)) * ε

A small edit in field value and first radial derivatives produces a small edit in both genuine shear quotients.

theorem NavierStokes.ModulatedCone.shears_eq_on_open {E U F V : ParametricModulation.RadialParameter → ℝ} {O : Set ParametricModulation.RadialParameter} (hO : IsOpen O) (hE : Set.EqOn E F O) (hU : Set.EqOn U V O) {p : ParametricModulation.RadialParameter} (hp : p ∈ O) : angularShear E p = angularShear F p ∧ signedAxialShear E U p = signedAxialShear F V p

Equality on an open collar includes equality of the actual shears.

noncomputable def NavierStokes.ModulatedCone.radialDerivative (E : ParametricModulation.RadialParameter → ℝ) (p : ParametricModulation.RadialParameter) : ℝ

The genuine derivative with the parameter held fixed.

Equations

• NavierStokes.ModulatedCone.radialDerivative E p = deriv (fun (X : ℝ) => E (X, p.2)) p.1

theorem NavierStokes.ModulatedCone.radialDerivative_smooth (E : ParametricModulation.RadialParameter → ℝ) (hE : ContDiff ℝ (↑⊤) E) : ContDiff ℝ (↑⊤) (radialDerivative E)

theorem NavierStokes.ModulatedCone.compact_shear_perturbation (E U : ParametricModulation.RadialParameter → ℝ) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) {S : Set ParametricModulation.RadialParameter} (hS : IsCompact S) (hpos : ∀ p ∈ S, 0 < E p) : ∃ (δ : ℝ) (C : ℝ), 0 < δ ∧ 0 ≤ C ∧ ∀ (F V : ParametricModulation.RadialParameter → ℝ) (ε : ℝ), 0 ≤ ε → ε ≤ δ → (∀ p ∈ S, |F p - E p| ≤ ε ∧ |radialDerivative F p - radialDerivative E p| ≤ ε ∧ |radialDerivative V p - radialDerivative U p| ≤ ε) → ∀ p ∈ S, δ ≤ F p ∧ |angularShear F p - angularShear E p| ≤ C * ε ∧ |signedAxialShear F V p - signedAxialShear E U p| ≤ C * ε

Compact smooth positive nominal fields have a uniform C¹-to-shear estimate. The positive denominator after the edit is a conclusion.

theorem NavierStokes.ModulatedCone.realized_profiles_boundary_shears {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (E U : ParametricModulation.RadialParameter → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hBK : B ⊆ K) : ∃ (O : Set ParametricModulation.RadialParameter), IsOpen O ∧ B ⊆ O ∧ ∀ (n : ℝ), ∀ p ∈ O, ParametricModulation.realizedE r E n p.1 p.2 = E p ∧ ParametricModulation.realizedU r E U n p.1 p.2 = U p ∧ angularShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E n q.1 q.2) p = angularShear E p ∧ signedAxialShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E n q.1 q.2) (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedU r E U n q.1 q.2) p = signedAxialShear E U p

The primitive construction preserves a single open collar for the values and the genuine radial shears, at every frequency.

theorem NavierStokes.ModulatedCone.shears_eq_of_radial_eventuallyEq {E U F V : ParametricModulation.RadialParameter → ℝ} {p : ParametricModulation.RadialParameter} (hE : (fun (X : ℝ) => E (X, p.2)) =ᶠ[nhds p.1] fun (X : ℝ) => F (X, p.2)) (hU : (fun (X : ℝ) => U (X, p.2)) =ᶠ[nhds p.1] fun (X : ℝ) => V (X, p.2)) : angularShear E p = angularShear F p ∧ signedAxialShear E U p = signedAxialShear F V p

Local agreement along the radial variable suffices for exact shear agreement.

theorem NavierStokes.ModulatedCone.nominal_stockShear_stable (a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ) {S : Set ParametricModulation.RadialParameter} (hS : IsCompact S) (ha : ContinuousOn a S) (hm : ContinuousOn m S) (hp₁ : ContinuousOn p₁ S) (hp₂ : ContinuousOn p₂ S) (hcone : ∀ p ∈ S, TrueConeLoop.InTrueCone (p₁ p) (p₂ p) (a p) (a p * m p)) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ p ∈ S, ∀ (q₁ q₂ A' C' : ℝ), |q₁ - p₁ p| ≤ ρ → |q₂ - p₂ p| ≤ ρ → |A' - a p| ≤ ρ → |C' - a p * m p| ≤ ρ → TrueConeLoop.InTrueCone q₁ q₂ A' C'

The same four-coordinate tolerance applies to an ordinary compact nominal true-cone patch (the constant periodic-loop case).

theorem NavierStokes.ModulatedCone.repaired_trueCone_of_bounds {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (E U : ParametricModulation.RadialParameter → ℝ) (hK : IsCompact K) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₁ : ContDiff ℝ (↑⊤) p₁) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (haK : ∀ p ∈ K, 0 < a p) (hX : ∀ p ∈ K, p.1 ≠ 0) (hE0 : ∀ p ∈ K, E p ≠ 0) (haNom : ∀ p ∈ K, a p = angularShear E p) (hbNom : ∀ p ∈ K, a p * m p = signedAxialShear E U p) (hrelaxed : ∀ p ∈ K, TrueConeLoop.nominalSpeed (a p) (m p) < ConeAlgebra.coneBound (p₁ p + p₂ p * m p) (p₂ p - p₁ p * m p)) (S : Set ParametricModulation.RadialParameter) (hS : IsCompact S) (hSpos : ∀ p ∈ S, 0 < E p) (haS : ∀ p ∈ S, a p = angularShear E p) (hbS : ∀ p ∈ S, a p * m p = signedAxialShear E U p) (hScone : ∀ p ∈ S, TrueConeLoop.InTrueCone (p₁ p) (p₂ p) (a p) (a p * m p)) (F V q₁ q₂ : ℕ → ParametricModulation.RadialParameter → ℝ) (n₀ : ℕ) (Cstock Cedit : ℝ) (hCedit : 0 ≤ Cedit) (hstock : ∀ (n : ℕ), n₀ ≤ n → 1 ≤ ↑n → ∀ p ∈ K ∪ S, |q₁ n p - p₁ p| ≤ Cstock / ↑n ∧ |q₂ n p - p₂ p| ≤ Cstock / ↑n) (hedit : ∀ (n : ℕ), n₀ ≤ n → 1 ≤ ↑n → ∀ p ∈ S, |F n p - E p| ≤ Cedit / ↑n ∧ |radialDerivative (F n) p - radialDerivative E p| ≤ Cedit / ↑n ∧ |radialDerivative (V n) p - radialDerivative U p| ≤ Cedit / ↑n) (hlocal : ∀ (n : ℕ), n₀ ≤ n → ∀ p ∈ K, ((fun (X : ℝ) => F n (X, p.2)) =ᶠ[nhds p.1] fun (X : ℝ) => ParametricModulation.realizedE r E (↑n) X p.2) ∧ (fun (X : ℝ) => V n (X, p.2)) =ᶠ[nhds p.1] fun (X : ℝ) => ParametricModulation.realizedU r E U (↑n) X p.2) : ∃ (N : ℕ), 0 < N ∧ ∀ (n : ℕ), N ≤ n → ∀ p ∈ K ∪ S, TrueConeLoop.InTrueCone (q₁ n p) (q₂ n p) (angularShear (F n) p) (signedAxialShear (F n) (V n) p)

Composition interface for the actual following repair. The modulation region uses its derived shear estimate, while a nominal true-cone patch uses the derived C¹ perturbation estimate. Later the actual history and moment construction supplies the stock/edit bounds and the local equality premise.

noncomputable def NavierStokes.ModulatedCone.Localized.historyIndex : StressActivation.HistoryRow → Fin 5

History index as an element of HistoryRow → Fin 5 | .mass => 0 | .angular => 1 | .transport => 2 | .energy => 3 | .pressure => 4.

Equations

• NavierStokes.ModulatedCone.Localized.historyIndex NavierStokes.StressActivation.HistoryRow.mass = 0
• NavierStokes.ModulatedCone.Localized.historyIndex NavierStokes.StressActivation.HistoryRow.angular = 1
• NavierStokes.ModulatedCone.Localized.historyIndex NavierStokes.StressActivation.HistoryRow.transport = 2
• NavierStokes.ModulatedCone.Localized.historyIndex NavierStokes.StressActivation.HistoryRow.energy = 3
• NavierStokes.ModulatedCone.Localized.historyIndex NavierStokes.StressActivation.HistoryRow.pressure = 4

theorem NavierStokes.ModulatedCone.Localized.profileHistory_eq_row {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (row : StressActivation.HistoryRow) (p : ProfileHistories.Point) : StressActivation.profileHistory P row p = ModulatedHistories.profileRows P p (historyIndex row)

theorem NavierStokes.ModulatedCone.Localized.fields_uniform_bound {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (J : Set ℝ) (hJ : IsCompact J) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℝ), 1 ≤ n → ∀ (X η : ℝ), η ∈ J → |ModulatedHistories.localizedF W r f n (X, η) - f (X, η)| ≤ C / n ∧ |ModulatedHistories.localizedU W r E U n (X, η) - U (X, η)| ≤ C / n

Localization preserves the uniform field-value estimate, including at all points outside the modulation window.

theorem NavierStokes.ModulatedCone.Localized.profileHistory_difference {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D D' : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (n : ℝ) (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hPf : P.f = ModulatedHistories.localizedF W r f n) (hPU : P.U = ModulatedHistories.localizedU W r E U n) (hQf : Q.f = f) (hQU : Q.U = U) (hP0 : P.pressure0 = Q.pressure0) (row : StressActivation.HistoryRow) (p : ProfileHistories.Point) (hX : 0 ≤ p.1) : StressActivation.profileHistory P row p - StressActivation.profileHistory Q row p = ModulatedHistories.historyDifference W r f E U n p.1 p.2 (historyIndex row)

Each actual localized profile history has the constructed integral difference; the pressure constant is retained exactly.

theorem NavierStokes.ModulatedCone.Localized.profileHistory_uniform_bound {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D D' : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (P : ℝ → ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hPf : ∀ (n : ℝ), (P n).f = ModulatedHistories.localizedF W r f n) (hPU : ∀ (n : ℝ), (P n).U = ModulatedHistories.localizedU W r E U n) (hQf : Q.f = f) (hQU : Q.U = U) (hP0 : ∀ (n : ℝ), (P n).pressure0 = Q.pressure0) (J : Set ℝ) (hJ : IsCompact J) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℝ), 1 ≤ n → ∀ (p : ProfileHistories.Point), 0 ≤ p.1 → p.2 ∈ J → p ∈ D.carrier → p ∈ D'.carrier → ∀ (row : StressActivation.HistoryRow), |StressActivation.profileHistory (P n) row p - StressActivation.profileHistory Q row p| ≤ C / n ∧ |ProfileHistories.parameterPartial (StressActivation.profileHistory (P n) row) p - ProfileHistories.parameterPartial (StressActivation.profileHistory Q row) p| ≤ C / n

Actual localized history values and their first parameter derivatives have one frequency-independent C/n bound.

theorem NavierStokes.ModulatedCone.Localized.profile_stocks_rate {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D D' : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (P : ℝ → ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hPf : ∀ (n : ℝ), (P n).f = ModulatedHistories.localizedF W r f n) (hPU : ∀ (n : ℝ), (P n).U = ModulatedHistories.localizedU W r E U n) (hQf : Q.f = f) (hQU : Q.U = U) (hP0 : ∀ (n : ℝ), (P n).pressure0 = Q.pressure0) (J : Set ℝ) (hJ : IsCompact J) (T : Set ProfileHistories.Point) (hT : IsCompact T) (hTJ : ∀ p ∈ T, p.2 ∈ J) (hTD : T ⊆ D.carrier) (hTD' : T ⊆ D'.carrier) (h : ℝ) (hX : ∀ p ∈ T, 0 < p.1) (hL : ∀ p ∈ T, NaturalAxisData.L h p.2 ≠ 0) (hpos : ∀ p ∈ T, 0 < Q.f p) : ∃ (N : ℕ) (C : ℝ), 0 < N ∧ 0 ≤ C ∧ ∀ (n : ℝ), ↑N ≤ n → ∀ p ∈ T, 0 < (P n).f p ∧ |ActivationStocks.profileStockOne (P n) h p - ActivationStocks.profileStockOne Q h p| ≤ C / n ∧ |ActivationStocks.profileStockTwo (P n) h p - ActivationStocks.profileStockTwo Q h p| ≤ C / n

The actual stocks of the localized modulation have a uniform C/n bound, derived from its actual axis-integrated histories.

theorem NavierStokes.ModulatedCone.Localized.splice_eventuallyEq (W : ModulatedHistories.Window) (base actual : ProfileHistories.Field) {p : ProfileHistories.Point} (hp : p.1 ∈ Set.Icc W.left W.right) (hleft : p.1 = W.left → actual =ᶠ[nhds p] base) (hright : p.1 = W.right → actual =ᶠ[nhds p] base) : ModulatedHistories.splice W base actual =ᶠ[nhds p] actual

theorem NavierStokes.ModulatedCone.Localized.raw_agreement {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hBK : B ⊆ K) (J : Set ℝ) (hends : ∀ η ∈ J, (W.left, η) ∈ B ∧ (W.right, η) ∈ B) (n : ℝ) {p : ProfileHistories.Point} (hp : p.1 ∈ Set.Icc W.left W.right) (hη : p.2 ∈ J) : ModulatedHistories.localizedF W r f n =ᶠ[nhds p] ModulatedHistories.rawF r f n ∧ ModulatedHistories.localizedU W r E U n =ᶠ[nhds p] ModulatedHistories.rawU r E U n

The endpoint collars make the localized functions locally equal to the raw modulated functions even at both endpoints of the closed window.

theorem NavierStokes.ModulatedCone.Localized.physical_profile_germs {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hBK : B ⊆ K) (J : Set ℝ) (hends : ∀ η ∈ J, (W.left, η) ∈ B ∧ (W.right, η) ∈ B) (n : ℝ) (P : ProfileHistories.Profiles D) (hPf : P.f = ModulatedHistories.localizedF W r f n) (hPU : P.U = ModulatedHistories.localizedU W r E U n) {p : ProfileHistories.Point} (hp : p.1 ∈ Set.Icc W.left W.right) (hη : p.2 ∈ J) (hphys : E =ᶠ[nhds p] fun (q : ProfileHistories.Point) => √(2 * q.1) * f q) : (P.E =ᶠ[nhds p] fun (q : ProfileHistories.Point) => ParametricModulation.realizedE r E n q.1 q.2) ∧ P.U =ᶠ[nhds p] fun (q : ProfileHistories.Point) => ParametricModulation.realizedU r E U n q.1 q.2

The actual localized physical fields agree locally with the raw realized fields, including at the boundary collars.

theorem NavierStokes.ModulatedCone.Localized.physical_shears_match {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hBK : B ⊆ K) (J : Set ℝ) (hends : ∀ η ∈ J, (W.left, η) ∈ B ∧ (W.right, η) ∈ B) (n : ℝ) (P : ProfileHistories.Profiles D) (hPf : P.f = ModulatedHistories.localizedF W r f n) (hPU : P.U = ModulatedHistories.localizedU W r E U n) {p : ProfileHistories.Point} (hp : p.1 ∈ Set.Icc W.left W.right) (hη : p.2 ∈ J) (hphys : E =ᶠ[nhds p] fun (q : ProfileHistories.Point) => √(2 * q.1) * f q) : angularShear P.E p = angularShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E n q.1 q.2) p ∧ signedAxialShear P.E P.U p = signedAxialShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E n q.1 q.2) (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedU r E U n q.1 q.2) p

Both shears of the actual localized physical profiles equal the already estimated realized shears, including at the boundary collars.

theorem NavierStokes.ModulatedCone.Localized.profiles_trueCone {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D D' : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (hK : IsCompact K) (hKW : ∀ p ∈ K, p.1 ∈ Set.Icc W.left W.right) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₁ : ContDiff ℝ (↑⊤) p₁) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (haK : ∀ p ∈ K, 0 < a p) (haNom : ∀ p ∈ K, a p = angularShear E p) (hbNom : ∀ p ∈ K, a p * m p = signedAxialShear E U p) (hrelaxed : ∀ p ∈ K, TrueConeLoop.nominalSpeed (a p) (m p) < ConeAlgebra.coneBound (p₁ p + p₂ p * m p) (p₂ p - p₁ p * m p)) (P : ℝ → ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hPf : ∀ (n : ℝ), (P n).f = ModulatedHistories.localizedF W r f n) (hPU : ∀ (n : ℝ), (P n).U = ModulatedHistories.localizedU W r E U n) (hQf : Q.f = f) (hQU : Q.U = U) (hP0 : ∀ (n : ℝ), (P n).pressure0 = Q.pressure0) (J : Set ℝ) (hJ : IsCompact J) (hKJ : ∀ p ∈ K, p.2 ∈ J) (hKD : K ⊆ D.carrier) (hKD' : K ⊆ D'.carrier) (h : ℝ) (hL : ∀ p ∈ K, NaturalAxisData.L h p.2 ≠ 0) (hpos : ∀ p ∈ K, 0 < Q.f p) (hstock₁ : ∀ p ∈ K, p₁ p = ActivationStocks.profileStockOne Q h p) (hstock₂ : ∀ p ∈ K, p₂ p = ActivationStocks.profileStockTwo Q h p) (hBK : B ⊆ K) (hends : ∀ η ∈ J, (W.left, η) ∈ B ∧ (W.right, η) ∈ B) (hphys : ∀ p ∈ K, E =ᶠ[nhds p] fun (q : ParametricModulation.RadialParameter) => √(2 * q.1) * f q) : ∃ (N : ℕ), 0 < N ∧ ∀ (n : ℕ), N ≤ n → ∀ p ∈ K, 0 < (P ↑n).f p ∧ TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne (P ↑n) h p) (ActivationStocks.profileStockTwo (P ↑n) h p) (angularShear (P ↑n).E p) (signedAxialShear (P ↑n).E (P ↑n).U p)

A finite integer frequency puts the actual localized profiles, with their actual axis-integrated stresses, in the true cone throughout the closed modulation window. All error bounds are derived in this theorem.

theorem NavierStokes.ModulatedCone.Localized.after_window_agreement {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (hBK : B ⊆ K) (J : Set ℝ) (hends : ∀ η ∈ J, (W.left, η) ∈ B ∧ (W.right, η) ∈ B) (n : ℝ) {p : ProfileHistories.Point} (hp : W.right ≤ p.1) (hη : p.2 ∈ J) : ModulatedHistories.localizedF W r f n =ᶠ[nhds p] f ∧ ModulatedHistories.localizedU W r E U n =ᶠ[nhds p] U

theorem NavierStokes.ModulatedCone.Localized.physical_after_window_agreement {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (hBK : B ⊆ K) (J : Set ℝ) (hends : ∀ η ∈ J, (W.left, η) ∈ B ∧ (W.right, η) ∈ B) (n : ℝ) (P : ProfileHistories.Profiles D) (hPf : P.f = ModulatedHistories.localizedF W r f n) (hPU : P.U = ModulatedHistories.localizedU W r E U n) {p : ProfileHistories.Point} (hp : W.right ≤ p.1) (hη : p.2 ∈ J) (hphys : E =ᶠ[nhds p] fun (q : ProfileHistories.Point) => √(2 * q.1) * f q) : P.E =ᶠ[nhds p] E ∧ P.U =ᶠ[nhds p] U

theorem NavierStokes.ModulatedCone.Localized.exists_profile_family {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (P0 : ℝ → ℝ) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (hP0 : ContDiff ℝ (↑⊤) P0) (J : Set ℝ) (hBK : B ⊆ K) (hends : ∀ η ∈ J, (W.left, η) ∈ B ∧ (W.right, η) ∈ B) : ∃ (Ω : Set ℝ) (hΩ : IsOpen Ω), J ⊆ Ω ∧ ∃ (P : ℝ → ProfileHistories.Profiles (ModulatedHistories.stripDomain Ω hΩ)), (∀ (n : ℝ), (P n).f = ModulatedHistories.localizedF W r f n ∧ (P n).U = ModulatedHistories.localizedU W r E U n ∧ (P n).pressure0 = P0) ∧ ∃ (V : Set ProfileHistories.Point), IsOpen V ∧ B ⊆ V ∧ ∀ (n : ℝ), ∀ p ∈ V, (P n).f p = f p ∧ (P n).U p = U p

The localized Profiles family used by the cone theorems is actually constructed from the modulation and one common axis-pressure function.

noncomputable def NavierStokes.ModulatedCone.Repaired.profileRepair {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (patch : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → ModulatedHistories.Coeff) (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) : ProfileHistories.Profiles D

The actual physical correction, retaining the existing axis pressure.

Equations

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

theorem NavierStokes.ModulatedCone.Repaired.profileRepair_radial_germs {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (patch : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → ModulatedHistories.Coeff) (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) {p : ProfileHistories.Point} (hp : p.1 ∉ Set.Ioo patch.left patch.right) : ((fun (X : ℝ) => (profileRepair P patch A c hA hc).E (X, p.2)) =ᶠ[nhds p.1] fun (X : ℝ) => P.E (X, p.2)) ∧ (fun (X : ℝ) => (profileRepair P patch A c hA hc).U (X, p.2)) =ᶠ[nhds p.1] fun (X : ℝ) => P.U (X, p.2)

noncomputable def NavierStokes.ModulatedCone.Repaired.rowsEta {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) : Fin 5 → ℝ

Rows eta, given by ![parameterPartial P.M p, parameterPartial P.I p, parameterPartial P.J p, parameterPartial P.S p, parameterPartial P.pressure p].

Equations

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

theorem NavierStokes.ModulatedCone.Repaired.rows_hasDerivAt {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) : HasDerivAt (fun (η : ℝ) => ModulatedHistories.profileRows P (p.1, η)) (rowsEta P p) p.2

theorem NavierStokes.ModulatedCone.Repaired.profileHistory_eta_eq_row {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (row : StressActivation.HistoryRow) (p : ProfileHistories.Point) : ProfileHistories.parameterPartial (StressActivation.profileHistory P row) p = rowsEta P p (Localized.historyIndex row)

theorem NavierStokes.ModulatedCone.Repaired.rows_first_jet_bound {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hp' : p ∈ D'.carrier) {J : Set ℝ} {ε : ℝ} (hjet : JetBounds.FiniteJetBound 1 (fun (η : ℝ) => ModulatedHistories.profileRows P (p.1, η) - ModulatedHistories.profileRows Q (p.1, η)) J ε) (hη : p.2 ∈ J) (row : StressActivation.HistoryRow) : |StressActivation.profileHistory P row p - StressActivation.profileHistory Q row p| ≤ ε ∧ |ProfileHistories.parameterPartial (StressActivation.profileHistory P row) p - ProfileHistories.parameterPartial (StressActivation.profileHistory Q row) p| ≤ ε

Vector bounds for the five actual history jets imply each actual history/parameter-derivative bound needed by the stock estimate.

theorem NavierStokes.ModulatedCone.Repaired.shears_unchanged_outside {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (patch : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → ModulatedHistories.Coeff) (hf : P.f = ModulatedHistories.applyRepairF patch A c Q.f) (hU : P.U = ModulatedHistories.applyRepairU patch A c Q.U) {p : ProfileHistories.Point} (hp : p.1 ∉ Set.Ioo patch.left patch.right) : P.E p = Q.E p ∧ P.U p = Q.U p ∧ angularShear P.E p = angularShear Q.E p ∧ signedAxialShear P.E P.U p = signedAxialShear Q.E Q.U p

The actual correction leaves the physical fields and both radial shears unchanged outside the open repair patch.

theorem NavierStokes.ModulatedCone.Repaired.radialDerivative_add (F G : ProfileHistories.Field) (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (p : ProfileHistories.Point) : radialDerivative (fun (q : ParametricModulation.RadialParameter) => F q + G q) p = radialDerivative F p + radialDerivative G p

theorem NavierStokes.ModulatedCone.Repaired.field_difference_identities {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (patch : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → ModulatedHistories.Coeff) (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) (hf : P.f = ModulatedHistories.applyRepairF patch A c Q.f) (hU : P.U = ModulatedHistories.applyRepairU patch A c Q.U) (E U : ProfileHistories.Field) (hE : ContDiff ℝ (↑⊤) E) (hUs : ContDiff ℝ (↑⊤) U) {p : ProfileHistories.Point} (hp : 0 < p.1) (hbaseE : Q.E =ᶠ[nhds p] E) (hbaseU : Q.U =ᶠ[nhds p] U) : P.E p - E p = ModulatedHistories.editE patch A c p ∧ radialDerivative P.E p - radialDerivative E p = radialDerivative (ModulatedHistories.editE patch A c) p ∧ radialDerivative P.U p - radialDerivative U p = radialDerivative (ModulatedHistories.editU patch A c) p

On a patch where the base profile is nominal, the actual physical repair has exactly its prescribed additive value and derivative errors.

theorem NavierStokes.ModulatedCone.Repaired.field_C1_bound (patch : FiveProfileMoments.Patch) (J : Set ℝ) (hJ : IsCompact J) (A : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) : ∃ (C : ℝ), 0 < C ∧ ∀ (c : ℝ → ModulatedHistories.Coeff), ContDiff ℝ (↑⊤) c → ∀ (ε : ℝ), 0 ≤ ε → JetBounds.FiniteJetBound 1 c J ε → ∀ {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D'), P.f = ModulatedHistories.applyRepairF patch A c Q.f → P.U = ModulatedHistories.applyRepairU patch A c Q.U → ∀ (E U : ProfileHistories.Field), ContDiff ℝ (↑⊤) E → ContDiff ℝ (↑⊤) U → ∀ (p : ProfileHistories.Point), 0 < p.1 → p.2 ∈ J → Q.E =ᶠ[nhds p] E → Q.U =ᶠ[nhds p] U → |P.E p - E p| ≤ C * ε ∧ |radialDerivative P.E p - radialDerivative E p| ≤ C * ε ∧ |radialDerivative P.U p - radialDerivative U p| ≤ C * ε

The actual moment edit supplies a uniform first-radial-derivative bound from its coefficient jet bound. No shear estimate is a premise.

theorem NavierStokes.ModulatedCone.Repaired.window_shears_match {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D D' : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hBK : B ⊆ K) (J : Set ℝ) (hends : ∀ η ∈ J, (W.left, η) ∈ B ∧ (W.right, η) ∈ B) (n : ℝ) (Q : ProfileHistories.Profiles D) (P : ProfileHistories.Profiles D') (hQf : Q.f = ModulatedHistories.localizedF W r f n) (hQU : Q.U = ModulatedHistories.localizedU W r E U n) (patch : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → ModulatedHistories.Coeff) (hgap : W.right < patch.left) (hPf : P.f = ModulatedHistories.applyRepairF patch A c Q.f) (hPU : P.U = ModulatedHistories.applyRepairU patch A c Q.U) {p : ProfileHistories.Point} (hp : p.1 ∈ Set.Icc W.left W.right) (hη : p.2 ∈ J) (hphys : E =ᶠ[nhds p] fun (q : ProfileHistories.Point) => √(2 * q.1) * f q) : angularShear P.E p = angularShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E n q.1 q.2) p ∧ signedAxialShear P.E P.U p = signedAxialShear (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedE r E n q.1 q.2) (fun (q : ParametricModulation.RadialParameter) => ParametricModulation.realizedU r E U n q.1 q.2) p

A later repair preserves the already realized shears on the entire closed modulation window, including both endpoint collars.

theorem NavierStokes.ModulatedCone.Repaired.profile_data_bound {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (patch : FiveProfileMoments.Patch) (hgap : W.right < patch.left) (A : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (J : Set ℝ) (hJ : IsCompact J) : ∃ (δ : ℝ) (C₁ : ℝ) (C₂ : ℝ), 0 < δ ∧ 0 < C₁ ∧ 0 < C₂ ∧ ∀ (n : ℝ), 1 ≤ n → ∀ (c : ℝ → ModulatedHistories.Coeff), ContDiff ℝ (↑⊤) c → ∀ (ε : ℝ), 0 ≤ ε → ε ≤ δ → JetBounds.FiniteJetBound 1 c J ε → ∀ {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D'), P.f = ModulatedHistories.applyRepairF patch A c (ModulatedHistories.localizedF W r f n) → P.U = ModulatedHistories.applyRepairU patch A c (ModulatedHistories.localizedU W r E U n) → Q.f = f → Q.U = U → P.pressure0 = Q.pressure0 → ∀ (p : ProfileHistories.Point), 0 ≤ p.1 → p.2 ∈ J → p ∈ D.carrier → p ∈ D'.carrier → ‖ModulatedStockBounds.profileData P p - ModulatedStockBounds.profileData Q p‖ ≤ C₁ / n + C₂ * ε

The actual repaired profile data satisfy a uniform estimate before, inside, and after the repair. The two contributions are the modulation error and the coefficient size of this same physical repair.

theorem NavierStokes.ModulatedCone.Repaired.profile_stocks_rate {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D D' : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (patch : FiveProfileMoments.Patch) (hgap : W.right < patch.left) (A : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (J : Set ℝ) (hJ : IsCompact J) (c : ℝ → ℝ → ModulatedHistories.Coeff) (hc : ∀ (n : ℝ), ContDiff ℝ (↑⊤) (c n)) (n₀ Cc : ℝ) (hCc : 0 ≤ Cc) (hcoeff : ∀ (n : ℝ), n₀ ≤ n → 1 ≤ n → JetBounds.FiniteJetBound 1 (c n) J (Cc / n)) (P : ℝ → ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hPf : ∀ (n : ℝ), (P n).f = ModulatedHistories.applyRepairF patch A (c n) (ModulatedHistories.localizedF W r f n)) (hPU : ∀ (n : ℝ), (P n).U = ModulatedHistories.applyRepairU patch A (c n) (ModulatedHistories.localizedU W r E U n)) (hQf : Q.f = f) (hQU : Q.U = U) (hP0 : ∀ (n : ℝ), (P n).pressure0 = Q.pressure0) (T : Set ProfileHistories.Point) (hT : IsCompact T) (hTJ : ∀ p ∈ T, p.2 ∈ J) (hTD : T ⊆ D.carrier) (hTD' : T ⊆ D'.carrier) (h : ℝ) (hX : ∀ p ∈ T, 0 < p.1) (hL : ∀ p ∈ T, NaturalAxisData.L h p.2 ≠ 0) (hpos : ∀ p ∈ T, 0 < Q.f p) : ∃ (N : ℕ) (C : ℝ), 0 < N ∧ 0 ≤ C ∧ ∀ (n : ℝ), ↑N ≤ n → ∀ p ∈ T, 0 < (P n).f p ∧ |ActivationStocks.profileStockOne (P n) h p - ActivationStocks.profileStockOne Q h p| ≤ C / n ∧ |ActivationStocks.profileStockTwo (P n) h p - ActivationStocks.profileStockTwo Q h p| ≤ C / n

Uniform stock estimates for a family of actual repaired profiles, using only the proved coefficient size of the moment solver.

theorem NavierStokes.ModulatedCone.Repaired.profiles_trueCone {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D D' : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (hK : IsCompact K) (hKW : ∀ p ∈ K, p.1 ∈ Set.Icc W.left W.right) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₁ : ContDiff ℝ (↑⊤) p₁) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (haK : ∀ p ∈ K, 0 < a p) (S : Set ProfileHistories.Point) (hS : IsCompact S) (hSW : ∀ p ∈ S, W.right ≤ p.1) (haNom : ∀ p ∈ K ∪ S, a p = angularShear E p) (hbNom : ∀ p ∈ K ∪ S, a p * m p = signedAxialShear E U p) (hrelaxed : ∀ p ∈ K, TrueConeLoop.nominalSpeed (a p) (m p) < ConeAlgebra.coneBound (p₁ p + p₂ p * m p) (p₂ p - p₁ p * m p)) (hScone : ∀ p ∈ S, TrueConeLoop.InTrueCone (p₁ p) (p₂ p) (a p) (a p * m p)) (P : ℝ → ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hPf : ∀ (n : ℝ), (P n).f = ModulatedHistories.localizedF W r f n) (hPU : ∀ (n : ℝ), (P n).U = ModulatedHistories.localizedU W r E U n) (hQf : Q.f = f) (hQU : Q.U = U) (hP0 : ∀ (n : ℝ), (P n).pressure0 = Q.pressure0) (J : Set ℝ) (hJ : IsCompact J) (hTJ : ∀ p ∈ K ∪ S, p.2 ∈ J) (hTD : K ∪ S ⊆ D.carrier) (hTD' : K ∪ S ⊆ D'.carrier) (h : ℝ) (hL : ∀ p ∈ K ∪ S, NaturalAxisData.L h p.2 ≠ 0) (hpos : ∀ p ∈ K ∪ S, 0 < Q.f p) (hstock₁ : ∀ p ∈ K ∪ S, p₁ p = ActivationStocks.profileStockOne Q h p) (hstock₂ : ∀ p ∈ K ∪ S, p₂ p = ActivationStocks.profileStockTwo Q h p) (hBK : B ⊆ K) (hends : ∀ η ∈ J, (W.left, η) ∈ B ∧ (W.right, η) ∈ B) (hphys : ∀ p ∈ K ∪ S, E =ᶠ[nhds p] fun (q : ParametricModulation.RadialParameter) => √(2 * q.1) * f q) (patch : FiveProfileMoments.Patch) (hgap : W.right < patch.left) (A : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (c : ℝ → ℝ → ModulatedHistories.Coeff) (hc : ∀ (n : ℝ), ContDiff ℝ (↑⊤) (c n)) (n₀ Cc : ℝ) (hCc : 0 ≤ Cc) (hcoeff : ∀ (n : ℝ), n₀ ≤ n → 1 ≤ n → JetBounds.FiniteJetBound 1 (c n) J (Cc / n)) : ∃ (N : ℕ), 0 < N ∧ ∀ (n : ℕ), N ≤ n → ∀ p ∈ K ∪ S, have R := profileRepair (P ↑n) patch A (c ↑n) hA ⋯; 0 < R.f p ∧ TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne R h p) (ActivationStocks.profileStockTwo R h p) (angularShear R.E p) (signedAxialShear R.E R.U p)

Both portions of the actual repaired construction lie in the true cone for one finite frequency threshold. The coefficient input is the quantitative output of the actual moment solver.

theorem NavierStokes.ModulatedCone.Repaired.exists_with_moment_repair {a m p₁ p₂ : ParametricModulation.RadialParameter → ℝ} {K B : Set ParametricModulation.RadialParameter} {D D' : ProfileHistories.RadialDomain} (W : ModulatedHistories.Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : ProfileHistories.Field) (hK : IsCompact K) (hKW : ∀ p ∈ K, p.1 ∈ Set.Icc W.left W.right) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₁ : ContDiff ℝ (↑⊤) p₁) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (haK : ∀ p ∈ K, 0 < a p) (S : Set ProfileHistories.Point) (hS : IsCompact S) (hSW : ∀ p ∈ S, W.right ≤ p.1) (haNom : ∀ p ∈ K ∪ S, a p = angularShear E p) (hbNom : ∀ p ∈ K ∪ S, a p * m p = signedAxialShear E U p) (hrelaxed : ∀ p ∈ K, TrueConeLoop.nominalSpeed (a p) (m p) < ConeAlgebra.coneBound (p₁ p + p₂ p * m p) (p₂ p - p₁ p * m p)) (hScone : ∀ p ∈ S, TrueConeLoop.InTrueCone (p₁ p) (p₂ p) (a p) (a p * m p)) (P : ℝ → ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hPf : ∀ (n : ℝ), (P n).f = ModulatedHistories.localizedF W r f n) (hPU : ∀ (n : ℝ), (P n).U = ModulatedHistories.localizedU W r E U n) (hQf : Q.f = f) (hQU : Q.U = U) (hP0 : ∀ (n : ℝ), (P n).pressure0 = Q.pressure0) (J : Set ℝ) (hJ : IsCompact J) (hTJ : ∀ p ∈ K ∪ S, p.2 ∈ J) (hTD : K ∪ S ⊆ D.carrier) (hTD' : K ∪ S ⊆ D'.carrier) (h : ℝ) (hL : ∀ p ∈ K ∪ S, NaturalAxisData.L h p.2 ≠ 0) (hpos : ∀ p ∈ K ∪ S, 0 < Q.f p) (hstock₁ : ∀ p ∈ K ∪ S, p₁ p = ActivationStocks.profileStockOne Q h p) (hstock₂ : ∀ p ∈ K ∪ S, p₂ p = ActivationStocks.profileStockTwo Q h p) (hBK : B ⊆ K) (hends : ∀ η ∈ J, (W.left, η) ∈ B ∧ (W.right, η) ∈ B) (hphys : ∀ p ∈ K ∪ S, E =ᶠ[nhds p] fun (q : ParametricModulation.RadialParameter) => √(2 * q.1) * f q) (patch : FiveProfileMoments.Patch) (hgap : W.right < patch.left) (A G : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (hG : ContDiff ℝ (↑⊤) G) (hApos : ∀ (η : ℝ), 0 < A η) (hwindow : Set.Icc W.left W.right ×ˢ J ⊆ K) (hfollowing : Set.Icc W.right patch.right ×ˢ J ⊆ S) (b : ℝ) (hb : FiveProfileMoments.GoodExponent b) (hpatchU : ∀ η ∈ J, ∀ X ∈ Set.Ioo patch.left patch.right, U (X, η) = G η) (hpatchE : ∀ η ∈ J, ∀ X ∈ Set.Ioo patch.left patch.right, √(2 * X) * f (X, η) = A η * X ^ b) : ∃ (N : ℕ) (c : ℝ → ModulatedHistories.Coeff) (hc : ContDiff ℝ (↑⊤) c), 0 < N ∧ have R := profileRepair (P ↑N) patch A c hA hc; (∀ p ∈ Set.Icc W.left patch.right ×ˢ J, 0 < R.f p ∧ TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne R h p) (ActivationStocks.profileStockTwo R h p) (angularShear R.E p) (signedAxialShear R.E R.U p)) ∧ (∀ η ∈ J, ∀ (X : ℝ), patch.right ≤ X → ModulatedHistories.profileRows R (X, η) = ModulatedHistories.profileRows Q (X, η)) ∧ ∀ (p : ProfileHistories.Point), p.1 ∉ Set.Ioo patch.left patch.right → R.E p = (P ↑N).E p ∧ R.U p = (P ↑N).U p ∧ angularShear R.E p = angularShear (P ↑N).E p ∧ signedAxialShear R.E R.U p = signedAxialShear (P ↑N).E (P ↑N).U p

The actual nonlinear five-row solve and the actual modulation allow one finite integer frequency with the true cone throughout the loop and following nominal patch. All five histories are restored exactly after the repair, and every radial germ outside its support is unchanged.