Actual initial stress activation

The activation integrates damped genuine reference derivatives. Error factors are constructed from the flat primitive integral, never supplied as input.

noncomputable def NavierStokes.StressActivation.logDomain (J : Set ℝ) (hJ : IsOpen J) : ProfileHistories.RadialDomain

Log domain, bundling carrier, isOpen, scale_mem.

Equations

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

noncomputable def NavierStokes.StressActivation.activation (T κ y : ℝ) : ℝ

Activation, given by (1 - κ) * OutgoingSchedule.sigma (y / T).

Equations

• NavierStokes.StressActivation.activation T κ y = (1 - κ) * NavierStokes.OutgoingSchedule.sigma (y / T)

noncomputable def NavierStokes.StressActivation.damping (T κ y : ℝ) : ℝ

Damping, given by 1 - activation T κ y.

Equations

• NavierStokes.StressActivation.damping T κ y = 1 - NavierStokes.StressActivation.activation T κ y

theorem NavierStokes.StressActivation.activation_smooth (T κ : ℝ) : ContDiff ℝ (↑⊤) (activation T κ)

theorem NavierStokes.StressActivation.damping_smooth (T κ : ℝ) : ContDiff ℝ (↑⊤) (damping T κ)

theorem NavierStokes.StressActivation.activation_nonneg (T κ y : ℝ) (hκ : κ ≤ 1) : 0 ≤ activation T κ y

theorem NavierStokes.StressActivation.activation_le_one (T κ y : ℝ) (hκ : κ ∈ Set.Icc 0 1) : activation T κ y ≤ 1

theorem NavierStokes.StressActivation.activation_monotone {T κ : ℝ} (hT : 0 < T) (hκ : κ ≤ 1) : Monotone (activation T κ)

theorem NavierStokes.StressActivation.activation_zero {T : ℝ} (hT : 0 < T) (κ : ℝ) {y : ℝ} (hy : y ≤ 0) : activation T κ y = 0

noncomputable def NavierStokes.StressActivation.weightedField (T κ : ℝ) (B : ProfileHistories.Field) : ProfileHistories.Field

Weighted field, defined pointwise by activation T κ p.1 * B p.

Equations

• NavierStokes.StressActivation.weightedField T κ B p = NavierStokes.StressActivation.activation T κ p.1 * B p

noncomputable def NavierStokes.StressActivation.weightedPrimitive (T κ : ℝ) (B : ProfileHistories.Field) : ProfileHistories.Field

Weighted primitive, given by primitive (weightedField T κ B).

Equations

• NavierStokes.StressActivation.weightedPrimitive T κ B = NavierStokes.ProfileHistories.primitive (NavierStokes.StressActivation.weightedField T κ B)

