Actual lag stocks during the activation ramp

The stock formulas are obtained from the genuine five profile histories. Smooth difference factors are constructed from the field and history factors; no estimate for a stock difference is supplied as an assumption.

Bounds for a shrinking activation ramp

The clock u = y / T keeps the cutoff fixed while the width tends to zero. All error factors below are actual transformed integrals and are smooth at T = 0. Compactness therefore gives width-uniform parameter-jet estimates.

noncomputable def NavierStokes.ActivationBounds.parameterCoefficient {E : Type u_1} (B : E × ProfileHistories.Point → ℝ) (q : (E × ℝ) × ℝ) : ℝ

Parameter coefficient, given by B (q.1.1, (q.2, q.1.2)) / stepDenominator 1 q.2.

Equations

• NavierStokes.ActivationBounds.parameterCoefficient B q = B (q.1.1, q.2, q.1.2) / NavierStokes.StressActivation.stepDenominator 1 q.2

noncomputable def NavierStokes.ActivationBounds.parameterFactor {E : Type u_1} (B : E × ProfileHistories.Point → ℝ) (q : E × ProfileHistories.Point) : ℝ

Parameter factor, given by q.2.1 ^ 2 * stepDenominator 1 q.2.1 * ParametricFlatFactor.factor 1 0 (parameterCoefficient B) ((q.1, q.2.2), q.2.1).

Equations

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

theorem NavierStokes.ActivationBounds.parameterFactor_eq {E : Type u_1} (B : E × ProfileHistories.Point → ℝ) (q : E) (p : ProfileHistories.Point) : parameterFactor B (q, p) = StressActivation.primitiveFactor 1 (fun (z : ProfileHistories.Point) => B (q, z)) p

theorem NavierStokes.ActivationBounds.parameterFactor_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {S : Set E} (hS : IsOpen S) {J : Set ℝ} (hJ : IsOpen J) {B : E × ProfileHistories.Point → ℝ} (hB : ContDiffOn ℝ (↑⊤) B (S ×ˢ Set.univ ×ˢ J)) : ContDiffOn ℝ (↑⊤) (parameterFactor B) (S ×ˢ Set.univ ×ˢ J)

@[simp]

theorem NavierStokes.ActivationBounds.parameterFactor_zero {E : Type u_1} (B : E × ProfileHistories.Point → ℝ) (q : E) (η : ℝ) : parameterFactor B (q, 0, η) = 0

theorem NavierStokes.ActivationBounds.parameterFactor_identity {E : Type u_1} (B : E × ProfileHistories.Point → ℝ) (q : E) (κ : ℝ) (p : ProfileHistories.Point) : StressActivation.weightedPrimitive 1 κ (fun (z : ProfileHistories.Point) => B (q, z)) p = p.1 * StressActivation.activation 1 κ p.1 * parameterFactor B (q, p)

theorem NavierStokes.ActivationBounds.compact_parameter_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {S Q : Set E} (hS : IsOpen S) (hQ : IsCompact Q) (hQS : Q ⊆ S) {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {H : E × ProfileHistories.Point → ℝ} (hH : ContDiffOn ℝ (↑⊤) H (S ×ˢ Set.univ ×ˢ J)) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ q ∈ Q, ∀ u ∈ Set.Icc 0 1, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => H (q, u, ξ)) η| ≤ M

A compact family bounds genuine parameter derivatives, with no restriction on the number of auxiliary parameters.

@[reducible, inline]

abbrev NavierStokes.ActivationBounds.ScaledPoint : Type

Scaled point: an abbreviation for (ℝ × ℝ) × Point.

Equations

• NavierStokes.ActivationBounds.ScaledPoint = ((ℝ × ℝ) × NavierStokes.ProfileHistories.Point)

noncomputable def NavierStokes.ActivationBounds.scaledDomain (J : Set ℝ) : Set ScaledPoint

Scaled domain, given by univ ×ˢ (univ ×ˢ J).

Equations

• NavierStokes.ActivationBounds.scaledDomain J = Set.univ ×ˢ Set.univ ×ˢ J

theorem NavierStokes.ActivationBounds.scaledDomain_open {J : Set ℝ} (hJ : IsOpen J) : IsOpen (scaledDomain J)

noncomputable def NavierStokes.ActivationBounds.rescale (F : ProfileHistories.Field) (q : ScaledPoint) : ℝ

The auxiliary parameters are (κ,T) and the point is (u,η).

Equations

• NavierStokes.ActivationBounds.rescale F q = F (q.1.2 * q.2.1, q.2.2)