theorem NavierStokes.StressActivation.weightedField_smooth (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {B : ProfileHistories.Field} (hB : ContDiffOn ℝ (↑⊤) B (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (weightedField T κ B) (logDomain J hJ).carrier

theorem NavierStokes.StressActivation.weightedPrimitive_smooth (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {B : ProfileHistories.Field} (hB : ContDiffOn ℝ (↑⊤) B (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (weightedPrimitive T κ B) (logDomain J hJ).carrier

theorem NavierStokes.StressActivation.weightedPrimitive_hasDerivAt (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {B : ProfileHistories.Field} (hB : ContDiffOn ℝ (↑⊤) B (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : HasDerivAt (fun (x : ℝ) => weightedPrimitive T κ B (x, η)) (activation T κ y * B (y, η)) y

theorem NavierStokes.StressActivation.weightedPrimitive_zero {T : ℝ} (hT : 0 < T) (κ : ℝ) (B : ProfileHistories.Field) {y : ℝ} (hy : y ≤ 0) (η : ℝ) : weightedPrimitive T κ B (y, η) = 0

noncomputable def NavierStokes.StressActivation.controlled (T κ : ℝ) (F : ProfileHistories.Field) : ProfileHistories.Field

Direct integration of the reference derivative times the prescribed damping.

Equations

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

theorem NavierStokes.StressActivation.controlled_smooth (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (controlled T κ F) (logDomain J hJ).carrier

theorem NavierStokes.StressActivation.controlled_hasDerivAt (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : HasDerivAt (fun (x : ℝ) => controlled T κ F (x, η)) (damping T κ y * ProfileHistories.radialPartial F (y, η)) y

@[simp]

theorem NavierStokes.StressActivation.controlled_initial (T κ : ℝ) (F : ProfileHistories.Field) (η : ℝ) : controlled T κ F (0, η) = F (0, η)

theorem NavierStokes.StressActivation.controlled_sub (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : controlled T κ F (y, η) - F (y, η) = -weightedPrimitive T κ (ProfileHistories.radialPartial F) (y, η)

A local-parameter version of the proved flat factor theorem

theorem NavierStokes.StressActivation.flatFactor_local {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {J : Set E} (hJ : IsOpen J) {b : E × ℝ → ℝ} (hb : ContDiffOn ℝ (↑⊤) b (J ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (ParametricFlatFactor.factor c j b) (J ×ˢ Set.univ)

noncomputable def NavierStokes.StressActivation.stepDenominator (T y : ℝ) : ℝ

Step denominator, given by FlatCutoff.edge 1 (y / T) + FlatCutoff.edge 1 (1 - y / T).

Equations

• NavierStokes.StressActivation.stepDenominator T y = NavierStokes.FlatCutoff.edge 1 (y / T) + NavierStokes.FlatCutoff.edge 1 (1 - y / T)

theorem NavierStokes.StressActivation.stepDenominator_pos (T y : ℝ) : 0 < stepDenominator T y

theorem NavierStokes.StressActivation.stepDenominator_smooth (T : ℝ) : ContDiff ℝ (↑⊤) (stepDenominator T)

theorem NavierStokes.StressActivation.edge_scaled {T : ℝ} (hT : 0 < T) (y : ℝ) : FlatCutoff.edge 1 (y / T) = FlatCutoff.edge (T ^ 2) y

theorem NavierStokes.StressActivation.activation_flat_form {T : ℝ} (hT : 0 < T) (κ y : ℝ) : activation T κ y = (1 - κ) * FlatCutoff.edge (T ^ 2) y / stepDenominator T y

noncomputable def NavierStokes.StressActivation.flatCoefficient (T : ℝ) (B : ProfileHistories.Field) (q : ℝ × ℝ) : ℝ

Flat coefficient, given by B (q.2, q.1) / stepDenominator T q.2.

Equations

• NavierStokes.StressActivation.flatCoefficient T B q = B (q.2, q.1) / NavierStokes.StressActivation.stepDenominator T q.2

noncomputable def NavierStokes.StressActivation.primitiveFactor (T : ℝ) (B : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Division by y e_a is implemented by a smooth transformed integral.

Equations

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

theorem NavierStokes.StressActivation.flatCoefficient_smooth (T : ℝ) {J : Set ℝ} (hJ : IsOpen J) {B : ProfileHistories.Field} (hB : ContDiffOn ℝ (↑⊤) B (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (flatCoefficient T B) (J ×ˢ Set.univ)

theorem NavierStokes.StressActivation.primitiveFactor_smooth {T : ℝ} (hT : 0 < T) {J : Set ℝ} (hJ : IsOpen J) {B : ProfileHistories.Field} (hB : ContDiffOn ℝ (↑⊤) B (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (primitiveFactor T B) (logDomain J hJ).carrier

@[simp]

theorem NavierStokes.StressActivation.primitiveFactor_zero (T : ℝ) (B : ProfileHistories.Field) (η : ℝ) : primitiveFactor T B (0, η) = 0

theorem NavierStokes.StressActivation.weightedPrimitive_factorization {T : ℝ} (hT : 0 < T) (κ : ℝ) (B : ProfileHistories.Field) (p : ProfileHistories.Point) : weightedPrimitive T κ B p = p.1 * activation T κ p.1 * primitiveFactor T B p

theorem NavierStokes.StressActivation.weightedPrimitive_bound {T κ M y : ℝ} (hT : 0 < T) (hκ : κ ≤ 1) (hM : 0 ≤ M) (hy : 0 ≤ y) (B : ProfileHistories.Field) (η : ℝ) (hB : ∀ t ∈ Set.Icc 0 y, |B (t, η)| ≤ M) : |weightedPrimitive T κ B (y, η)| ≤ M * y * activation T κ y

The basic quantitative estimate is uniform as κ tends to zero and in the ramp length: its constant is only a bound for the reference coefficient.

theorem NavierStokes.StressActivation.controlled_difference_factorization {T : ℝ} (hT : 0 < T) (κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : controlled T κ F (y, η) - F (y, η) = y * activation T κ y * -primitiveFactor T (ProfileHistories.radialPartial F) (y, η)

theorem NavierStokes.StressActivation.weightedPrimitive_scale (T κ : ℝ) (B : ProfileHistories.Field) (p : ProfileHistories.Point) : weightedPrimitive T κ B p = (1 - κ) * weightedPrimitive T 0 B p

noncomputable def NavierStokes.StressActivation.meanExp (x : ℝ) : ℝ

Mean exp, given by average (fun p : Point => Real.exp p.1) (x, 0).

Equations

• NavierStokes.StressActivation.meanExp x = NavierStokes.ProfileHistories.average (fun (p : NavierStokes.ProfileHistories.Point) => Real.exp p.1) (x, 0)

theorem NavierStokes.StressActivation.meanExp_smooth : ContDiff ℝ (↑⊤) meanExp

theorem NavierStokes.StressActivation.exp_sub_one (x : ℝ) : Real.exp x - 1 = x * meanExp x

noncomputable def NavierStokes.StressActivation.referenceAngular (L : ProfileHistories.Field) : ProfileHistories.Field

Reference angular, defined pointwise by Real.exp (L p).

Equations

• NavierStokes.StressActivation.referenceAngular L p = Real.exp (L p)

noncomputable def NavierStokes.StressActivation.activatedAngular (T κ : ℝ) (L : ProfileHistories.Field) : ProfileHistories.Field

Activated angular, defined pointwise by Real.exp (controlled T κ L p).

Equations

• NavierStokes.StressActivation.activatedAngular T κ L p = Real.exp (NavierStokes.StressActivation.controlled T κ L p)

noncomputable def NavierStokes.StressActivation.referenceP1 (L : ProfileHistories.Field) : ProfileHistories.Field

Reference P1, defined pointwise by -2 * radialPartial L p.

Equations

• NavierStokes.StressActivation.referenceP1 L p = -2 * NavierStokes.ProfileHistories.radialPartial L p

noncomputable def NavierStokes.StressActivation.radius (X0 y : ℝ) : ℝ

Radius, given by X0 * Real.exp y.

Equations

• NavierStokes.StressActivation.radius X0 y = X0 * Real.exp y

noncomputable def NavierStokes.StressActivation.referenceNs (X0 : ℝ) (U : ProfileHistories.Field) : ProfileHistories.Field

Reference ns, defined pointwise by -2 * radialPartial U p / radius X0 p.1.

Equations

• NavierStokes.StressActivation.referenceNs X0 U p = -2 * NavierStokes.ProfileHistories.radialPartial U p / NavierStokes.StressActivation.radius X0 p.1

theorem NavierStokes.StressActivation.activatedAngular_pos (T κ : ℝ) (L : ProfileHistories.Field) (p : ProfileHistories.Point) : 0 < activatedAngular T κ L p

theorem NavierStokes.StressActivation.activatedAngular_smooth (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (activatedAngular T κ L) (logDomain J hJ).carrier

theorem NavierStokes.StressActivation.activation_angular_equation (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : HasDerivAt (fun (x : ℝ) => Real.log (activatedAngular T κ L (x, η))) (-(damping T κ y * referenceP1 L (y, η)) / 2) y

The first equation in (18), for the logarithm of the actual positive field.

theorem NavierStokes.StressActivation.activation_axial_equation (T κ : ℝ) {X0 : ℝ} (hX0 : 0 < X0) {J : Set ℝ} (hJ : IsOpen J) {U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : HasDerivAt (fun (x : ℝ) => controlled T κ U (x, η)) (-(damping T κ y * radius X0 y * referenceNs X0 U (y, η)) / 2) y

The second equation in (18), with n_s obtained from the reference field.

noncomputable def NavierStokes.StressActivation.relativeFactor (T κ : ℝ) (L : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Relative factor, given by -primitiveFactor T (radialPartial L) p * meanExp (-weightedPrimitive T κ (radialPartial L) p).

Equations

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

theorem NavierStokes.StressActivation.relativeFactor_smooth {T : ℝ} (hT : 0 < T) (κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (relativeFactor T κ L) (logDomain J hJ).carrier

@[simp]

theorem NavierStokes.StressActivation.relativeFactor_zero (T κ : ℝ) (L : ProfileHistories.Field) (η : ℝ) : relativeFactor T κ L (0, η) = 0

theorem NavierStokes.StressActivation.angular_relative_difference {T : ℝ} (hT : 0 < T) (κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : activatedAngular T κ L (y, η) / referenceAngular L (y, η) - 1 = y * activation T κ y * relativeFactor T κ L (y, η)

theorem NavierStokes.StressActivation.controlled_eq_reference_before {T : ℝ} (hT : 0 < T) (κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (logDomain J hJ).carrier) {y : ℝ} (hy : y ≤ 0) {η : ℝ} (hη : η ∈ J) : controlled T κ F (y, η) = F (y, η)

Actual parameter jets, uniformly including κ=0

@[reducible, inline]

abbrev NavierStokes.StressActivation.FamilyPoint : Type

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

Equations

• NavierStokes.StressActivation.FamilyPoint = ((ℝ × ℝ) × ℝ)

noncomputable def NavierStokes.StressActivation.relativeFamily (T : ℝ) (L : ProfileHistories.Field) (q : FamilyPoint) : ℝ

Relative family, given by relativeFactor T q.1.1 L (q.1.2, q.2).

Equations

• NavierStokes.StressActivation.relativeFamily T L q = NavierStokes.StressActivation.relativeFactor T q.1.1 L (q.1.2, q.2)

noncomputable def NavierStokes.StressActivation.differenceFamily (T : ℝ) (F : ProfileHistories.Field) (q : FamilyPoint) : ℝ

Difference family, given by -primitiveFactor T (radialPartial F) (q.1.2, q.2).

Equations

• NavierStokes.StressActivation.differenceFamily T F q = -NavierStokes.StressActivation.primitiveFactor T (NavierStokes.ProfileHistories.radialPartial F) (q.1.2, q.2)

theorem NavierStokes.StressActivation.relativeFamily_smooth {T : ℝ} (hT : 0 < T) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (relativeFamily T L) (Set.univ ×ˢ J)

theorem NavierStokes.StressActivation.differenceFamily_smooth {T : ℝ} (hT : 0 < T) {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (differenceFamily T F) (Set.univ ×ˢ J)

theorem NavierStokes.StressActivation.compact_parameter_jet_bound {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {H : FamilyPoint → ℝ} (hH : ContDiffOn ℝ (↑⊤) H (Set.univ ×ˢ J)) (T : ℝ) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => H ((κ, y), ξ)) η| ≤ M

Compactness bounds the genuine η derivatives of a jointly smooth family. In particular the compact κ range contains zero; inverse powers of κ cannot enter.

theorem NavierStokes.StressActivation.scaled_family_jet_bound {T : ℝ} (_hT : 0 < T) {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {H : FamilyPoint → ℝ} (hH : ContDiffOn ℝ (↑⊤) H (Set.univ ×ˢ J)) {E : ℝ → ℝ → ℝ → ℝ} (hE : ∀ (κ y η : ℝ), η ∈ J → E κ y η = y * activation T κ y * H ((κ, y), η)) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (E κ y) η| ≤ M * y * activation T κ y

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

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

Flat integrals of smoothly parameterized families

noncomputable def NavierStokes.StressActivation.familyFlatCoefficient (T : ℝ) (B : FamilyPoint → ℝ) (q : (ℝ × ℝ) × ℝ) : ℝ

Family flat coefficient, given by B ((q.1.1, q.2), q.1.2) / stepDenominator T q.2.

Equations

• NavierStokes.StressActivation.familyFlatCoefficient T B q = B ((q.1.1, q.2), q.1.2) / NavierStokes.StressActivation.stepDenominator T q.2

noncomputable def NavierStokes.StressActivation.familyPrimitiveFactor (T : ℝ) (B : FamilyPoint → ℝ) (q : FamilyPoint) : ℝ

Family primitive factor, given by q.1.2 ^ 2 * stepDenominator T q.1.2 * ParametricFlatFactor.factor (T ^ 2) 0 (familyFlatCoefficient T B) ((q.1.1, q.2), q.1.2).

Equations

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

theorem NavierStokes.StressActivation.familyPrimitiveFactor_eq (T : ℝ) (B : FamilyPoint → ℝ) (κ y η : ℝ) : familyPrimitiveFactor T B ((κ, y), η) = primitiveFactor T (fun (p : ProfileHistories.Point) => B ((κ, p.1), p.2)) (y, η)

theorem NavierStokes.StressActivation.familyPrimitiveFactor_smooth {T : ℝ} (hT : 0 < T) {J : Set ℝ} (hJ : IsOpen J) {B : FamilyPoint → ℝ} (hB : ContDiffOn ℝ (↑⊤) B (Set.univ ×ˢ J)) : ContDiffOn ℝ (↑⊤) (familyPrimitiveFactor T B) (Set.univ ×ˢ J)

theorem NavierStokes.StressActivation.weighted_family_parameter_jet_bounds {T : ℝ} (hT : 0 < T) {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {B : FamilyPoint → ℝ} (hB : ContDiffOn ℝ (↑⊤) B (Set.univ ×ˢ J)) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => weightedPrimitive T κ (fun (p : ProfileHistories.Point) => B ((κ, p.1), p.2)) (y, ξ)) η| ≤ M * y * activation T κ y

The five actual pressure and moment histories

inductive NavierStokes.StressActivation.HistoryRow : Type

History row data for stress activation.

• mass : HistoryRow
• angular : HistoryRow
• transport : HistoryRow
• energy : HistoryRow
• pressure : HistoryRow

noncomputable def NavierStokes.StressActivation.radialDensity : HistoryRow → ℝ → ℝ → ℝ → ℝ

These are the integrands used by ProfileHistories.Profiles.

Equations

• NavierStokes.StressActivation.radialDensity NavierStokes.StressActivation.HistoryRow.mass x✝² x✝¹ x✝ = x✝
• NavierStokes.StressActivation.radialDensity NavierStokes.StressActivation.HistoryRow.angular x✝² x✝¹ x✝ = 2 * x✝² * x✝¹
• NavierStokes.StressActivation.radialDensity NavierStokes.StressActivation.HistoryRow.transport x✝² x✝¹ x✝ = x✝ * (2 * x✝² * x✝¹)
• NavierStokes.StressActivation.radialDensity NavierStokes.StressActivation.HistoryRow.energy x✝² x✝¹ x✝ = x✝ ^ 2 - x✝² * x✝¹ ^ 2
• NavierStokes.StressActivation.radialDensity NavierStokes.StressActivation.HistoryRow.pressure x✝² x✝¹ x✝ = x✝¹ ^ 2

noncomputable def NavierStokes.StressActivation.logDensity (X0 : ℝ) (f U : ProfileHistories.Field) (r : HistoryRow) : ProfileHistories.Field

The Jacobian X converts the physical radial histories to log time.

Equations

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

noncomputable def NavierStokes.StressActivation.logHistory (X0 : ℝ) (initial : HistoryRow → ℝ → ℝ) (f U : ProfileHistories.Field) (r : HistoryRow) : ProfileHistories.Field

The initial row values are shared; every subsequent value is recomputed.

Equations

• NavierStokes.StressActivation.logHistory X0 initial f U r p = initial r p.2 + NavierStokes.ProfileHistories.primitive (NavierStokes.StressActivation.logDensity X0 f U r) p

theorem NavierStokes.StressActivation.radius_smooth (X0 : ℝ) : ContDiff ℝ (↑⊤) (radius X0)

theorem NavierStokes.StressActivation.logDensity_smooth (X0 : ℝ) {J : Set ℝ} (hJ : IsOpen J) {f U : ProfileHistories.Field} (hf : ContDiffOn ℝ (↑⊤) f (logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (r : HistoryRow) : ContDiffOn ℝ (↑⊤) (logDensity X0 f U r) (logDomain J hJ).carrier

theorem NavierStokes.StressActivation.logHistory_smooth (X0 : ℝ) (initial : HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {f U : ProfileHistories.Field} (hf : ContDiffOn ℝ (↑⊤) f (logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (r : HistoryRow) (hi : ContDiffOn ℝ (↑⊤) (initial r) J) : ContDiffOn ℝ (↑⊤) (logHistory X0 initial f U r) (logDomain J hJ).carrier

@[simp]

theorem NavierStokes.StressActivation.logHistory_initial (X0 : ℝ) (initial : HistoryRow → ℝ → ℝ) (f U : ProfileHistories.Field) (r : HistoryRow) (η : ℝ) : logHistory X0 initial f U r (0, η) = initial r η

noncomputable def NavierStokes.StressActivation.fieldFamily (F : ProfileHistories.Field) (q : FamilyPoint) : ℝ

Field family, given by F (q.1.2, q.2).

Equations

• NavierStokes.StressActivation.fieldFamily F q = F (q.1.2, q.2)

theorem NavierStokes.StressActivation.fieldFamily_smooth {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (fieldFamily F) (Set.univ ×ˢ J)

noncomputable def NavierStokes.StressActivation.controlledFamily (T : ℝ) (F : ProfileHistories.Field) (q : FamilyPoint) : ℝ

Controlled family, given by controlled T q.1.1 F (q.1.2, q.2).

Equations

• NavierStokes.StressActivation.controlledFamily T F q = NavierStokes.StressActivation.controlled T q.1.1 F (q.1.2, q.2)

theorem NavierStokes.StressActivation.controlledFamily_smooth (T : ℝ) {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (controlledFamily T F) (Set.univ ×ˢ J)

noncomputable def NavierStokes.StressActivation.angularFamily (T : ℝ) (L : ProfileHistories.Field) (q : FamilyPoint) : ℝ

Angular family, given by activatedAngular T q.1.1 L (q.1.2, q.2).

Equations

• NavierStokes.StressActivation.angularFamily T L q = NavierStokes.StressActivation.activatedAngular T q.1.1 L (q.1.2, q.2)

theorem NavierStokes.StressActivation.angularFamily_smooth (T : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (angularFamily T L) (Set.univ ×ˢ J)

noncomputable def NavierStokes.StressActivation.angularDifferenceFamily (T : ℝ) (L : ProfileHistories.Field) (q : FamilyPoint) : ℝ

Angular difference family, given by fieldFamily (referenceAngular L) q * relativeFamily T L q.

Equations

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

theorem NavierStokes.StressActivation.angularDifferenceFamily_smooth {T : ℝ} (hT : 0 < T) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (angularDifferenceFamily T L) (Set.univ ×ˢ J)

theorem NavierStokes.StressActivation.angular_difference_factorization {T : ℝ} (hT : 0 < T) (κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : activatedAngular T κ L (y, η) - referenceAngular L (y, η) = y * activation T κ y * angularDifferenceFamily T L ((κ, y), η)

noncomputable def NavierStokes.StressActivation.densityDifferenceFamily (T X0 : ℝ) (L U : ProfileHistories.Field) (r : HistoryRow) (q : FamilyPoint) : ℝ

Density difference family as an element of ℝ.

Equations

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

theorem NavierStokes.StressActivation.densityDifferenceFamily_smooth {T : ℝ} (hT : 0 < T) (X0 : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (r : HistoryRow) : ContDiffOn ℝ (↑⊤) (densityDifferenceFamily T X0 L U r) (Set.univ ×ˢ J)

theorem NavierStokes.StressActivation.density_difference_factorization {T : ℝ} (hT : 0 < T) (κ X0 : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (r : HistoryRow) (y : ℝ) {η : ℝ} (hη : η ∈ J) : logDensity X0 (activatedAngular T κ L) (controlled T κ U) r (y, η) - logDensity X0 (referenceAngular L) U r (y, η) = y * activation T κ y * densityDifferenceFamily T X0 L U r ((κ, y), η)

noncomputable def NavierStokes.StressActivation.historyIntegrandFamily (T X0 : ℝ) (L U : ProfileHistories.Field) (r : HistoryRow) (q : FamilyPoint) : ℝ

History integrand family, given by q.1.2 * densityDifferenceFamily T X0 L U r q.

Equations

• NavierStokes.StressActivation.historyIntegrandFamily T X0 L U r q = q.1.2 * NavierStokes.StressActivation.densityDifferenceFamily T X0 L U r q

theorem NavierStokes.StressActivation.historyIntegrandFamily_smooth {T : ℝ} (hT : 0 < T) (X0 : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (r : HistoryRow) : ContDiffOn ℝ (↑⊤) (historyIntegrandFamily T X0 L U r) (Set.univ ×ˢ J)

theorem NavierStokes.StressActivation.history_difference_integral {T : ℝ} (hT : 0 < T) (κ X0 : ℝ) (initial : HistoryRow → ℝ → ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (r : HistoryRow) (y : ℝ) {η : ℝ} (hη : η ∈ J) : logHistory X0 initial (activatedAngular T κ L) (controlled T κ U) r (y, η) - logHistory X0 initial (referenceAngular L) U r (y, η) = weightedPrimitive T κ (fun (p : ProfileHistories.Point) => historyIntegrandFamily T X0 L U r ((κ, p.1), p.2)) (y, η)

noncomputable def NavierStokes.StressActivation.historyDifferenceFamily (T X0 : ℝ) (L U : ProfileHistories.Field) (r : HistoryRow) : FamilyPoint → ℝ

History difference family, given by familyPrimitiveFactor T (historyIntegrandFamily T X0 L U r).

Equations

• NavierStokes.StressActivation.historyDifferenceFamily T X0 L U r = NavierStokes.StressActivation.familyPrimitiveFactor T (NavierStokes.StressActivation.historyIntegrandFamily T X0 L U r)

theorem NavierStokes.StressActivation.historyDifferenceFamily_smooth {T : ℝ} (hT : 0 < T) (X0 : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (r : HistoryRow) : ContDiffOn ℝ (↑⊤) (historyDifferenceFamily T X0 L U r) (Set.univ ×ˢ J)

@[simp]

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

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

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

Identification with the physical ProfileHistories integrals

noncomputable def NavierStokes.StressActivation.profileDensity {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : HistoryRow) : ProfileHistories.Field

Profile density, defined pointwise by radialDensity r p.1 (P.f p) (P.U p).

Equations

• NavierStokes.StressActivation.profileDensity P r p = NavierStokes.StressActivation.radialDensity r p.1 (P.f p) (P.U p)

noncomputable def NavierStokes.StressActivation.profileHistory {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) : HistoryRow → ProfileHistories.Field

Profile history as an element of HistoryRow → Field | .mass => P.M | .angular => P.I | .transport => P.J | .energy => P.S | .pressure => P.pressure.

Equations

• NavierStokes.StressActivation.profileHistory P NavierStokes.StressActivation.HistoryRow.mass = P.M
• NavierStokes.StressActivation.profileHistory P NavierStokes.StressActivation.HistoryRow.angular = P.I
• NavierStokes.StressActivation.profileHistory P NavierStokes.StressActivation.HistoryRow.transport = P.J
• NavierStokes.StressActivation.profileHistory P NavierStokes.StressActivation.HistoryRow.energy = P.S
• NavierStokes.StressActivation.profileHistory P NavierStokes.StressActivation.HistoryRow.pressure = P.pressure

noncomputable def NavierStokes.StressActivation.profileInitial {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) : HistoryRow → ℝ → ℝ

Profile initial as an element of HistoryRow → ℝ → ℝ | .pressure => P.pressure0 | _ => fun _ => 0.

Equations

• NavierStokes.StressActivation.profileInitial P NavierStokes.StressActivation.HistoryRow.pressure = P.pressure0
• NavierStokes.StressActivation.profileInitial P x✝ = fun (x : ℝ) => 0

theorem NavierStokes.StressActivation.profileHistory_eq_initial_add_primitive {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : HistoryRow) (p : ProfileHistories.Point) : profileHistory P r p = profileInitial P r p.2 + ProfileHistories.primitive (profileDensity P r) p

theorem NavierStokes.StressActivation.profileDensity_smooth {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : HistoryRow) : ContDiffOn ℝ (↑⊤) (profileDensity P r) D.carrier

theorem NavierStokes.StressActivation.profileHistory_smooth {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : HistoryRow) : ContDiffOn ℝ (↑⊤) (profileHistory P r) D.carrier

theorem NavierStokes.StressActivation.profileHistory_hasDerivAt {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : HistoryRow) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) : HasDerivAt (fun (x : ℝ) => profileHistory P r (x, p.2)) (profileDensity P r p) p.1

noncomputable def NavierStokes.StressActivation.logPullback (X0 : ℝ) (F : ProfileHistories.Field) : ProfileHistories.Field

Log pullback, defined pointwise by F (radius X0 p.1, p.2).

Equations

• NavierStokes.StressActivation.logPullback X0 F p = F (NavierStokes.StressActivation.radius X0 p.1, p.2)

theorem NavierStokes.StressActivation.radius_hasDerivAt (X0 y : ℝ) : HasDerivAt (radius X0) (radius X0 y) y

theorem NavierStokes.StressActivation.profileHistory_log_integral {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (X0 : ℝ) (r : HistoryRow) (y η : ℝ) (hmem : ∀ (t : ℝ), (radius X0 t, η) ∈ D.carrier) : logHistory X0 (fun (s : HistoryRow) (ξ : ℝ) => profileHistory P s (X0, ξ)) (logPullback X0 P.f) (logPullback X0 P.U) r (y, η) = profileHistory P r (radius X0 y, η)

The change to log radius is proved by differentiating the actual physical history. This includes the pressure constant and all four moment histories.

theorem NavierStokes.StressActivation.profileHistory_congr_up_to {D : ProfileHistories.RadialDomain} (P Q : ProfileHistories.Profiles D) (r : HistoryRow) {X η : ℝ} (hX : 0 ≤ X) (h0 : profileInitial P r η = 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, η)) : profileHistory P r (X, η) = profileHistory Q r (X, η)

theorem NavierStokes.StressActivation.logHistory_congr_slice (X0 : ℝ) (initial₁ initial₂ : HistoryRow → ℝ → ℝ) (f₁ U₁ f₂ U₂ : ProfileHistories.Field) (r : HistoryRow) (y η : ℝ) (hi : initial₁ r η = initial₂ r η) (hf : ∀ (t : ℝ), f₁ (t, η) = f₂ (t, η)) (hu : ∀ (t : ℝ), U₁ (t, η) = U₂ (t, η)) : logHistory X0 initial₁ f₁ U₁ r (y, η) = logHistory X0 initial₂ f₂ U₂ r (y, η)

Attaching the actual ramp to the proved natural reference path

noncomputable def NavierStokes.StressActivation.FromReference.refLog (N : ReferencePath.Input) (δ : ℝ) : ProfileHistories.Field

Ref log, given by ReferencePath.continuation δ N.logF.

Equations

• NavierStokes.StressActivation.FromReference.refLog N δ = NavierStokes.ReferencePath.continuation δ N.logF

noncomputable def NavierStokes.StressActivation.FromReference.refAxial (N : ReferencePath.Input) (δ : ℝ) : ProfileHistories.Field

Ref axial, given by ReferencePath.continuation δ N.logU.

Equations

• NavierStokes.StressActivation.FromReference.refAxial N δ = NavierStokes.ReferencePath.continuation δ N.logU

theorem NavierStokes.StressActivation.FromReference.refLog_smooth (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) : ContDiffOn ℝ (↑⊤) (refLog N δ) (logDomain ReferencePath.parameterInterval ReferencePath.parameterInterval_open).carrier

theorem NavierStokes.StressActivation.FromReference.refAxial_smooth (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) : ContDiffOn ℝ (↑⊤) (refAxial N δ) (logDomain ReferencePath.parameterInterval ReferencePath.parameterInterval_open).carrier

noncomputable def NavierStokes.StressActivation.FromReference.f (N : ReferencePath.Input) (T κ δ : ℝ) : ProfileHistories.Field

F, defined pointwise by if p.1 ≤ N.endpoint then N.refF δ p else activatedAngular T κ (refLog N δ) (N.logTime p.1, p.2).

Equations

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

noncomputable def NavierStokes.StressActivation.FromReference.U (N : ReferencePath.Input) (T κ δ : ℝ) : ProfileHistories.Field

U, defined pointwise by if p.1 ≤ N.endpoint then N.refU δ p else controlled T κ (refAxial N δ) (N.logTime p.1, p.2).

Equations

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

theorem NavierStokes.StressActivation.FromReference.f_eq_reference (N : ReferencePath.Input) (T κ δ : ℝ) {p : ProfileHistories.Point} (hp : p.1 ≤ N.endpoint) : f N T κ δ p = N.refF δ p

theorem NavierStokes.StressActivation.FromReference.U_eq_reference (N : ReferencePath.Input) (T κ δ : ℝ) {p : ProfileHistories.Point} (hp : p.1 ≤ N.endpoint) : U N T κ δ p = N.refU δ p

theorem NavierStokes.StressActivation.FromReference.f_eq_logtime (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 < p.1) : f N T κ δ p = activatedAngular T κ (refLog N δ) (N.logTime p.1, p.2)

theorem NavierStokes.StressActivation.FromReference.U_eq_logtime (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 < p.1) : U N T κ δ p = controlled T κ (refAxial N δ) (N.logTime p.1, p.2)

theorem NavierStokes.StressActivation.FromReference.f_smooth (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) : ContDiffOn ℝ (↑⊤) (f N T κ δ) N.radialDomain.carrier

theorem NavierStokes.StressActivation.FromReference.U_smooth (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) : ContDiffOn ℝ (↑⊤) (U N T κ δ) N.radialDomain.carrier

theorem NavierStokes.StressActivation.FromReference.f_pos (N : ReferencePath.Input) (T κ δ : ℝ) {p : ProfileHistories.Point} (hp : p ∈ N.radialDomain.carrier) (hX : 0 ≤ p.1) : 0 < f N T κ δ p

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

These are the actual radial pressure and lag inputs, recomputed from ACT.

Equations

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

theorem NavierStokes.StressActivation.FromReference.histories_initial (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (r : HistoryRow) (η : ℝ) : profileHistory (histories N hT hδ hδT κ P0 hP0) r (N.endpoint, η) = profileHistory (N.histories hδ hδT P0 hP0) r (N.endpoint, η)

theorem NavierStokes.StressActivation.FromReference.log_radius_mem (N : ReferencePath.Input) (y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : (radius N.endpoint y, η) ∈ N.radialDomain.carrier

theorem NavierStokes.StressActivation.FromReference.f_logPullback (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : logPullback N.endpoint (f N T κ δ) (y, η) = activatedAngular T κ (refLog N δ) (y, η)

theorem NavierStokes.StressActivation.FromReference.U_logPullback (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : logPullback N.endpoint (U N T κ δ) (y, η) = controlled T κ (refAxial N δ) (y, η)

theorem NavierStokes.StressActivation.FromReference.refF_logPullback (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : logPullback N.endpoint (N.refF δ) (y, η) = referenceAngular (refLog N δ) (y, η)

theorem NavierStokes.StressActivation.FromReference.refU_logPullback (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : logPullback N.endpoint (N.refU δ) (y, η) = refAxial N δ (y, η)

theorem NavierStokes.StressActivation.FromReference.histories_log_formula (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (r : HistoryRow) (y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : profileHistory (histories N hT hδ hδT κ P0 hP0) r (radius N.endpoint y, η) = logHistory N.endpoint (fun (s : HistoryRow) (ξ : ℝ) => profileHistory (N.histories hδ hδT P0 hP0) s (N.endpoint, ξ)) (activatedAngular T κ (refLog N δ)) (controlled T κ (refAxial N δ)) r (y, η)

theorem NavierStokes.StressActivation.FromReference.reference_histories_log_formula (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (r : HistoryRow) (y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : profileHistory (N.histories hδ hδT P0 hP0) r (radius N.endpoint y, η) = logHistory N.endpoint (fun (s : HistoryRow) (ξ : ℝ) => profileHistory (N.histories hδ hδT P0 hP0) s (N.endpoint, ξ)) (referenceAngular (refLog N δ)) (refAxial N δ) r (y, η)

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

The five physical histories inherit the constructed smooth factor.

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

theorem NavierStokes.StressActivation.FromReference.angular_equation (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : HasDerivAt (fun (t : ℝ) => Real.log (f N T κ δ (radius N.endpoint t, η))) (-(damping T κ y * referenceP1 (refLog N δ) (y, η)) / 2) y

theorem NavierStokes.StressActivation.FromReference.axial_equation (N : ReferencePath.Input) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ y : ℝ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : HasDerivAt (fun (t : ℝ) => U N T κ δ (radius N.endpoint t, η)) (-(damping T κ y * radius N.endpoint y * referenceNs N.endpoint (refAxial N δ) (y, η)) / 2) y

Exact shear identities and cancellation of the common damping

noncomputable def NavierStokes.StressActivation.actualP1 (T κ : ℝ) (L : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Actual P1, given by -2 * deriv (fun y => Real.log (activatedAngular T κ L (y, p.2))) p.1.

Equations

• NavierStokes.StressActivation.actualP1 T κ L p = -2 * deriv (fun (y : ℝ) => Real.log (NavierStokes.StressActivation.activatedAngular T κ L (y, p.2))) p.1

noncomputable def NavierStokes.StressActivation.velocity (X0 : ℝ) (f : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Velocity, given by Real.sqrt (2 * radius X0 p.1) * f p.

Equations

• NavierStokes.StressActivation.velocity X0 f p = √(2 * NavierStokes.StressActivation.radius X0 p.1) * f p

noncomputable def NavierStokes.StressActivation.referenceP2 (X0 : ℝ) (L U : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Reference P2, given by -2 * radialPartial U p / velocity X0 (referenceAngular L) p.

Equations

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

noncomputable def NavierStokes.StressActivation.actualP2 (T κ X0 : ℝ) (L U : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Actual P2, given by -2 * deriv (fun y => controlled T κ U (y, p.2)) p.1 / velocity X0 (activatedAngular T κ L) p.

Equations

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

noncomputable def NavierStokes.StressActivation.shearSlope (T κ X0 : ℝ) (L U : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Shear slope, given by actualP2 T κ X0 L U p / actualP1 T κ L p.

Equations

• NavierStokes.StressActivation.shearSlope T κ X0 L U p = NavierStokes.StressActivation.actualP2 T κ X0 L U p / NavierStokes.StressActivation.actualP1 T κ L p

noncomputable def NavierStokes.StressActivation.shearSize (T κ X0 : ℝ) (L U : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Shear size, given by actualP1 T κ L p + actualP2 T κ X0 L U p ^ 2 / actualP1 T κ L p.

Equations

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

noncomputable def NavierStokes.StressActivation.referenceSize (X0 : ℝ) (L U : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Reference size, given by referenceP1 L p + referenceP2 X0 L U p ^ 2 / referenceP1 L p.

Equations

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

theorem NavierStokes.StressActivation.damping_ge (T κ y : ℝ) (hκ : κ ≤ 1) : κ ≤ damping T κ y

theorem NavierStokes.StressActivation.damping_pos (T κ y : ℝ) (hκ : κ ∈ Set.Ioc 0 1) : 0 < damping T κ y

theorem NavierStokes.StressActivation.actualP1_eq (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : actualP1 T κ L (y, η) = damping T κ y * referenceP1 L (y, η)

theorem NavierStokes.StressActivation.actualP1_pos (T : ℝ) {κ : ℝ} (hκ : κ ∈ Set.Ioc 0 1) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) (hp : 0 < referenceP1 L (y, η)) : 0 < actualP1 T κ L (y, η)

theorem NavierStokes.StressActivation.actualP2_eq (T κ : ℝ) {X0 : ℝ} (hX0 : 0 < X0) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : actualP2 T κ X0 L U (y, η) = damping T κ y * referenceP2 X0 L U (y, η) * (referenceAngular L (y, η) / activatedAngular T κ L (y, η))

theorem NavierStokes.StressActivation.shearSlope_eq (T : ℝ) {κ X0 : ℝ} (hκ : κ ∈ Set.Ioc 0 1) (hX0 : 0 < X0) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) (hp : referenceP1 L (y, η) ≠ 0) : shearSlope T κ X0 L U (y, η) = referenceP2 X0 L U (y, η) / referenceP1 L (y, η) * (referenceAngular L (y, η) / activatedAngular T κ L (y, η))

The reference shear ratio contains no inverse power of the damping.

theorem NavierStokes.StressActivation.shearSize_error (T : ℝ) {κ X0 : ℝ} (hκ : κ ∈ Set.Ioc 0 1) (hX0 : 0 < X0) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) (hp : referenceP1 L (y, η) ≠ 0) : shearSize T κ X0 L U (y, η) - damping T κ y * referenceSize X0 L U (y, η) = damping T κ y * (referenceP2 X0 L U (y, η) ^ 2 / referenceP1 L (y, η)) * ((referenceAngular L (y, η) / activatedAngular T κ L (y, η)) ^ 2 - 1)

theorem NavierStokes.StressActivation.controlled_bound {T κ M y : ℝ} (hT : 0 < T) (hκ : κ ≤ 1) (hM : 0 ≤ M) (hy : 0 ≤ y) {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (logDomain J hJ).carrier) {η : ℝ} (hη : η ∈ J) (hB : ∀ t ∈ Set.Icc 0 y, |ProfileHistories.radialPartial F (t, η)| ≤ M) : |controlled T κ F (y, η) - F (y, η)| ≤ M * y * activation T κ y