theorem NavierStokes.ActivationBounds.rescale_smooth {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (rescale F) (scaledDomain J)

noncomputable def NavierStokes.ActivationBounds.scaledDistance (q : ScaledPoint) : ℝ

Scaled distance, given by q.1.2 * q.2.1 * activation 1 q.1.1 q.2.1.

Equations

• NavierStokes.ActivationBounds.scaledDistance q = q.1.2 * q.2.1 * NavierStokes.StressActivation.activation 1 q.1.1 q.2.1

theorem NavierStokes.ActivationBounds.scaledDistance_smooth : ContDiff ℝ (↑⊤) scaledDistance

theorem NavierStokes.ActivationBounds.activation_scaled {T : ℝ} (hT : T ≠ 0) (κ u : ℝ) : StressActivation.activation T κ (T * u) = StressActivation.activation 1 κ u

theorem NavierStokes.ActivationBounds.primitive_rescaled (T : ℝ) (F : ProfileHistories.Field) (u η : ℝ) : ProfileHistories.primitive F (T * u, η) = T * ProfileHistories.primitive (fun (p : ProfileHistories.Point) => F (T * p.1, p.2)) (u, η)

theorem NavierStokes.ActivationBounds.weightedPrimitive_rescaled {T : ℝ} (hT : T ≠ 0) (κ : ℝ) (B : ProfileHistories.Field) (u η : ℝ) : StressActivation.weightedPrimitive T κ B (T * u, η) = T * StressActivation.weightedPrimitive 1 κ (fun (p : ProfileHistories.Point) => B (T * p.1, p.2)) (u, η)

noncomputable def NavierStokes.ActivationBounds.primitiveErrorFactor (B : ProfileHistories.Field) : ScaledPoint → ℝ

Primitive error factor, given by parameterFactor (rescale B).

Equations

• NavierStokes.ActivationBounds.primitiveErrorFactor B = NavierStokes.ActivationBounds.parameterFactor (NavierStokes.ActivationBounds.rescale B)

theorem NavierStokes.ActivationBounds.primitiveErrorFactor_smooth {J : Set ℝ} (hJ : IsOpen J) {B : ProfileHistories.Field} (hB : ContDiffOn ℝ (↑⊤) B (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (primitiveErrorFactor B) (scaledDomain J)

theorem NavierStokes.ActivationBounds.weightedPrimitive_scaled_factor {T : ℝ} (hT : T ≠ 0) (κ : ℝ) (B : ProfileHistories.Field) (u η : ℝ) : StressActivation.weightedPrimitive T κ B (T * u, η) = scaledDistance ((κ, T), u, η) * primitiveErrorFactor B ((κ, T), u, η)

noncomputable def NavierStokes.ActivationBounds.controlledErrorFactor (F : ProfileHistories.Field) : ScaledPoint → ℝ

Controlled error factor, defined pointwise by -primitiveErrorFactor (radialPartial F) q.

Equations

• NavierStokes.ActivationBounds.controlledErrorFactor F q = -NavierStokes.ActivationBounds.primitiveErrorFactor (NavierStokes.ProfileHistories.radialPartial F) q

theorem NavierStokes.ActivationBounds.controlledErrorFactor_smooth {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (controlledErrorFactor F) (scaledDomain J)

theorem NavierStokes.ActivationBounds.controlled_scaled_factor {T : ℝ} (hT : T ≠ 0) (κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) (u : ℝ) {η : ℝ} (hη : η ∈ J) : StressActivation.controlled T κ F (T * u, η) - F (T * u, η) = scaledDistance ((κ, T), u, η) * controlledErrorFactor F ((κ, T), u, η)

noncomputable def NavierStokes.ActivationBounds.controlledValue (F : ProfileHistories.Field) (q : ScaledPoint) : ℝ

Controlled value, given by rescale F q + scaledDistance q * controlledErrorFactor F q.

Equations

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

theorem NavierStokes.ActivationBounds.controlledValue_smooth {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (controlledValue F) (scaledDomain J)

theorem NavierStokes.ActivationBounds.controlledValue_eq {T : ℝ} (hT : T ≠ 0) (κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) (u : ℝ) {η : ℝ} (hη : η ∈ J) : controlledValue F ((κ, T), u, η) = StressActivation.controlled T κ F (T * u, η)

noncomputable def NavierStokes.ActivationBounds.angularValue (L : ProfileHistories.Field) : ScaledPoint → ℝ

Angular value, defined pointwise by Real.exp (controlledValue L q).

Equations

• NavierStokes.ActivationBounds.angularValue L q = Real.exp (NavierStokes.ActivationBounds.controlledValue L q)

noncomputable def NavierStokes.ActivationBounds.relativeErrorFactor (L : ProfileHistories.Field) (q : ScaledPoint) : ℝ

Relative error factor, given by controlledErrorFactor L q * meanExp (scaledDistance q * controlledErrorFactor L q).

Equations

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

theorem NavierStokes.ActivationBounds.relativeErrorFactor_smooth {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (relativeErrorFactor L) (scaledDomain J)

theorem NavierStokes.ActivationBounds.angular_relative_scaled_factor {T : ℝ} (hT : T ≠ 0) (κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (u : ℝ) {η : ℝ} (hη : η ∈ J) : StressActivation.activatedAngular T κ L (T * u, η) / StressActivation.referenceAngular L (T * u, η) - 1 = scaledDistance ((κ, T), u, η) * relativeErrorFactor L ((κ, T), u, η)

noncomputable def NavierStokes.ActivationBounds.angularErrorFactor (L : ProfileHistories.Field) (q : ScaledPoint) : ℝ

Angular error factor, given by Real.exp (rescale L q) * relativeErrorFactor L q.

Equations

• NavierStokes.ActivationBounds.angularErrorFactor L q = Real.exp (NavierStokes.ActivationBounds.rescale L q) * NavierStokes.ActivationBounds.relativeErrorFactor L q

theorem NavierStokes.ActivationBounds.angularErrorFactor_smooth {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (angularErrorFactor L) (scaledDomain J)

theorem NavierStokes.ActivationBounds.angular_scaled_factor {T : ℝ} (hT : T ≠ 0) (κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (u : ℝ) {η : ℝ} (hη : η ∈ J) : StressActivation.activatedAngular T κ L (T * u, η) - StressActivation.referenceAngular L (T * u, η) = scaledDistance ((κ, T), u, η) * angularErrorFactor L ((κ, T), u, η)

theorem NavierStokes.ActivationBounds.width_uniform_jet_bound {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {H : ScaledPoint → ℝ} (hH : ContDiffOn ℝ (↑⊤) H (scaledDomain J)) {E : ℝ → ℝ → ℝ → ℝ → ℝ} (hE : ∀ (κ T : ℝ), 0 < T → ∀ (u η : ℝ), η ∈ J → E κ T (T * u) η = scaledDistance ((κ, T), u, η) * H ((κ, T), u, η)) (T0 : ℝ) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ T ∈ Set.Ioc 0 T0, ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (E κ T y) η| ≤ M * y * StressActivation.activation T κ y

A smooth fixed-clock factor gives one constant for every positive ramp width up to T0, including widths arbitrarily close to zero.

theorem NavierStokes.ActivationBounds.weightedPrimitive_uniform_jets {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {B : ProfileHistories.Field} (hB : ContDiffOn ℝ (↑⊤) B (StressActivation.logDomain J hJ).carrier) (T0 : ℝ) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ T ∈ Set.Ioc 0 T0, ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => StressActivation.weightedPrimitive T κ B (y, ξ)) η| ≤ M * y * StressActivation.activation T κ y

theorem NavierStokes.ActivationBounds.controlled_uniform_jets {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) (T0 : ℝ) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ T ∈ Set.Ioc 0 T0, ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => StressActivation.controlled T κ F (y, ξ) - F (y, ξ)) η| ≤ M * y * StressActivation.activation T κ y

theorem NavierStokes.ActivationBounds.angular_relative_uniform_jets {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (T0 : ℝ) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ T ∈ Set.Ioc 0 T0, ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => StressActivation.activatedAngular T κ L (y, ξ) / StressActivation.referenceAngular L (y, ξ) - 1) η| ≤ M * y * StressActivation.activation T κ y

theorem NavierStokes.ActivationBounds.angular_uniform_jets {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (T0 : ℝ) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ T ∈ Set.Ioc 0 T0, ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => StressActivation.activatedAngular T κ L (y, ξ) - StressActivation.referenceAngular L (y, ξ)) η| ≤ M * y * StressActivation.activation T κ y

Width-uniform factors for the actual five histories

noncomputable def NavierStokes.ActivationBounds.densityErrorFactor (X0 : ℝ) (L U : ProfileHistories.Field) (r : StressActivation.HistoryRow) (q : ScaledPoint) : ℝ

Density error factor as an element of ℝ.

Equations

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

theorem NavierStokes.ActivationBounds.densityErrorFactor_smooth (X0 : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (r : StressActivation.HistoryRow) : ContDiffOn ℝ (↑⊤) (densityErrorFactor X0 L U r) (scaledDomain J)

theorem NavierStokes.ActivationBounds.density_scaled_factor {T : ℝ} (hT : T ≠ 0) (κ X0 : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (r : StressActivation.HistoryRow) (u : ℝ) {η : ℝ} (hη : η ∈ J) : StressActivation.logDensity X0 (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U) r (T * u, η) - StressActivation.logDensity X0 (StressActivation.referenceAngular L) U r (T * u, η) = scaledDistance ((κ, T), u, η) * densityErrorFactor X0 L U r ((κ, T), u, η)

noncomputable def NavierStokes.ActivationBounds.historyCoefficient (X0 : ℝ) (L U : ProfileHistories.Field) (r : StressActivation.HistoryRow) (q : ScaledPoint) : ℝ

History coefficient, given by q.1.2 * q.2.1 * densityErrorFactor X0 L U r q.

Equations

• NavierStokes.ActivationBounds.historyCoefficient X0 L U r q = q.1.2 * q.2.1 * NavierStokes.ActivationBounds.densityErrorFactor X0 L U r q

noncomputable def NavierStokes.ActivationBounds.historyErrorFactor (X0 : ℝ) (L U : ProfileHistories.Field) (r : StressActivation.HistoryRow) : ScaledPoint → ℝ

History error factor, given by parameterFactor (historyCoefficient X0 L U r).

Equations

• NavierStokes.ActivationBounds.historyErrorFactor X0 L U r = NavierStokes.ActivationBounds.parameterFactor (NavierStokes.ActivationBounds.historyCoefficient X0 L U r)

theorem NavierStokes.ActivationBounds.historyErrorFactor_smooth (X0 : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (r : StressActivation.HistoryRow) : ContDiffOn ℝ (↑⊤) (historyErrorFactor X0 L U r) (scaledDomain J)

@[simp]

theorem NavierStokes.ActivationBounds.historyErrorFactor_zero (X0 : ℝ) (L U : ProfileHistories.Field) (r : StressActivation.HistoryRow) (κ T η : ℝ) : historyErrorFactor X0 L U r ((κ, T), 0, η) = 0

theorem NavierStokes.ActivationBounds.history_scaled_factor {T : ℝ} (hT : T ≠ 0) (κ X0 : ℝ) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (r : StressActivation.HistoryRow) (u : ℝ) {η : ℝ} (hη : η ∈ J) : StressActivation.logHistory X0 initial (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U) r (T * u, η) - StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U r (T * u, η) = scaledDistance ((κ, T), u, η) * historyErrorFactor X0 L U r ((κ, T), u, η)

theorem NavierStokes.ActivationBounds.history_uniform_jets (X0 : ℝ) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (T0 : ℝ) (r : StressActivation.HistoryRow) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ T ∈ Set.Ioc 0 T0, ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => StressActivation.logHistory X0 initial (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U) r (y, ξ) - StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U r (y, ξ)) η| ≤ M * y * StressActivation.activation T κ y

Genuine parameter differentiation of the scaled factors

noncomputable def NavierStokes.ActivationBounds.etaD (H : ScaledPoint → ℝ) (q : ScaledPoint) : ℝ

Eta D, given by deriv (fun ξ => H (q.1, (q.2.1, ξ))) q.2.2.

Equations

• NavierStokes.ActivationBounds.etaD H q = deriv (fun (ξ : ℝ) => H (q.1, q.2.1, ξ)) q.2.2

noncomputable def NavierStokes.ActivationBounds.etaLinear (H : ScaledPoint → ℝ) (q : ScaledPoint) : ℝ

Eta linear, given by fderiv ℝ H q ((0, 0), (0, 1)).

Equations

• NavierStokes.ActivationBounds.etaLinear H q = (fderiv ℝ H q) ((0, 0), 0, 1)

theorem NavierStokes.ActivationBounds.etaLinear_hasDerivAt {J : Set ℝ} (hJ : IsOpen J) {H : ScaledPoint → ℝ} (hH : ContDiffOn ℝ (↑⊤) H (scaledDomain J)) {q : ScaledPoint} (hq : q ∈ scaledDomain J) : HasDerivAt (fun (ξ : ℝ) => H (q.1, q.2.1, ξ)) (etaLinear H q) q.2.2

theorem NavierStokes.ActivationBounds.etaD_eq_etaLinear {J : Set ℝ} (hJ : IsOpen J) {H : ScaledPoint → ℝ} (hH : ContDiffOn ℝ (↑⊤) H (scaledDomain J)) {q : ScaledPoint} (hq : q ∈ scaledDomain J) : etaD H q = etaLinear H q

theorem NavierStokes.ActivationBounds.etaD_smooth {J : Set ℝ} (hJ : IsOpen J) {H : ScaledPoint → ℝ} (hH : ContDiffOn ℝ (↑⊤) H (scaledDomain J)) : ContDiffOn ℝ (↑⊤) (etaD H) (scaledDomain J)

theorem NavierStokes.ActivationBounds.etaD_hasDerivAt {J : Set ℝ} (hJ : IsOpen J) {H : ScaledPoint → ℝ} (hH : ContDiffOn ℝ (↑⊤) H (scaledDomain J)) {q : ScaledPoint} (hq : q ∈ scaledDomain J) : HasDerivAt (fun (ξ : ℝ) => H (q.1, q.2.1, ξ)) (etaD H q) q.2.2

theorem NavierStokes.ActivationBounds.etaD_scaledDistance_mul (H : ScaledPoint → ℝ) (q : ScaledPoint) : etaD (fun (z : ScaledPoint) => scaledDistance z * H z) q = scaledDistance q * etaD H q

theorem NavierStokes.ActivationBounds.etaD_rescale {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) {q : ScaledPoint} (hq : q ∈ scaledDomain J) : etaD (rescale F) q = rescale (ProfileHistories.parameterPartial F) q

theorem NavierStokes.ActivationBounds.etaD_congr {J : Set ℝ} (hJ : IsOpen J) {H G : ScaledPoint → ℝ} (h : ∀ q ∈ scaledDomain J, H q = G q) {q : ScaledPoint} (hq : q ∈ scaledDomain J) : etaD H q = etaD G q

Independence of the continuation length on the natural overlap

theorem NavierStokes.ActivationBounds.continuation_radialPartial {R δ : ℝ} (hR : 0 < R) (hδ : 0 < δ) (hδR : 2 * δ < R) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (ReferencePath.earlyStrip R hR J hJ).carrier) {p : ProfileHistories.Point} (hη : p.2 ∈ J) : ProfileHistories.radialPartial (ReferencePath.continuation δ G) p = ReferencePath.slopeCutoff δ p.1 * ProfileHistories.radialPartial G p

theorem NavierStokes.ActivationBounds.controlled_continuation_independent {R δ₁ δ₂ : ℝ} (hR : 0 < R) (hδ₁ : 0 < δ₁) (hδ₁R : 2 * δ₁ < R) (hδ₂ : 0 < δ₂) (hδ₂R : 2 * δ₂ < R) {J : Set ℝ} (hJ : IsOpen J) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (ReferencePath.earlyStrip R hR J hJ).carrier) (T κ : ℝ) {p : ProfileHistories.Point} (hη : p.2 ∈ J) (hp₁ : p.1 ≤ δ₁) (hp₂ : p.1 ≤ δ₂) : StressActivation.controlled T κ (ReferencePath.continuation δ₁ G) p = StressActivation.controlled T κ (ReferencePath.continuation δ₂ G) p

theorem NavierStokes.ActivationBounds.profileInitial_congr {D : ProfileHistories.RadialDomain} (P Q : ProfileHistories.Profiles D) (h0 : ∀ (η : ℝ), P.pressure0 η = Q.pressure0 η) (r : StressActivation.HistoryRow) (η : ℝ) : StressActivation.profileInitial P r η = StressActivation.profileInitial Q r η

theorem NavierStokes.ActivationBounds.NaturalOverlap.f_independent (N : ReferencePath.Input) {T δ₁ δ₂ : ℝ} (hT : 0 < T) (hδ₁ : 0 < δ₁) (hδ₁R : 2 * δ₁ < ReferencePath.rampLimit) (hδ₂ : 0 < δ₂) (hδ₂R : 2 * δ₂ < ReferencePath.rampLimit) (κ : ℝ) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hp₁ : p.1 ≤ StressActivation.radius N.endpoint δ₁) (hp₂ : p.1 ≤ StressActivation.radius N.endpoint δ₂) : StressActivation.FromReference.f N T κ δ₁ p = StressActivation.FromReference.f N T κ δ₂ p

theorem NavierStokes.ActivationBounds.NaturalOverlap.U_independent (N : ReferencePath.Input) {T δ₁ δ₂ : ℝ} (hT : 0 < T) (hδ₁ : 0 < δ₁) (hδ₁R : 2 * δ₁ < ReferencePath.rampLimit) (hδ₂ : 0 < δ₂) (hδ₂R : 2 * δ₂ < ReferencePath.rampLimit) (κ : ℝ) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hp₁ : p.1 ≤ StressActivation.radius N.endpoint δ₁) (hp₂ : p.1 ≤ StressActivation.radius N.endpoint δ₂) : StressActivation.FromReference.U N T κ δ₁ p = StressActivation.FromReference.U N T κ δ₂ p

theorem NavierStokes.ActivationBounds.NaturalOverlap.histories_independent (N : ReferencePath.Input) {T δ₁ δ₂ : ℝ} (hT : 0 < T) (hδ₁ : 0 < δ₁) (hδ₁R : 2 * δ₁ < ReferencePath.rampLimit) (hδ₂ : 0 < δ₂) (hδ₂R : 2 * δ₂ < ReferencePath.rampLimit) (κ : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (r : StressActivation.HistoryRow) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 ≤ p.1) (hp₁ : p.1 ≤ StressActivation.radius N.endpoint δ₁) (hp₂ : p.1 ≤ StressActivation.radius N.endpoint δ₂) : StressActivation.profileHistory (StressActivation.FromReference.histories N hT hδ₁ hδ₁R κ P0 hP0) r p = StressActivation.profileHistory (StressActivation.FromReference.histories N hT hδ₂ hδ₂R κ P0 hP0) r p

Equality is from the axis up to the comparison radius, so all recomputed histories are equal, not just their endpoint fields.

theorem NavierStokes.ActivationBounds.NaturalOverlap.reference_histories_independent (N : ReferencePath.Input) {δ₁ δ₂ : ℝ} (hδ₁ : 0 < δ₁) (hδ₁R : 2 * δ₁ < ReferencePath.rampLimit) (hδ₂ : 0 < δ₂) (hδ₂R : 2 * δ₂ < ReferencePath.rampLimit) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (r : StressActivation.HistoryRow) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 ≤ p.1) (hp₁ : p.1 ≤ StressActivation.radius N.endpoint δ₁) (hp₂ : p.1 ≤ StressActivation.radius N.endpoint δ₂) : StressActivation.profileHistory (N.histories hδ₁ hδ₁R P0 hP0) r p = StressActivation.profileHistory (N.histories hδ₂ hδ₂R P0 hP0) r p

theorem NavierStokes.ActivationBounds.NaturalOverlap.radius_mono (N : ReferencePath.Input) {s t : ℝ} (hst : s ≤ t) : StressActivation.radius N.endpoint s ≤ StressActivation.radius N.endpoint t

theorem NavierStokes.ActivationBounds.NaturalOverlap.fixed_history_scaled_factor (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδR : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (r : StressActivation.HistoryRow) (u : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : StressActivation.profileHistory (StressActivation.FromReference.histories N hT hδ hδR κ P0 hP0) r (StressActivation.radius N.endpoint (T * u), η) - StressActivation.profileHistory (N.histories hδ hδR P0 hP0) r (StressActivation.radius N.endpoint (T * u), η) = scaledDistance ((κ, T), u, η) * historyErrorFactor N.endpoint (StressActivation.FromReference.refLog N δ) (StressActivation.FromReference.refAxial N δ) r ((κ, T), u, η)

theorem NavierStokes.ActivationBounds.NaturalOverlap.diagonal_history_scaled_factor (N : ReferencePath.Input) {T δ0 : ℝ} (hT : 0 < T) (hTR : 2 * T < ReferencePath.rampLimit) (hδ0 : 0 < δ0) (hδ0R : 2 * δ0 < ReferencePath.rampLimit) (hTδ0 : T ≤ δ0) (κ : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (r : StressActivation.HistoryRow) {u η : ℝ} (hu : u ∈ Set.Icc 0 1) (hη : η ∈ ReferencePath.parameterInterval) : StressActivation.profileHistory (StressActivation.FromReference.histories N hT hT hTR κ P0 hP0) r (StressActivation.radius N.endpoint (T * u), η) - StressActivation.profileHistory (N.histories hT hTR P0 hP0) r (StressActivation.radius N.endpoint (T * u), η) = scaledDistance ((κ, T), u, η) * historyErrorFactor N.endpoint (StressActivation.FromReference.refLog N δ0) (StressActivation.FromReference.refAxial N δ0) r ((κ, T), u, η)

The manuscript uses the same width for ACT and REF. Its first-ramp histories have the fixed-reference factors whenever T ≤ δ0.

theorem NavierStokes.ActivationBounds.NaturalOverlap.diagonal_histories_uniform_jets (N : ReferencePath.Input) {δ0 : ℝ} (hδ0 : 0 < δ0) (hδ0R : 2 * δ0 < ReferencePath.rampLimit) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ ReferencePath.parameterInterval) (r : StressActivation.HistoryRow) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (T : ℝ) (hT : T ∈ Set.Ioc 0 δ0) (hTR : 2 * T < ReferencePath.rampLimit), ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => StressActivation.profileHistory (StressActivation.FromReference.histories N ⋯ ⋯ hTR κ P0 hP0) r (StressActivation.radius N.endpoint y, ξ) - StressActivation.profileHistory (N.histories ⋯ hTR P0 hP0) r (StressActivation.radius N.endpoint y, ξ)) η| ≤ M * y * StressActivation.activation T κ y

noncomputable def NavierStokes.ActivationStocks.massFlux (h X η M Mη : ℝ) : ℝ

Mass flux, given by X - 2 * NaturalAxisData.D h * η * M - NaturalAxisData.d η * Mη.

Equations

• NavierStokes.ActivationStocks.massFlux h X η M Mη = X - 2 * NavierStokes.NaturalAxisData.D h * η * M - NavierStokes.NaturalAxisData.d η * Mη

noncomputable def NavierStokes.ActivationStocks.angularRemainder (h η I Iη J Jη : ℝ) : ℝ

Angular remainder, given by (1 - h) * I - NaturalAxisData.D h * η * Iη - NaturalAxisData.d η * Jη + 2 * (h - NaturalAxisData.D h) * η * J.

Equations

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

noncomputable def NavierStokes.ActivationStocks.stockOne (h X η f M Mη I Iη J Jη : ℝ) : ℝ

Stock one, given by (-massFlux h X η M Mη + angularRemainder h η I Iη J Jη / (2 * X * f)) / NaturalAxisData.L h η.

Equations

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

noncomputable def NavierStokes.ActivationStocks.stockTwo (h X η f U M Mη S Sη P Pη : ℝ) : ℝ

Stock two as an element of ℝ.

Equations

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

noncomputable def NavierStokes.ActivationStocks.profileStockOne {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : ℝ

Profile stock one, given by p.1 * P.angularLag h p / NaturalAxisData.L h p.2.

Equations

• NavierStokes.ActivationStocks.profileStockOne P h p = p.1 * P.angularLag h p / NavierStokes.NaturalAxisData.L h p.2

noncomputable def NavierStokes.ActivationStocks.profileStockTwo {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : ℝ

Profile stock two, given by p.1 * P.axialLag h p / (NaturalAxisData.L h p.2 * P.E p).

Equations

• NavierStokes.ActivationStocks.profileStockTwo P h p = p.1 * P.axialLag h p / (NavierStokes.NaturalAxisData.L h p.2 * P.E p)

theorem NavierStokes.ActivationStocks.profile_massFlux {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) : p.1 * P.W h p = massFlux h p.1 p.2 (P.M p) (ProfileHistories.parameterPartial P.M p)

theorem NavierStokes.ActivationStocks.profileStockOne_eq {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : p.1 ≠ 0) (hf : P.f p ≠ 0) : profileStockOne P h p = stockOne h p.1 p.2 (P.f p) (P.M p) (ProfileHistories.parameterPartial P.M p) (P.I p) (ProfileHistories.parameterPartial P.I p) (P.J p) (ProfileHistories.parameterPartial P.J p)

theorem NavierStokes.ActivationStocks.profileStockTwo_eq {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) : profileStockTwo P h p = stockTwo h p.1 p.2 (P.f p) (P.U p) (P.M p) (ProfileHistories.parameterPartial P.M p) (P.S p) (ProfileHistories.parameterPartial P.S p) (P.pressure p) (ProfileHistories.parameterPartial P.pressure p)

structure NavierStokes.ActivationStocks.SmoothPair {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : Set E) (w : E → ℝ) : Type u_1

Two actual smooth values with an explicitly constructed smooth factor for their difference. The following algebra constructs new factors.

• actual : E → ℝ

  Actual of SmoothPair, of type E → ℝ.

• reference : E → ℝ

  Reference of SmoothPair, of type E → ℝ.

• factor : E → ℝ

  Factor of SmoothPair, of type E → ℝ.

• actual_smooth : ContDiffOn ℝ (↑⊤) self.actual Ω
• reference_smooth : ContDiffOn ℝ (↑⊤) self.reference Ω
• factor_smooth : ContDiffOn ℝ (↑⊤) self.factor Ω
• difference (p : E) : p ∈ Ω → self.actual p - self.reference p = w p * self.factor p

noncomputable def NavierStokes.ActivationStocks.SmoothPair.common {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set E} {w : E → ℝ} (F : E → ℝ) (hF : ContDiffOn ℝ (↑⊤) F Ω) : SmoothPair Ω w

Common, bundling actual, reference, factor, actual_smooth and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActivationStocks.SmoothPair.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set E} {w : E → ℝ} (A B : SmoothPair Ω w) : SmoothPair Ω w

Add, bundling actual, reference, factor, actual_smooth and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActivationStocks.SmoothPair.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set E} {w : E → ℝ} (A : SmoothPair Ω w) : SmoothPair Ω w

Neg, bundling actual, reference, factor, actual_smooth and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActivationStocks.SmoothPair.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set E} {w : E → ℝ} (A B : SmoothPair Ω w) : SmoothPair Ω w

Sub, given by A.add B.neg.

Equations

• A.sub B = A.add B.neg

noncomputable def NavierStokes.ActivationStocks.SmoothPair.mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set E} {w : E → ℝ} (A B : SmoothPair Ω w) : SmoothPair Ω w

Mul, bundling actual, reference, factor, actual_smooth and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActivationStocks.SmoothPair.inv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set E} {w : E → ℝ} (A : SmoothPair Ω w) (ha : ∀ p ∈ Ω, A.actual p ≠ 0) (hr : ∀ p ∈ Ω, A.reference p ≠ 0) : SmoothPair Ω w

Inv, bundling actual, reference, factor, actual_smooth and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActivationStocks.SmoothPair.div {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set E} {w : E → ℝ} (A B : SmoothPair Ω w) (ha : ∀ p ∈ Ω, B.actual p ≠ 0) (hr : ∀ p ∈ Ω, B.reference p ≠ 0) : SmoothPair Ω w

Div, given by A.mul (B.inv ha hr).

Equations

• A.div B ha hr = A.mul (B.inv ha hr)

noncomputable def NavierStokes.ActivationStocks.etaD (F : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Eta D, given by deriv (fun η => F (p.1, η)) p.2.

Equations

• NavierStokes.ActivationStocks.etaD F p = deriv (fun (η : ℝ) => F (p.1, η)) p.2

theorem NavierStokes.ActivationStocks.etaD_eq_parameterPartial {D : ProfileHistories.RadialDomain} {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) : etaD F p = ProfileHistories.parameterPartial F p

noncomputable def NavierStokes.ActivationStocks.logViewOne (h X0 : ℝ) (f : ProfileHistories.Field) (H : StressActivation.HistoryRow → ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Log view one, constructed using stockOne.

Equations

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

noncomputable def NavierStokes.ActivationStocks.logViewTwo (h X0 : ℝ) (f U : ProfileHistories.Field) (H : StressActivation.HistoryRow → ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Log view two, constructed using stockTwo.

Equations

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

theorem NavierStokes.ActivationStocks.etaD_history_identity {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : StressActivation.HistoryRow) {J : Set ℝ} (hJ : IsOpen J) {X y η : ℝ} (hη : η ∈ J) {H : ProfileHistories.Field} (hmem : (X, η) ∈ D.carrier) (heq : ∀ ξ ∈ J, H (y, ξ) = StressActivation.profileHistory P r (X, ξ)) : etaD H (y, η) = ProfileHistories.parameterPartial (StressActivation.profileHistory P r) (X, η)

theorem NavierStokes.ActivationStocks.profileStockOne_logView {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h X0 : ℝ) {J : Set ℝ} (hJ : IsOpen J) {p : ProfileHistories.Point} (hη : p.2 ∈ J) (hmem : (StressActivation.radius X0 p.1, p.2) ∈ D.carrier) (hX : StressActivation.radius X0 p.1 ≠ 0) {f : ProfileHistories.Field} {H : StressActivation.HistoryRow → ProfileHistories.Field} (hfield : f p = P.f (StressActivation.radius X0 p.1, p.2)) (hf : f p ≠ 0) (hH : ∀ (r : StressActivation.HistoryRow), ∀ ξ ∈ J, H r (p.1, ξ) = StressActivation.profileHistory P r (StressActivation.radius X0 p.1, ξ)) : profileStockOne P h (StressActivation.radius X0 p.1, p.2) = logViewOne h X0 f H p

theorem NavierStokes.ActivationStocks.profileStockTwo_logView {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h X0 : ℝ) {J : Set ℝ} (hJ : IsOpen J) {p : ProfileHistories.Point} (hη : p.2 ∈ J) (hmem : (StressActivation.radius X0 p.1, p.2) ∈ D.carrier) (hX : 0 < StressActivation.radius X0 p.1) {f U : ProfileHistories.Field} {H : StressActivation.HistoryRow → ProfileHistories.Field} (hfield : f p = P.f (StressActivation.radius X0 p.1, p.2)) (hU : U p = P.U (StressActivation.radius X0 p.1, p.2)) (hH : ∀ (r : StressActivation.HistoryRow), ∀ ξ ∈ J, H r (p.1, ξ) = StressActivation.profileHistory P r (StressActivation.radius X0 p.1, ξ)) : profileStockTwo P h (StressActivation.radius X0 p.1, p.2) = logViewTwo h X0 f U H p

noncomputable def NavierStokes.ActivationStocks.FromReference.initial (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) : StressActivation.HistoryRow → ℝ → ℝ

Initial, defined pointwise by profileHistory (N.histories hδ hδT P0 hP0) r (N.endpoint, η).

Equations

• NavierStokes.ActivationStocks.FromReference.initial N hδ hδT P0 hP0 r η = NavierStokes.StressActivation.profileHistory (N.histories hδ hδT P0 hP0) r (N.endpoint, η)

theorem NavierStokes.ActivationStocks.FromReference.initial_smooth (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (r : StressActivation.HistoryRow) : ContDiffOn ℝ (↑⊤) (initial N hδ hδT P0 hP0 r) ReferencePath.parameterInterval

theorem NavierStokes.ActivationStocks.FromReference.actual_stockOne_logView (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ h : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : profileStockOne (StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0) h (StressActivation.radius N.endpoint y, η) = logViewOne h N.endpoint (StressActivation.activatedAngular T κ (StressActivation.FromReference.refLog N δ)) (StressActivation.logHistory N.endpoint (initial N hδ hδT P0 hP0) (StressActivation.activatedAngular T κ (StressActivation.FromReference.refLog N δ)) (StressActivation.controlled T κ (StressActivation.FromReference.refAxial N δ))) (y, η)

theorem NavierStokes.ActivationStocks.FromReference.actual_stockTwo_logView (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ h : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : profileStockTwo (StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0) h (StressActivation.radius N.endpoint y, η) = logViewTwo h N.endpoint (StressActivation.activatedAngular T κ (StressActivation.FromReference.refLog N δ)) (StressActivation.controlled T κ (StressActivation.FromReference.refAxial N δ)) (StressActivation.logHistory N.endpoint (initial N hδ hδT P0 hP0) (StressActivation.activatedAngular T κ (StressActivation.FromReference.refLog N δ)) (StressActivation.controlled T κ (StressActivation.FromReference.refAxial N δ))) (y, η)

theorem NavierStokes.ActivationStocks.FromReference.reference_stockOne_logView (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (h : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : profileStockOne (N.histories hδ hδT P0 hP0) h (StressActivation.radius N.endpoint y, η) = logViewOne h N.endpoint (StressActivation.referenceAngular (StressActivation.FromReference.refLog N δ)) (StressActivation.logHistory N.endpoint (initial N hδ hδT P0 hP0) (StressActivation.referenceAngular (StressActivation.FromReference.refLog N δ)) (StressActivation.FromReference.refAxial N δ)) (y, η)

theorem NavierStokes.ActivationStocks.FromReference.reference_stockTwo_logView (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (h : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : profileStockTwo (N.histories hδ hδT P0 hP0) h (StressActivation.radius N.endpoint y, η) = logViewTwo h N.endpoint (StressActivation.referenceAngular (StressActivation.FromReference.refLog N δ)) (StressActivation.FromReference.refAxial N δ) (StressActivation.logHistory N.endpoint (initial N hδ hδT P0 hP0) (StressActivation.referenceAngular (StressActivation.FromReference.refLog N δ)) (StressActivation.FromReference.refAxial N δ)) (y, η)

@[reducible, inline]

abbrev NavierStokes.ActivationStocks.StockPair (J : Set ℝ) : Type

Stock pair: an abbreviation for SmoothPair (scaledDomain J) scaledDistance.

Equations

• NavierStokes.ActivationStocks.StockPair J = NavierStokes.ActivationStocks.SmoothPair (NavierStokes.ActivationBounds.scaledDomain J) NavierStokes.ActivationBounds.scaledDistance

noncomputable def NavierStokes.ActivationStocks.etaPair {J : Set ℝ} (hJ : IsOpen J) (A : StockPair J) : StockPair J

Parameter differentiation preserves the same flat-distance factor.

Equations

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

theorem NavierStokes.ActivationStocks.etaPair_actual_eq {J : Set ℝ} (hJ : IsOpen J) (A : StockPair J) (F : ProfileHistories.Field) (κ T u : ℝ) {η : ℝ} (hη : η ∈ J) (heq : ∀ ξ ∈ J, A.actual ((κ, T), u, ξ) = F (T * u, ξ)) : (etaPair hJ A).actual ((κ, T), u, η) = etaD F (T * u, η)

theorem NavierStokes.ActivationStocks.etaPair_reference_eq {J : Set ℝ} (hJ : IsOpen J) (A : StockPair J) (F : ProfileHistories.Field) (κ T u : ℝ) {η : ℝ} (hη : η ∈ J) (heq : ∀ ξ ∈ J, A.reference ((κ, T), u, ξ) = F (T * u, ξ)) : (etaPair hJ A).reference ((κ, T), u, η) = etaD F (T * u, η)

noncomputable def NavierStokes.ActivationStocks.controlledPair {J : Set ℝ} (hJ : IsOpen J) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) : StockPair J

Controlled pair, bundling actual, reference, factor, actual_smooth and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActivationStocks.angularPair {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) : StockPair J

Angular pair, bundling actual, reference, factor, actual_smooth and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActivationStocks.historyPair (X0 : ℝ) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (r : StressActivation.HistoryRow) : StockPair J

History pair, bundling actual, reference, factor, actual_smooth and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActivationStocks.historyPair_actual_eq (X0 : ℝ) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) {T : ℝ} (hT : T ≠ 0) (κ : ℝ) (r : StressActivation.HistoryRow) (u : ℝ) {η : ℝ} (hη : η ∈ J) : (historyPair X0 initial hJ hL hU hi r).actual ((κ, T), u, η) = StressActivation.logHistory X0 initial (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U) r (T * u, η)

theorem NavierStokes.ActivationStocks.angularPair_actual_eq {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) {T : ℝ} (hT : T ≠ 0) (κ u : ℝ) {η : ℝ} (hη : η ∈ J) : (angularPair hJ hL).actual ((κ, T), u, η) = StressActivation.activatedAngular T κ L (T * u, η)

noncomputable def NavierStokes.ActivationStocks.scaledRadius (X0 : ℝ) (q : ActivationBounds.ScaledPoint) : ℝ

Scaled radius, given by radius X0 (q.1.2 * q.2.1).

Equations

• NavierStokes.ActivationStocks.scaledRadius X0 q = NavierStokes.StressActivation.radius X0 (q.1.2 * q.2.1)

theorem NavierStokes.ActivationStocks.scaledRadius_smooth (X0 : ℝ) : ContDiff ℝ (↑⊤) (scaledRadius X0)

theorem NavierStokes.ActivationStocks.scaledRadius_pos {X0 : ℝ} (hX0 : 0 < X0) (q : ActivationBounds.ScaledPoint) : 0 < scaledRadius X0 q

noncomputable def NavierStokes.ActivationStocks.constantPair (J : Set ℝ) (c : ℝ) : StockPair J

Constant pair, given by SmoothPair.common (fun _ => c) contDiffOn_const.

Equations

• NavierStokes.ActivationStocks.constantPair J c = NavierStokes.ActivationStocks.SmoothPair.common (fun (x : NavierStokes.ActivationBounds.ScaledPoint) => c) ⋯

noncomputable def NavierStokes.ActivationStocks.parameterPair (J : Set ℝ) (g : ℝ → ℝ) (hg : ContDiff ℝ (↑⊤) g) : StockPair J

Parameter pair, given by SmoothPair.common (fun q => g q.2.2) (hg.comp contDiff_snd.snd).contDiffOn.

Equations

• NavierStokes.ActivationStocks.parameterPair J g hg = NavierStokes.ActivationStocks.SmoothPair.common (fun (q : NavierStokes.ActivationBounds.ScaledPoint) => g q.2.2) ⋯

noncomputable def NavierStokes.ActivationStocks.radiusPair (J : Set ℝ) (X0 : ℝ) : StockPair J

Radius pair, given by SmoothPair.common (scaledRadius X0) (scaledRadius_smooth X0).contDiffOn.

Equations

• NavierStokes.ActivationStocks.radiusPair J X0 = NavierStokes.ActivationStocks.SmoothPair.common (NavierStokes.ActivationStocks.scaledRadius X0) ⋯

noncomputable def NavierStokes.ActivationStocks.sqrtRadiusPair (J : Set ℝ) {X0 : ℝ} (hX0 : 0 < X0) : StockPair J

Sqrt radius pair, constructed using SmoothPair.common.

Equations

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

noncomputable def NavierStokes.ActivationStocks.dPair (J : Set ℝ) : StockPair J

D pair, given by parameterPair J NaturalAxisData.d (contDiff_const.sub (contDiff_id.pow 2)).

Equations

• NavierStokes.ActivationStocks.dPair J = NavierStokes.ActivationStocks.parameterPair J NavierStokes.NaturalAxisData.d NavierStokes.ActivationStocks.dPair._proof_1

noncomputable def NavierStokes.ActivationStocks.lPair (J : Set ℝ) (h : ℝ) : StockPair J

L pair, given by parameterPair J (NaturalAxisData.L h) (contDiff_const.sub (contDiff_const.mul (contDiff_id.pow 2))).

Equations

• NavierStokes.ActivationStocks.lPair J h = NavierStokes.ActivationStocks.parameterPair J (NavierStokes.NaturalAxisData.L h) ⋯

noncomputable def NavierStokes.ActivationStocks.etaPairCommon (J : Set ℝ) : StockPair J

Eta pair common, given by parameterPair J id contDiff_id.

Equations

• NavierStokes.ActivationStocks.etaPairCommon J = NavierStokes.ActivationStocks.parameterPair J id NavierStokes.ActivationStocks.etaPairCommon._proof_1

noncomputable def NavierStokes.ActivationStocks.massFluxPair {J : Set ℝ} (h X0 : ℝ) (H Hη : StressActivation.HistoryRow → StockPair J) : StockPair J

Mass flux pair as an element of StockPair J.

Equations

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

noncomputable def NavierStokes.ActivationStocks.angularRemainderPair {J : Set ℝ} (h : ℝ) (H Hη : StressActivation.HistoryRow → StockPair J) : StockPair J

Angular remainder pair as an element of StockPair J.

Equations

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

noncomputable def NavierStokes.ActivationStocks.stockOnePair {J : Set ℝ} (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) (F : StockPair J) (H Hη : StressActivation.HistoryRow → StockPair J) (hfa : ∀ q ∈ ActivationBounds.scaledDomain J, F.actual q ≠ 0) (hfr : ∀ q ∈ ActivationBounds.scaledDomain J, F.reference q ≠ 0) : StockPair J

Stock one pair as an element of StockPair J.

Equations

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

noncomputable def NavierStokes.ActivationStocks.stockTwoPair {J : Set ℝ} (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) (F U : StockPair J) (H Hη : StressActivation.HistoryRow → StockPair J) (hfa : ∀ q ∈ ActivationBounds.scaledDomain J, F.actual q ≠ 0) (hfr : ∀ q ∈ ActivationBounds.scaledDomain J, F.reference q ≠ 0) : StockPair J

Stock two pair as an element of StockPair J.

Equations

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

theorem NavierStokes.ActivationStocks.stockOnePair_actual {J : Set ℝ} (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) (F : StockPair J) (H Hη : StressActivation.HistoryRow → StockPair J) (hfa : ∀ q ∈ ActivationBounds.scaledDomain J, F.actual q ≠ 0) (hfr : ∀ q ∈ ActivationBounds.scaledDomain J, F.reference q ≠ 0) (q : ActivationBounds.ScaledPoint) : (stockOnePair h hX0 hcoef F H Hη hfa hfr).actual q = stockOne h (scaledRadius X0 q) q.2.2 (F.actual q) ((H StressActivation.HistoryRow.mass).actual q) ((Hη StressActivation.HistoryRow.mass).actual q) ((H StressActivation.HistoryRow.angular).actual q) ((Hη StressActivation.HistoryRow.angular).actual q) ((H StressActivation.HistoryRow.transport).actual q) ((Hη StressActivation.HistoryRow.transport).actual q)

theorem NavierStokes.ActivationStocks.stockOnePair_reference {J : Set ℝ} (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) (F : StockPair J) (H Hη : StressActivation.HistoryRow → StockPair J) (hfa : ∀ q ∈ ActivationBounds.scaledDomain J, F.actual q ≠ 0) (hfr : ∀ q ∈ ActivationBounds.scaledDomain J, F.reference q ≠ 0) (q : ActivationBounds.ScaledPoint) : (stockOnePair h hX0 hcoef F H Hη hfa hfr).reference q = stockOne h (scaledRadius X0 q) q.2.2 (F.reference q) ((H StressActivation.HistoryRow.mass).reference q) ((Hη StressActivation.HistoryRow.mass).reference q) ((H StressActivation.HistoryRow.angular).reference q) ((Hη StressActivation.HistoryRow.angular).reference q) ((H StressActivation.HistoryRow.transport).reference q) ((Hη StressActivation.HistoryRow.transport).reference q)

theorem NavierStokes.ActivationStocks.stockTwoPair_actual {J : Set ℝ} (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) (F U : StockPair J) (H Hη : StressActivation.HistoryRow → StockPair J) (hfa : ∀ q ∈ ActivationBounds.scaledDomain J, F.actual q ≠ 0) (hfr : ∀ q ∈ ActivationBounds.scaledDomain J, F.reference q ≠ 0) (q : ActivationBounds.ScaledPoint) : (stockTwoPair h hX0 hcoef F U H Hη hfa hfr).actual q = stockTwo h (scaledRadius X0 q) q.2.2 (F.actual q) (U.actual q) ((H StressActivation.HistoryRow.mass).actual q) ((Hη StressActivation.HistoryRow.mass).actual q) ((H StressActivation.HistoryRow.energy).actual q) ((Hη StressActivation.HistoryRow.energy).actual q) ((H StressActivation.HistoryRow.pressure).actual q) ((Hη StressActivation.HistoryRow.pressure).actual q)

theorem NavierStokes.ActivationStocks.stockTwoPair_reference {J : Set ℝ} (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) (F U : StockPair J) (H Hη : StressActivation.HistoryRow → StockPair J) (hfa : ∀ q ∈ ActivationBounds.scaledDomain J, F.actual q ≠ 0) (hfr : ∀ q ∈ ActivationBounds.scaledDomain J, F.reference q ≠ 0) (q : ActivationBounds.ScaledPoint) : (stockTwoPair h hX0 hcoef F U H Hη hfa hfr).reference q = stockTwo h (scaledRadius X0 q) q.2.2 (F.reference q) (U.reference q) ((H StressActivation.HistoryRow.mass).reference q) ((Hη StressActivation.HistoryRow.mass).reference q) ((H StressActivation.HistoryRow.energy).reference q) ((Hη StressActivation.HistoryRow.energy).reference q) ((H StressActivation.HistoryRow.pressure).reference q) ((Hη StressActivation.HistoryRow.pressure).reference q)

noncomputable def NavierStokes.ActivationStocks.activationOnePair (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) : StockPair J

Activation one pair, constructed using stockOnePair.

Equations

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

noncomputable def NavierStokes.ActivationStocks.activationTwoPair (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) : StockPair J

Activation two pair, constructed using stockTwoPair.

Equations

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

theorem NavierStokes.ActivationStocks.historyEtaPair_actual {X0 : ℝ} (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) {T : ℝ} (hT : T ≠ 0) (κ u : ℝ) {η : ℝ} (hη : η ∈ J) (r : StressActivation.HistoryRow) : (etaPair hJ (historyPair X0 initial hJ hL hU hi r)).actual ((κ, T), u, η) = etaD (StressActivation.logHistory X0 initial (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U) r) (T * u, η)

theorem NavierStokes.ActivationStocks.historyEtaPair_reference {X0 : ℝ} (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (q : ActivationBounds.ScaledPoint) (r : StressActivation.HistoryRow) : (etaPair hJ (historyPair X0 initial hJ hL hU hi r)).reference q = etaD (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U r) (q.1.2 * q.2.1, q.2.2)

theorem NavierStokes.ActivationStocks.activationOnePair_actual (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) {T : ℝ} (hT : T ≠ 0) (κ u : ℝ) {η : ℝ} (hη : η ∈ J) : (activationOnePair h hX0 initial hJ hL hU hi hcoef).actual ((κ, T), u, η) = logViewOne h X0 (StressActivation.activatedAngular T κ L) (StressActivation.logHistory X0 initial (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U)) (T * u, η)

theorem NavierStokes.ActivationStocks.activationOnePair_reference (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) (q : ActivationBounds.ScaledPoint) : (activationOnePair h hX0 initial hJ hL hU hi hcoef).reference q = logViewOne h X0 (StressActivation.referenceAngular L) (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U) (q.1.2 * q.2.1, q.2.2)

theorem NavierStokes.ActivationStocks.activationTwoPair_actual (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) {T : ℝ} (hT : T ≠ 0) (κ u : ℝ) {η : ℝ} (hη : η ∈ J) : (activationTwoPair h hX0 initial hJ hL hU hi hcoef).actual ((κ, T), u, η) = logViewTwo h X0 (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U) (StressActivation.logHistory X0 initial (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U)) (T * u, η)

theorem NavierStokes.ActivationStocks.activationTwoPair_reference (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) (q : ActivationBounds.ScaledPoint) : (activationTwoPair h hX0 initial hJ hL hU hi hcoef).reference q = logViewTwo h X0 (StressActivation.referenceAngular L) U (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U) (q.1.2 * q.2.1, q.2.2)

theorem NavierStokes.ActivationStocks.exists_log_stock_factors (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) : ∃ (P : ActivationBounds.ScaledPoint → ℝ) (Q : ActivationBounds.ScaledPoint → ℝ), ContDiffOn ℝ (↑⊤) P (ActivationBounds.scaledDomain J) ∧ ContDiffOn ℝ (↑⊤) Q (ActivationBounds.scaledDomain J) ∧ ∀ (T : ℝ), T ≠ 0 → ∀ (κ u η : ℝ), η ∈ J → logViewOne h X0 (StressActivation.activatedAngular T κ L) (StressActivation.logHistory X0 initial (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U)) (T * u, η) - logViewOne h X0 (StressActivation.referenceAngular L) (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U) (T * u, η) = ActivationBounds.scaledDistance ((κ, T), u, η) * P ((κ, T), u, η) ∧ logViewTwo h X0 (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U) (StressActivation.logHistory X0 initial (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U)) (T * u, η) - logViewTwo h X0 (StressActivation.referenceAngular L) U (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U) (T * u, η) = ActivationBounds.scaledDistance ((κ, T), u, η) * Q ((κ, T), u, η)

Both stock errors have actual smooth factors on a domain containing the zero-width face. The input hypotheses concern only fields, initial history values, and the nonzero coordinate coefficient.

theorem NavierStokes.ActivationStocks.activationOnePair_zero (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) (κ u : ℝ) {η : ℝ} (hη : η ∈ J) : (activationOnePair h hX0 initial hJ hL hU hi hcoef).actual ((κ, 0), u, η) = (activationOnePair h hX0 initial hJ hL hU hi hcoef).reference ((κ, 0), u, η)

theorem NavierStokes.ActivationStocks.activationTwoPair_zero (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) (κ u : ℝ) {η : ℝ} (hη : η ∈ J) : (activationTwoPair h hX0 initial hJ hL hU hi hcoef).actual ((κ, 0), u, η) = (activationTwoPair h hX0 initial hJ hL hU hi hcoef).reference ((κ, 0), u, η)

theorem NavierStokes.ActivationStocks.log_stocks_uniform_jets (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ J) (T0 : ℝ) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ T ∈ Set.Ioc 0 T0, ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => logViewOne h X0 (StressActivation.activatedAngular T κ L) (StressActivation.logHistory X0 initial (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U)) (y, ξ) - logViewOne h X0 (StressActivation.referenceAngular L) (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U) (y, ξ)) η| ≤ M * y * StressActivation.activation T κ y ∧ |iteratedDeriv n (fun (ξ : ℝ) => logViewTwo h X0 (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U) (StressActivation.logHistory X0 initial (StressActivation.activatedAngular T κ L) (StressActivation.controlled T κ U)) (y, ξ) - logViewTwo h X0 (StressActivation.referenceAngular L) U (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U) (y, ξ)) η| ≤ M * y * StressActivation.activation T κ y

theorem NavierStokes.ActivationStocks.FromReference.exists_physical_stock_factors (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (h : ℝ) (hcoef : ∀ η ∈ ReferencePath.parameterInterval, NaturalAxisData.L h η ≠ 0) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) : ∃ (P : ActivationBounds.ScaledPoint → ℝ) (Q : ActivationBounds.ScaledPoint → ℝ), ContDiffOn ℝ (↑⊤) P (ActivationBounds.scaledDomain ReferencePath.parameterInterval) ∧ ContDiffOn ℝ (↑⊤) Q (ActivationBounds.scaledDomain ReferencePath.parameterInterval) ∧ ∀ (T : ℝ) (hT : 0 < T) (κ u η : ℝ), η ∈ ReferencePath.parameterInterval → profileStockOne (StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0) h (StressActivation.radius N.endpoint (T * u), η) - profileStockOne (N.histories hδ hδT P0 hP0) h (StressActivation.radius N.endpoint (T * u), η) = ActivationBounds.scaledDistance ((κ, T), u, η) * P ((κ, T), u, η) ∧ profileStockTwo (StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0) h (StressActivation.radius N.endpoint (T * u), η) - profileStockTwo (N.histories hδ hδT P0 hP0) h (StressActivation.radius N.endpoint (T * u), η) = ActivationBounds.scaledDistance ((κ, T), u, η) * Q ((κ, T), u, η)

The factors concern the actual recomputed ACT and REF lag histories. Their common scaled domain contains T=0.

theorem NavierStokes.ActivationStocks.FromReference.physical_stocks_uniform_bound (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (h : ℝ) (hcoef : ∀ η ∈ ReferencePath.parameterInterval, NaturalAxisData.L h η ≠ 0) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (T0 : ℝ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (T : ℝ) (hT : 0 < T), T ≤ T0 → ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ Set.Icc (-1) 1, |profileStockOne (StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0) h (StressActivation.radius N.endpoint y, η) - profileStockOne (N.histories hδ hδT P0 hP0) h (StressActivation.radius N.endpoint y, η)| ≤ M * y * StressActivation.activation T κ y ∧ |profileStockTwo (StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0) h (StressActivation.radius N.endpoint y, η) - profileStockTwo (N.histories hδ hδT P0 hP0) h (StressActivation.radius N.endpoint y, η)| ≤ M * y * StressActivation.activation T κ y

One constant controls both actual stock errors for every sufficiently small positive width and all activation parameters, including κ=0.

Agreement of the reference stocks with the natural stress-free stocks

theorem NavierStokes.ActivationStocks.profileHistory_congr_across {D E : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles E) (r : StressActivation.HistoryRow) {X η : ℝ} (hX : 0 ≤ X) (h0 : StressActivation.profileInitial P r η = StressActivation.profileInitial Q r η) (hf : ∀ x ∈ Set.Icc 0 X, P.f (x, η) = Q.f (x, η)) (hu : ∀ x ∈ Set.Icc 0 X, P.U (x, η) = Q.U (x, η)) : StressActivation.profileHistory P r (X, η) = StressActivation.profileHistory Q r (X, η)

theorem NavierStokes.ActivationStocks.profiles_stocks_congr {D E : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles E) (h : ℝ) {J : Set ℝ} (hJ : IsOpen J) {X η : ℝ} (hη : η ∈ J) (hp : (X, η) ∈ D.carrier) (hq : (X, η) ∈ E.carrier) (hX : 0 < X) (hf : P.f (X, η) = Q.f (X, η)) (hfne : Q.f (X, η) ≠ 0) (hu : P.U (X, η) = Q.U (X, η)) (hH : ∀ (r : StressActivation.HistoryRow), ∀ ξ ∈ J, StressActivation.profileHistory P r (X, ξ) = StressActivation.profileHistory Q r (X, ξ)) : profileStockOne P h (X, η) = profileStockOne Q h (X, η) ∧ profileStockTwo P h (X, η) = profileStockTwo Q h (X, η)

noncomputable def NavierStokes.ActivationStocks.naturalDomain {Λ : ℝ} (hΛ : 0 < Λ) : ProfileHistories.RadialDomain

Natural domain, bundling carrier, isOpen, scale_mem.

Equations

• NavierStokes.ActivationStocks.naturalDomain hΛ = { carrier := NavierStokes.NaturalProfile.domain Λ, isOpen := ⋯, scale_mem := ⋯ }

noncomputable def NavierStokes.ActivationStocks.naturalHistories {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) : ProfileHistories.Profiles (naturalDomain hΛ)

Natural histories, bundling f, U, f_smooth, U_smooth and the required compatibility proofs.

Equations

• NavierStokes.ActivationStocks.naturalHistories F hΛ hP0 = { f := F.f, U := F.U, f_smooth := ⋯, U_smooth := ⋯, pressure0 := P0, pressure0_smooth := ⋯ }

theorem NavierStokes.ActivationStocks.radialPartial_natural_field {Λ : ℝ} (hΛ : 0 < Λ) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (NaturalProfile.domain Λ)) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : ProfileHistories.radialPartial G p = NaturalAxisBridge.partialY G p

theorem NavierStokes.ActivationStocks.parameterPartial_natural_field {Λ : ℝ} (hΛ : 0 < Λ) {G : ProfileHistories.Field} (hG : ContDiffOn ℝ (↑⊤) G (NaturalProfile.domain Λ)) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : ProfileHistories.parameterPartial G p = NaturalAxisBridge.partialEta G p

theorem NavierStokes.ActivationStocks.naturalHistories_average {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : (naturalHistories F hΛ hP0).Ubar p = F.Ubar p

theorem NavierStokes.ActivationStocks.naturalHistories_pressure {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : (naturalHistories F hΛ hP0).pressure p = F.Pi p

theorem NavierStokes.ActivationStocks.naturalHistories_average_derivative {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : ProfileHistories.parameterPartial (naturalHistories F hΛ hP0).Ubar p = NaturalAxisBridge.partialEta F.Ubar p

theorem NavierStokes.ActivationStocks.naturalHistories_pressure_derivative {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : ProfileHistories.parameterPartial (naturalHistories F hΛ hP0).pressure p = NaturalAxisBridge.partialEta F.Pi p

theorem NavierStokes.ActivationStocks.naturalHistories_W {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : (naturalHistories F hΛ hP0).W h p = NaturalProfile.transportW h F.Ubar p

theorem NavierStokes.ActivationStocks.naturalHistories_angularSource {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) (hf : F.f p ≠ 0) : (naturalHistories F hΛ hP0).angularSource h p = 2 * p.1 * F.f p * NaturalEntrance.Sq h F.f F.U F.Ubar p

theorem NavierStokes.ActivationStocks.naturalHistories_axialSource {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) : (naturalHistories F hΛ hP0).axialSource h p = NaturalEntrance.Sn h F.U F.Ubar F.Pi p

theorem NavierStokes.ActivationStocks.naturalHistories_stocks {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {p : ProfileHistories.Point} (hp : p ∈ NaturalProfile.domain Λ) (hX : 0 < p.1) (hL : NaturalAxisData.L h p.2 ≠ 0) (hf : ∀ x ∈ Set.uIcc 0 p.1, F.f (x, p.2) ≠ 0) : profileStockOne (naturalHistories F hΛ hP0) h p = NaturalEntrance.p1 F.f p ∧ profileStockTwo (naturalHistories F hΛ hP0) h p = NaturalEntrance.p2 F.f F.U p

theorem NavierStokes.ActivationStocks.reference_stocks_natural {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hsmall : NaturalAxisData.SmallParameters h j) (y : ℝ) (hy : y ≤ δ) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : have N := ReferencePath.Input.ofNatural hΛ F; have p := N.fromLog (y, η); profileStockOne (N.histories hδ hδT P0 hP0) h p = NaturalEntrance.p1 F.f p ∧ profileStockTwo (N.histories hδ hδT P0 hP0) h p = NaturalEntrance.p2 F.f F.U p

On the full natural part of REF, including its endpoint, the actual integral-defined stocks equal the stress-free derivative coordinates. The proof transfers all five history rows and their genuine parameter derivatives from the natural solution.