One flat weight on the active annulus

The logarithmic edge distances carry their actual exponential coefficients. The global estimates are obtained from smooth edge factors and compactness.

noncomputable def NavierStokes.ActiveAnnulusWeight.weight (c a b y : ℝ) : ℝ

Weight, given by FlatCutoff.edge c (y-a) * FlatCutoff.edge 4 (b-y).

Equations

• NavierStokes.ActiveAnnulusWeight.weight c a b y = NavierStokes.FlatCutoff.edge c (y - a) * NavierStokes.FlatCutoff.edge 4 (b - y)

noncomputable def NavierStokes.ActiveAnnulusWeight.edgeDistance (a b y : ℝ) : ℝ

Edge distance, given by min 1 (min (y-a) (b-y)).

Equations

• NavierStokes.ActiveAnnulusWeight.edgeDistance a b y = min 1 (min (y - a) (b - y))

noncomputable def NavierStokes.ActiveAnnulusWeight.radialWeight (c a b X : ℝ) : ℝ

Radial weight, with branches according to 0 < X.

Equations

• NavierStokes.ActiveAnnulusWeight.radialWeight c a b X = if 0 < X then NavierStokes.ActiveAnnulusWeight.weight c a b (Real.log X) else 0

theorem NavierStokes.ActiveAnnulusWeight.edge_le_one {c : ℝ} (hc : 0 ≤ c) (x : ℝ) : FlatCutoff.edge c x ≤ 1

theorem NavierStokes.ActiveAnnulusWeight.edge_mono_pos {c x y : ℝ} (hc : 0 ≤ c) (hx : 0 < x) (hxy : x ≤ y) : FlatCutoff.edge c x ≤ FlatCutoff.edge c y

theorem NavierStokes.ActiveAnnulusWeight.weight_nonneg (c a b y : ℝ) : 0 ≤ weight c a b y

theorem NavierStokes.ActiveAnnulusWeight.weight_pos {c a b y : ℝ} (hy : y ∈ Set.Ioo a b) : 0 < weight c a b y

theorem NavierStokes.ActiveAnnulusWeight.weight_zero_left (c b : ℝ) {a y : ℝ} (hy : y ≤ a) : weight c a b y = 0

theorem NavierStokes.ActiveAnnulusWeight.weight_zero_right (c a : ℝ) {b y : ℝ} (hy : b ≤ y) : weight c a b y = 0

theorem NavierStokes.ActiveAnnulusWeight.weight_le_left (c a b y : ℝ) : weight c a b y ≤ FlatCutoff.edge c (y - a)

theorem NavierStokes.ActiveAnnulusWeight.weight_le_right {c : ℝ} (hc : 0 ≤ c) (a b y : ℝ) : weight c a b y ≤ FlatCutoff.edge 4 (b - y)

theorem NavierStokes.ActiveAnnulusWeight.weight_le_one {c : ℝ} (hc : 0 ≤ c) (a b y : ℝ) : weight c a b y ≤ 1

theorem NavierStokes.ActiveAnnulusWeight.weight_smooth {c : ℝ} (hc : 0 < c) (a b : ℝ) : ContDiff ℝ (↑⊤) (weight c a b)

theorem NavierStokes.ActiveAnnulusWeight.edgeDistance_pos {a b y : ℝ} (hy : y ∈ Set.Ioo a b) : 0 < edgeDistance a b y

theorem NavierStokes.ActiveAnnulusWeight.edgeDistance_le_one (a b y : ℝ) : edgeDistance a b y ≤ 1

theorem NavierStokes.ActiveAnnulusWeight.edgeDistance_le_left (a b y : ℝ) : edgeDistance a b y ≤ y - a

theorem NavierStokes.ActiveAnnulusWeight.edgeDistance_le_right (a b y : ℝ) : edgeDistance a b y ≤ b - y

theorem NavierStokes.ActiveAnnulusWeight.iteratedDeriv_zero_function (n : ℕ) : (iteratedDeriv n fun (x : ℝ) => 0) = fun (x : ℝ) => 0

theorem NavierStokes.ActiveAnnulusWeight.flat_left_of_zero {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) {a : ℝ} (hz : ∀ x < a, f x = 0) (n : ℕ) : iteratedDeriv n f a = 0

theorem NavierStokes.ActiveAnnulusWeight.flat_right_of_zero {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) {b : ℝ} (hz : ∀ (x : ℝ), b < x → f x = 0) (n : ℕ) : iteratedDeriv n f b = 0

theorem NavierStokes.ActiveAnnulusWeight.weight_flat_left {c : ℝ} (hc : 0 < c) (a b : ℝ) (n : ℕ) : iteratedDeriv n (weight c a b) a = 0

theorem NavierStokes.ActiveAnnulusWeight.weight_flat_right {c : ℝ} (hc : 0 < c) (a b : ℝ) (n : ℕ) : iteratedDeriv n (weight c a b) b = 0

theorem NavierStokes.ActiveAnnulusWeight.radialWeight_zero_left (c b : ℝ) {a X : ℝ} (hX : X ≤ Real.exp a) : radialWeight c a b X = 0

theorem NavierStokes.ActiveAnnulusWeight.radialWeight_zero_right (c a : ℝ) {b X : ℝ} (hX : Real.exp b ≤ X) : radialWeight c a b X = 0

theorem NavierStokes.ActiveAnnulusWeight.radialWeight_pos {c a b X : ℝ} (hX : X ∈ Set.Ioo (Real.exp a) (Real.exp b)) : 0 < radialWeight c a b X

theorem NavierStokes.ActiveAnnulusWeight.radialWeight_smooth {c : ℝ} (hc : 0 < c) (a b : ℝ) : ContDiff ℝ (↑⊤) (radialWeight c a b)

theorem NavierStokes.ActiveAnnulusWeight.radialWeight_flat_left {c : ℝ} (hc : 0 < c) (a b : ℝ) (n : ℕ) : iteratedDeriv n (radialWeight c a b) (Real.exp a) = 0

theorem NavierStokes.ActiveAnnulusWeight.radialWeight_flat_right {c : ℝ} (hc : 0 < c) (a b : ℝ) (n : ℕ) : iteratedDeriv n (radialWeight c a b) (Real.exp b) = 0

theorem NavierStokes.ActiveAnnulusWeight.weight_lower_middle {c a b d y : ℝ} (hc : 0 ≤ c) (hd : 0 < d) (hy : y ∈ Set.Icc (a + d) (b - d)) : FlatCutoff.edge c d * FlatCutoff.edge 4 d ≤ weight c a b y

theorem NavierStokes.ActiveAnnulusWeight.weight_compare_left {c a b d y : ℝ} (hd : 0 < b - a - d) (hy : y ≤ a + d) : FlatCutoff.edge c (y - a) ≤ weight c a b y / FlatCutoff.edge 4 (b - a - d)

theorem NavierStokes.ActiveAnnulusWeight.weight_compare_right {c a b d y : ℝ} (hc : 0 ≤ c) (hd : 0 < b - a - d) (hy : b - d ≤ y) : FlatCutoff.edge 4 (b - y) ≤ weight c a b y / FlatCutoff.edge c (b - a - d)

theorem NavierStokes.ActiveAnnulusWeight.distance_power_le_left {a b y : ℝ} (hy : y ∈ Set.Ioo a b) {n N : ℕ} (hn : n ≤ N) : edgeDistance a b y ^ N ≤ (y - a) ^ n

theorem NavierStokes.ActiveAnnulusWeight.distance_power_le_right {a b y : ℝ} (hy : y ∈ Set.Ioo a b) {n N : ℕ} (hn : n ≤ N) : edgeDistance a b y ^ N ≤ (b - y) ^ n

theorem NavierStokes.ActiveAnnulusWeight.left_bound_to_weight {c a b d y C : ℝ} (hC : 0 ≤ C) (hd : 0 < b - a - d) (hy : y ∈ Set.Ioo a b) (hyl : y ≤ a + d) {n N : ℕ} (hn : n ≤ N) : C * FlatCutoff.edge c (y - a) / (y - a) ^ n ≤ C / FlatCutoff.edge 4 (b - a - d) * weight c a b y / edgeDistance a b y ^ N

theorem NavierStokes.ActiveAnnulusWeight.right_bound_to_weight {c a b d y C : ℝ} (hc : 0 ≤ c) (hC : 0 ≤ C) (hd : 0 < b - a - d) (hy : y ∈ Set.Ioo a b) (hyr : b - d ≤ y) {n N : ℕ} (hn : n ≤ N) : C * FlatCutoff.edge 4 (b - y) / (b - y) ^ n ≤ C / FlatCutoff.edge c (b - a - d) * weight c a b y / edgeDistance a b y ^ N

theorem NavierStokes.ActiveAnnulusWeight.interior_bound_to_weight {c a b d y C : ℝ} (hc : 0 ≤ c) (hC : 0 ≤ C) (hd : 0 < d) (hy : y ∈ Set.Ioo a b) (hym : y ∈ Set.Icc (a + d) (b - d)) (N : ℕ) : C ≤ C / (FlatCutoff.edge c d * FlatCutoff.edge 4 d) * weight c a b y / edgeDistance a b y ^ N

structure NavierStokes.ActiveAnnulusWeight.EdgeFactor {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (K : Set E) (c : ℝ) (T : E × ℝ → V) : Type (max u_1 u_2)

An actual local edge identity and a smooth coefficient. No weighted derivative bound is included in these data.

• coefficient : E × ℝ → V

  Coefficient of EdgeFactor, of type E × ℝ → V.

• order : ℕ

  Order of EdgeFactor, of type ℕ.

• width : ℝ

  Width of EdgeFactor, of type ℝ.

• width_pos : 0 < self.width
• domain : Set (E × ℝ)

  Domain of EdgeFactor, of type Set (E × ℝ).

• domain_open : IsOpen self.domain
• boundary_mem : K ×ˢ {0} ⊆ self.domain
• smooth : ContDiffOn ℝ (↑⊤) self.coefficient self.domain
• boundary_ne_zero (p : E) : p ∈ K → self.coefficient (p, 0) ≠ 0
• identity (p : E) : p ∈ K → ∀ (x : ℝ), 0 < x → x < self.width → T (p, x) = (FlatCutoff.edge c x / x ^ self.order) • self.coefficient (p, x)

noncomputable def NavierStokes.ActiveAnnulusWeight.EdgeFactor.transfer {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Set E} {c : ℝ} {T S : E × ℝ → V} (F : EdgeFactor K c T) {w : ℝ} (hw : 0 < w) (hww : w ≤ F.width) (he : ∀ p ∈ K, ∀ (x : ℝ), 0 < x → x < w → S (p, x) = T (p, x)) : EdgeFactor K c S

Exact local equality transports an edge model to a joined stress.

Equations

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

theorem NavierStokes.ActiveAnnulusWeight.compact_nonzero_collar {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] {K : Set E} (hK : IsCompact K) {B : E × ℝ → V} {O : Set (E × ℝ)} (hO : IsOpen O) (hB : ContinuousOn B O) (hK0 : K ×ˢ {0} ⊆ O) (hne : ∀ p ∈ K, B (p, 0) ≠ 0) : ∃ (d : ℝ) (c : ℝ), 0 < d ∧ 0 < c ∧ K ×ˢ Set.Icc 0 d ⊆ O ∧ ∀ p ∈ K, ∀ x ∈ Set.Icc 0 d, c ≤ ‖B (p, x)‖

theorem NavierStokes.ActiveAnnulusWeight.EdgeFactor.collar {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Set E} (hK : IsCompact K) {c : ℝ} {T : E × ℝ → V} (F : EdgeFactor K c T) : ∃ (d : ℝ) (m : ℝ), 0 < d ∧ d < F.width ∧ d ≤ 1 ∧ 0 < m ∧ K ×ˢ Set.Icc 0 d ⊆ F.domain ∧ ∀ p ∈ K, ∀ (x : ℝ), 0 < x → x ≤ d → m * FlatCutoff.edge c x ≤ ‖T (p, x)‖

noncomputable def NavierStokes.ActiveAnnulusWeight.leftChart {E : Type u_1} {V : Type u_2} (a : ℝ) (T : E × ℝ → V) (q : E × ℝ) : V

Left chart, given by T (q.1,a+q.2).

Equations

• NavierStokes.ActiveAnnulusWeight.leftChart a T q = T (q.1, a + q.2)

noncomputable def NavierStokes.ActiveAnnulusWeight.rightChart {E : Type u_1} {V : Type u_2} (b : ℝ) (T : E × ℝ → V) (q : E × ℝ) : V

Right chart, given by T (q.1,b-q.2).

Equations

• NavierStokes.ActiveAnnulusWeight.rightChart b T q = T (q.1, b - q.2)

noncomputable def NavierStokes.ActiveAnnulusWeight.radialReflection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : E × ℝ ≃ₗᵢ[ℝ] E × ℝ

Radial reflection, given by { (LinearEquiv.refl ℝ E).prodCongr (LinearEquiv.neg ℝ) with norm_map' := by intro q; simp [Prod.norm_def] }.

Equations

• NavierStokes.ActiveAnnulusWeight.radialReflection = { toLinearEquiv := (LinearEquiv.refl ℝ E).prodCongr (LinearEquiv.neg ℝ), norm_map' := ⋯ }

theorem NavierStokes.ActiveAnnulusWeight.iteratedFDeriv_leftChart {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℝ) (T : E × ℝ → V) (n : ℕ) (q : E × ℝ) : iteratedFDeriv ℝ n (leftChart a T) q = iteratedFDeriv ℝ n T (q.1, a + q.2)

theorem NavierStokes.ActiveAnnulusWeight.norm_iteratedFDeriv_rightChart {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (b : ℝ) (T : E × ℝ → V) (n : ℕ) (q : E × ℝ) : ‖iteratedFDeriv ℝ n (rightChart b T) q‖ = ‖iteratedFDeriv ℝ n T (q.1, b - q.2)‖

theorem NavierStokes.ActiveAnnulusWeight.iteratedFDeriv_eq_of_eqOn {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {S : Set (E × ℝ)} (hS : UniqueDiffOn ℝ S) {f g : E × ℝ → V} (he : Set.EqOn f g S) {q : E × ℝ} (hq : q ∈ S) (hf : ContDiffAt ℝ (↑⊤) f q) (hg : ContDiffAt ℝ (↑⊤) g q) (n : ℕ) : iteratedFDeriv ℝ n f q = iteratedFDeriv ℝ n g q

theorem NavierStokes.ActiveAnnulusWeight.EdgeFactor.derivative_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Set E} (hK : IsCompact K) (hKd : UniqueDiffOn ℝ K) {c : ℝ} (hc : 0 < c) {T : E × ℝ → V} (F : EdgeFactor K c T) (n : ℕ) {d : ℝ} (hd : 0 < d) (hdw : d < F.width) (hdom : K ×ˢ Set.Icc 0 d ⊆ F.domain) (hT : ∀ p ∈ K, ∀ (x : ℝ), 0 < x → x ≤ d → ContDiffAt ℝ (↑⊤) T (p, x)) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ K, ∀ (x : ℝ), 0 < x → x ≤ d → ‖iteratedFDeriv ℝ i T (p, x)‖ ≤ C * FlatCutoff.edge c x / x ^ N

The local derivative estimates are consequences of the actual factor identity. Unique differentiability of the compact parameter set also covers its endpoints.

theorem NavierStokes.ActiveAnnulusWeight.compact_jets_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {O S : Set (E × ℝ)} (hO : IsOpen O) {T : E × ℝ → V} (hT : ContDiffOn ℝ (↑⊤) T O) (hS : IsCompact S) (hSO : S ⊆ O) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ i ≤ n, ∀ q ∈ S, ‖iteratedFDeriv ℝ i T q‖ ≤ C

theorem NavierStokes.ActiveAnnulusWeight.exists_global_lower_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Set E} (hK : IsCompact K) {a b c : ℝ} (hab : a < b) (hc : 0 < c) {T : E × ℝ → V} (hT : ContinuousOn T (K ×ˢ Set.Icc a b)) (hinterior : ∀ p ∈ K, ∀ y ∈ Set.Ioo a b, T (p, y) ≠ 0) (FL : EdgeFactor K c (leftChart a T)) (FR : EdgeFactor K 4 (rightChart b T)) : ∃ (m : ℝ), 0 < m ∧ ∀ p ∈ K, ∀ y ∈ Set.Ioo a b, m * weight c a b y ≤ ‖T (p, y)‖

Positivity inside and genuine nonzero edge factors give one global positive lower constant for the explicit product weight.

theorem NavierStokes.ActiveAnnulusWeight.exists_global_derivative_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Set E} (hK : IsCompact K) (hKd : UniqueDiffOn ℝ K) {a b c : ℝ} (hab : a < b) (hc : 0 < c) {T : E × ℝ → V} {O : Set (E × ℝ)} (hO : IsOpen O) (hT : ContDiffOn ℝ (↑⊤) T O) (hKO : K ×ˢ Set.Icc a b ⊆ O) (FL : EdgeFactor K c (leftChart a T)) (FR : EdgeFactor K 4 (rightChart b T)) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ K, ∀ y ∈ Set.Ioo a b, ‖iteratedFDeriv ℝ i T (p, y)‖ ≤ C * weight c a b y / edgeDistance a b y ^ N

All fixed full derivative tensors share the same explicit flat weight. The constants come from actual smooth coefficient jets and compactness.

theorem NavierStokes.ActiveAnnulusWeight.global_weighted_bounds {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Set E} (hK : IsCompact K) (hKd : UniqueDiffOn ℝ K) {a b c : ℝ} (hab : a < b) (hc : 0 < c) {T : E × ℝ → V} {O : Set (E × ℝ)} (hO : IsOpen O) (hT : ContDiffOn ℝ (↑⊤) T O) (hKO : K ×ˢ Set.Icc a b ⊆ O) (hinterior : ∀ p ∈ K, ∀ y ∈ Set.Ioo a b, T (p, y) ≠ 0) (FL : EdgeFactor K c (leftChart a T)) (FR : EdgeFactor K 4 (rightChart b T)) : (∃ (m : ℝ), 0 < m ∧ ∀ p ∈ K, ∀ y ∈ Set.Ioo a b, m * weight c a b y ≤ ‖T (p, y)‖) ∧ ∀ (n : ℕ), ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ K, ∀ y ∈ Set.Ioo a b, ‖iteratedFDeriv ℝ i T (p, y)‖ ≤ C * weight c a b y / edgeDistance a b y ^ N

Equation (20), for actual derivative tensors in the fixed logarithmic profile chart. The lower constant and the weight are independent of order.

noncomputable def NavierStokes.ActiveAnnulusWeight.logChart {E : Type u_1} (q : E × ℝ) : E × ℝ

Log chart, given by (q.1,Real.log q.2).

Equations

• NavierStokes.ActiveAnnulusWeight.logChart q = (q.1, Real.log q.2)

noncomputable def NavierStokes.ActiveAnnulusWeight.radialPullback {E : Type u_1} {V : Type u_2} (T : E × ℝ → V) (q : E × ℝ) : V

Radial pullback, given by T (logChart q).

Equations

• NavierStokes.ActiveAnnulusWeight.radialPullback T q = T (NavierStokes.ActiveAnnulusWeight.logChart q)

theorem NavierStokes.ActiveAnnulusWeight.logChart_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : ContDiffOn ℝ (↑⊤) logChart (Set.univ ×ˢ Set.Ioi 0)

theorem NavierStokes.ActiveAnnulusWeight.exists_radial_derivative_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Set E} (hK : IsCompact K) (hKd : UniqueDiffOn ℝ K) {a b c : ℝ} (hab : a < b) (hc : 0 < c) {T : E × ℝ → V} {O : Set (E × ℝ)} (hO : IsOpen O) (hT : ContDiffOn ℝ (↑⊤) T O) (hKO : K ×ˢ Set.Icc a b ⊆ O) (FL : EdgeFactor K c (leftChart a T)) (FR : EdgeFactor K 4 (rightChart b T)) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ p ∈ K, ∀ X ∈ Set.Ioo (Real.exp a) (Real.exp b), ‖iteratedFDeriv ℝ n (radialPullback T) (p, X)‖ ≤ C * radialWeight c a b X / edgeDistance a b (Real.log X) ^ N

The same weight controls genuine derivatives in X, not just in log X. The change-of-variable constants are bounded on the fixed positive annulus.

theorem NavierStokes.ActiveAnnulusWeight.radial_lower_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup V] {K : Set E} {a b c m : ℝ} {T : E × ℝ → V} (hlower : ∀ p ∈ K, ∀ y ∈ Set.Ioo a b, m * weight c a b y ≤ ‖T (p, y)‖) {p : E} (hp : p ∈ K) {X : ℝ} (hX : X ∈ Set.Ioo (Real.exp a) (Real.exp b)) : m * radialWeight c a b X ≤ ‖radialPullback T (p, X)‖

noncomputable def NavierStokes.ActiveAnnulusWeight.WeightedBounds {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (K : Set E) (c a b : ℝ) (T : E × ℝ → V) : Prop

The complete estimates in both fixed profile charts.

Equations

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

theorem NavierStokes.ActiveAnnulusWeight.weightedBounds_of_edge_factors {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Set E} (hK : IsCompact K) (hKd : UniqueDiffOn ℝ K) {a b c : ℝ} (hab : a < b) (hc : 0 < c) {T : E × ℝ → V} {O : Set (E × ℝ)} (hO : IsOpen O) (hT : ContDiffOn ℝ (↑⊤) T O) (hKO : K ×ˢ Set.Icc a b ⊆ O) (hinterior : ∀ p ∈ K, ∀ y ∈ Set.Ioo a b, T (p, y) ≠ 0) (FL : EdgeFactor K c (leftChart a T)) (FR : EdgeFactor K 4 (rightChart b T)) : WeightedBounds K c a b T

noncomputable def NavierStokes.ActiveAnnulusWeight.tilt (v : ℝ × ℝ) : ℝ

Tilt, given by v.2 / v.1.

Equations

• NavierStokes.ActiveAnnulusWeight.tilt v = v.2 / v.1

noncomputable def NavierStokes.ActiveAnnulusWeight.unitOfTilt (t : ℝ) : ℝ × ℝ

Unit of tilt, given by ((Real.sqrt (1+t^2))⁻¹,t / Real.sqrt (1+t^2)).

Equations

• NavierStokes.ActiveAnnulusWeight.unitOfTilt t = ((√(1 + t ^ 2))⁻¹, t / √(1 + t ^ 2))

noncomputable def NavierStokes.ActiveAnnulusWeight.direction (v : ℝ × ℝ) : ℝ × ℝ

Euclidean unit direction with positive angular component.

Equations

• NavierStokes.ActiveAnnulusWeight.direction v = NavierStokes.ActiveAnnulusWeight.unitOfTilt (NavierStokes.ActiveAnnulusWeight.tilt v)

theorem NavierStokes.ActiveAnnulusWeight.unitOfTilt_smooth : ContDiff ℝ (↑⊤) unitOfTilt

theorem NavierStokes.ActiveAnnulusWeight.unitOfTilt_normSq (t : ℝ) : (unitOfTilt t).1 ^ 2 + (unitOfTilt t).2 ^ 2 = 1

theorem NavierStokes.ActiveAnnulusWeight.tilt_smul {r : ℝ} (hr : r ≠ 0) (v : ℝ × ℝ) : tilt (r • v) = tilt v

theorem NavierStokes.ActiveAnnulusWeight.direction_smul {r : ℝ} (hr : r ≠ 0) (v : ℝ × ℝ) : direction (r • v) = direction v

theorem NavierStokes.ActiveAnnulusWeight.direction_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {O : Set (E × ℝ)} {B : E × ℝ → ℝ × ℝ} (hB : ContDiffOn ℝ (↑⊤) B O) (hne : ∀ q ∈ O, (B q).1 ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (q : E × ℝ) => direction (B q)) O

theorem NavierStokes.ActiveAnnulusWeight.positive_domain_open {E : Type u_1} [NormedAddCommGroup E] {O : Set (E × ℝ)} (hO : IsOpen O) {g : E × ℝ → ℝ} (hg : ContinuousOn g O) : IsOpen {q : E × ℝ | q ∈ O ∧ 0 < g q}

theorem NavierStokes.ActiveAnnulusWeight.compact_positive_collar {E : Type u_1} [NormedAddCommGroup E] {K : Set E} (hK : IsCompact K) {O : Set (E × ℝ)} (hO : IsOpen O) {g : E × ℝ → ℝ} (hg : ContinuousOn g O) (hK0 : K ×ˢ {0} ⊆ O) (hpos : ∀ p ∈ K, 0 < g (p, 0)) : ∃ (d : ℝ) (ε : ℝ), 0 < d ∧ 0 < ε ∧ K ×ˢ Set.Icc 0 d ⊆ O ∧ ∀ p ∈ K, ∀ x ∈ Set.Icc 0 d, ε ≤ g (p, x)

theorem NavierStokes.ActiveAnnulusWeight.EdgeFactor.direction_collar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsCompact K) {c : ℝ} {T : E × ℝ → ℝ × ℝ} (F : EdgeFactor K c T) (hfirst : ∀ p ∈ K, 0 < (F.coefficient (p, 0)).1) : ∃ (d : ℝ) (W : Set (E × ℝ)), 0 < d ∧ d < F.width ∧ IsOpen W ∧ K ×ˢ Set.Icc 0 d ⊆ W ∧ ContDiffOn ℝ (↑⊤) (fun (q : E × ℝ) => direction (F.coefficient q)) W ∧ (∀ p ∈ K, ∀ (x : ℝ), 0 < x → x ≤ d → direction (T (p, x)) = direction (F.coefficient (p, x))) ∧ ∀ p ∈ K, ∀ (x : ℝ), 0 < x → x ≤ d → 0 < (T (p, x)).1

A positive angular edge factor yields a genuine smooth unit direction for the stress, even where the stress itself vanishes at the edge.

noncomputable def NavierStokes.ActiveAnnulusWeight.directionProjection (s t : ℝ) : ℝ

Direction projection, given by 1+s*t.

Equations

• NavierStokes.ActiveAnnulusWeight.directionProjection s t = 1 + s * t

noncomputable def NavierStokes.ActiveAnnulusWeight.directionGap (v s t : ℝ) : ℝ

Direction gap, given by 2*(directionProjection s t)^2 - (v-2)*(t-s)^2.

Equations

• NavierStokes.ActiveAnnulusWeight.directionGap v s t = 2 * NavierStokes.ActiveAnnulusWeight.directionProjection s t ^ 2 - (v - 2) * (t - s) ^ 2

theorem NavierStokes.ActiveAnnulusWeight.aligned_direction_margin (v s : ℝ) : 0 < directionProjection s s ∧ 0 < directionGap v s s

theorem NavierStokes.ActiveAnnulusWeight.aligned_direction_collar {E : Type u_1} [NormedAddCommGroup E] {K : Set E} (hK : IsCompact K) {O : Set (E × ℝ)} (hO : IsOpen O) (hK0 : K ×ˢ {0} ⊆ O) {v s t : E × ℝ → ℝ} (hv : ContinuousOn v O) (hs : ContinuousOn s O) (ht : ContinuousOn t O) (halign : ∀ p ∈ K, t (p, 0) = s (p, 0)) : ∃ (d : ℝ) (ε : ℝ), 0 < d ∧ 0 < ε ∧ K ×ˢ Set.Icc 0 d ⊆ O ∧ ∀ p ∈ K, ∀ x ∈ Set.Icc 0 d, ε ≤ directionProjection (s (p, x)) (t (p, x)) ∧ ε ≤ directionGap (v (p, x)) (s (p, x)) (t (p, x))

Equality of the boundary direction with the shear direction gives a strict cone margin on one uniform collar by continuity and compactness.

theorem NavierStokes.ActiveAnnulusWeight.EdgeFactor.aligned_collar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsCompact K) {c : ℝ} {T : E × ℝ → ℝ × ℝ} (F : EdgeFactor K c T) (hfirst : ∀ p ∈ K, 0 < (F.coefficient (p, 0)).1) {O : Set (E × ℝ)} (hO : IsOpen O) (hK0 : K ×ˢ {0} ⊆ O) {v s : E × ℝ → ℝ} (hv : ContinuousOn v O) (hs : ContinuousOn s O) (halign : ∀ p ∈ K, tilt (F.coefficient (p, 0)) = s (p, 0)) : ∃ (d : ℝ) (ε : ℝ) (W : Set (E × ℝ)), 0 < d ∧ d < F.width ∧ 0 < ε ∧ IsOpen W ∧ K ×ˢ Set.Icc 0 d ⊆ W ∧ ContDiffOn ℝ (↑⊤) (fun (q : E × ℝ) => direction (F.coefficient q)) W ∧ (∀ p ∈ K, ∀ x ∈ Set.Icc 0 d, ε ≤ directionProjection (s (p, x)) (tilt (F.coefficient (p, x))) ∧ ε ≤ directionGap (v (p, x)) (s (p, x)) (tilt (F.coefficient (p, x)))) ∧ ∀ p ∈ K, ∀ (x : ℝ), 0 < x → x ≤ d → direction (T (p, x)) = direction (F.coefficient (p, x)) ∧ ε ≤ directionProjection (s (p, x)) (tilt (T (p, x))) ∧ ε ≤ directionGap (v (p, x)) (s (p, x)) (tilt (T (p, x)))

The actual stress direction has a smooth extension and a uniform strict cone margin when the genuine edge factor is aligned with the limiting shear.

noncomputable def NavierStokes.ActiveAnnulusWeight.HasStrictDirectionCollar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set E) (T B : E × ℝ → ℝ × ℝ) (v s : E × ℝ → ℝ) (width : ℝ) : Prop

A smooth extension of the actual unit direction, with strict margins for the true homogeneous cone inequalities on a full closed edge collar.

Equations

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

noncomputable def NavierStokes.ActiveAnnulusWeight.HasTrueDirectionCollar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set E) (T B : E × ℝ → ℝ × ℝ) (v s : E × ℝ → ℝ) (width : ℝ) : Prop

The directional certificate together with the speed condition v_s > 2 on one common positive-width collar.

Equations

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

theorem NavierStokes.ActiveAnnulusWeight.HasStrictDirectionCollar.true_of_speed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsCompact K) {T B : E × ℝ → ℝ × ℝ} {v s : E × ℝ → ℝ} {width : ℝ} (hdir : HasStrictDirectionCollar K T B v s width) {O : Set (E × ℝ)} (hO : IsOpen O) (hK0 : K ×ˢ {0} ⊆ O) (hv : ContinuousOn v O) (hvs : ∀ p ∈ K, 2 < v (p, 0)) : HasTrueDirectionCollar K T B v s width

theorem NavierStokes.ActiveAnnulusWeight.actual_shear_coordinates_smooth (T κ : ℝ) {X0 : ℝ} (hX0 : 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) : ContDiffOn ℝ (↑⊤) (StressActivation.actualP1 T κ L) (StressActivation.logDomain J hJ).carrier ∧ ContDiffOn ℝ (↑⊤) (StressActivation.actualP2 T κ X0 L U) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.ActiveAnnulusWeight.actual_shear_coordinates_zero {T : ℝ} (hT : 0 < T) (κ : ℝ) {X0 : ℝ} (hX0 : 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) {η : ℝ} (hη : η ∈ J) : StressActivation.actualP1 T κ L (0, η) = StressActivation.referenceP1 L (0, η) ∧ StressActivation.actualP2 T κ X0 L U (0, η) = StressActivation.referenceP2 X0 L U (0, η)

theorem NavierStokes.ActiveAnnulusWeight.actual_shear_domain {T : ℝ} (hT : 0 < T) (κ : ℝ) {X0 : ℝ} (hX0 : 0 < X0) {J K : Set ℝ} (hJ : IsOpen J) (hKJ : K ⊆ J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hA0 : ∀ η ∈ K, 0 < StressActivation.referenceP1 L (0, η)) : ∃ (O : Set (ℝ × ℝ)), IsOpen O ∧ K ×ˢ {0} ⊆ O ∧ ContDiffOn ℝ (↑⊤) (fun (q : ℝ × ℝ) => StressActivation.shearSize T κ X0 L U (q.2, q.1)) O ∧ ContDiffOn ℝ (↑⊤) (fun (q : ℝ × ℝ) => StressActivation.shearSlope T κ X0 L U (q.2, q.1)) O

noncomputable def NavierStokes.ActiveAnnulusWeight.activationCoefficient (T κ : ℝ) (D : ActivationBounds.ScaledPoint → ℝ × ℝ) (q : ℝ × ℝ) : ℝ × ℝ

Fixed activation parameters expose the actual Gaussian coefficient T². The coefficient is smooth through the attachment.

Equations

• NavierStokes.ActiveAnnulusWeight.activationCoefficient T κ D q = ((1 - κ) / NavierStokes.StressActivation.stepDenominator T q.2) • D ((κ, T), q.2 / T, q.1)

theorem NavierStokes.ActiveAnnulusWeight.activationCoefficient_smooth {J : Set ℝ} (T κ : ℝ) {D : ActivationBounds.ScaledPoint → ℝ × ℝ} (hD : ContDiffOn ℝ (↑⊤) D (ActivationBounds.scaledDomain J)) : ContDiffOn ℝ (↑⊤) (activationCoefficient T κ D) (J ×ˢ Set.univ)

theorem NavierStokes.ActiveAnnulusWeight.activationCoefficient_edge {T κ : ℝ} {D : ActivationBounds.ScaledPoint → ℝ × ℝ} (η : ℝ) : activationCoefficient T κ D (η, 0) = ((1 - κ) / StressActivation.stepDenominator T 0) • D ((κ, T), 0, η)

noncomputable def NavierStokes.ActiveAnnulusWeight.activationEdgeFactor {J K : Set ℝ} (hJ : IsOpen J) (hKJ : K ⊆ J) {T κ d : ℝ} (hT : 0 < T) (hκ : κ < 1) (hd : 0 < d) {D : ActivationBounds.ScaledPoint → ℝ × ℝ} (hD : ContDiffOn ℝ (↑⊤) D (ActivationBounds.scaledDomain J)) (hD0 : ∀ η ∈ K, D ((κ, T), 0, η) ≠ 0) {S : ℝ × ℝ → ℝ × ℝ} (hfactor : ∀ (u η : ℝ), T * u ∈ Set.Icc 0 d → η ∈ K → S (T * u, η) = (StressActivation.activation 1 κ u * (D ((κ, T), u, η)).1, StressActivation.activation 1 κ u * (D ((κ, T), u, η)).2)) : EdgeFactor K (T ^ 2) fun (q : ℝ × ℝ) => S (q.2, q.1)

This is the factor in the actual activation stress identity, after its scaled coordinate is converted back to the logarithmic edge distance.

Equations

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

theorem NavierStokes.ActiveAnnulusWeight.exists_natural_activation_factor {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (F : NaturalEntrance.EntranceProfile d Λ C) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) {T κ : ℝ} (hT : 0 < T) (hκ : κ < 1) : have N := ReferencePath.Input.ofNatural hΛ F.profile.family; have L := StressActivation.FromReference.refLog N δ; have U := StressActivation.FromReference.refAxial N δ; have I := ActivationStocks.FromReference.initial N hδ hδlim P0 hP0; Nonempty (EdgeFactor (Set.Icc (-1) 1) (T ^ 2) fun (q : ℝ × ℝ) => ActivationCone.activatedStress h N.endpoint I L U T κ (q.2, q.1))

theorem NavierStokes.ActiveAnnulusWeight.exists_natural_activation_factor_aligned {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (F : NaturalEntrance.EntranceProfile d Λ C) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) {T κ : ℝ} (hT : 0 < T) (hκ : κ < 1) : have N := ReferencePath.Input.ofNatural hΛ F.profile.family; have L := StressActivation.FromReference.refLog N δ; have U := StressActivation.FromReference.refAxial N δ; have I := ActivationStocks.FromReference.initial N hδ hδlim P0 hP0; ∃ (G : EdgeFactor (Set.Icc (-1) 1) (T ^ 2) fun (q : ℝ × ℝ) => ActivationCone.activatedStress h N.endpoint I L U T κ (q.2, q.1)), (∀ η ∈ Set.Icc (-1) 1, 0 < (G.coefficient (η, 0)).1) ∧ ∀ η ∈ Set.Icc (-1) 1, tilt (G.coefficient (η, 0)) = StressActivation.referenceP2 N.endpoint L U (0, η) / StressActivation.referenceP1 L (0, η)

The coefficient is constructed from the actual reference histories. Its boundary tilt is exactly the reference shear tilt, rather than an assumed directional estimate.

theorem NavierStokes.ActiveAnnulusWeight.natural_activation_strict_direction {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (F : NaturalEntrance.EntranceProfile d Λ C) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) {T κ : ℝ} (hT : 0 < T) (hκ : κ < 1) : have N := ReferencePath.Input.ofNatural hΛ F.profile.family; have L := StressActivation.FromReference.refLog N δ; have U := StressActivation.FromReference.refAxial N δ; have I := ActivationStocks.FromReference.initial N hδ hδlim P0 hP0; have S := fun (q : ℝ × ℝ) => ActivationCone.activatedStress h N.endpoint I L U T κ (q.2, q.1); ∃ (G : EdgeFactor (Set.Icc (-1) 1) (T ^ 2) S), HasStrictDirectionCollar (Set.Icc (-1) 1) S G.coefficient (fun (q : ℝ × ℝ) => StressActivation.shearSize T κ N.endpoint L U (q.2, q.1)) (fun (q : ℝ × ℝ) => StressActivation.shearSlope T κ N.endpoint L U (q.2, q.1)) G.width

The initial ACT stress has a genuine smooth unit-direction extension and a strict cone margin relative to its actual shear.

theorem NavierStokes.ActiveAnnulusWeight.natural_activation_true_direction {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (F : NaturalEntrance.EntranceProfile d Λ C) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) {T κ : ℝ} (hT : 0 < T) (hκ : κ < 1) : have N := ReferencePath.Input.ofNatural hΛ F.profile.family; have L := StressActivation.FromReference.refLog N δ; have U := StressActivation.FromReference.refAxial N δ; have I := ActivationStocks.FromReference.initial N hδ hδlim P0 hP0; have S := fun (q : ℝ × ℝ) => ActivationCone.activatedStress h N.endpoint I L U T κ (q.2, q.1); ∃ (G : EdgeFactor (Set.Icc (-1) 1) (T ^ 2) S), HasTrueDirectionCollar (Set.Icc (-1) 1) S G.coefficient (fun (q : ℝ × ℝ) => StressActivation.shearSize T κ N.endpoint L U (q.2, q.1)) (fun (q : ℝ × ℝ) => StressActivation.shearSlope T κ N.endpoint L U (q.2, q.1)) G.width

noncomputable def NavierStokes.ActiveAnnulusWeight.terminalEdgeFactor {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 w : ℝ) (hw : 0 < w) : EdgeFactor (Set.Icc (-1) 1) 4 (TerminalEdgeFactor.profileStress C d y0)

The actual terminal stress uses coefficient 4 and inverse-cubic order. The smooth factor is defined through the closed parameter endpoints.

Equations

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

theorem NavierStokes.ActiveAnnulusWeight.terminal_strict_direction {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) : HasStrictDirectionCollar (Set.Icc (-1) 1) (TerminalEdgeFactor.profileStress C d y0) (TerminalEdgeFactor.profileStressFactor C d y0) (TerminalEdgeFactor.profileSpeed C d y0) (fun (x : ℝ × ℝ) => 0) 1

theorem NavierStokes.ActiveAnnulusWeight.terminal_true_direction {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) : HasTrueDirectionCollar (Set.Icc (-1) 1) (TerminalEdgeFactor.profileStress C d y0) (TerminalEdgeFactor.profileStressFactor C d y0) (TerminalEdgeFactor.profileSpeed C d y0) (fun (x : ℝ × ℝ) => 0) 1

theorem NavierStokes.ActiveAnnulusWeight.actual_edge_join {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (F : NaturalEntrance.EntranceProfile d Λ C) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) {T κ : ℝ} (hT : 0 < T) (hκ : κ < 1) {Ct : ℝ} (hCt : 0 < Ct) (dt : OutgoingTail.TailData) (y0 : ℝ) {a b : ℝ} (hab : a < b) {S : ℝ × ℝ → ℝ × ℝ} {O : Set (ℝ × ℝ)} (hO : IsOpen O) (hS : ContDiffOn ℝ (↑⊤) S O) (hSO : Set.Icc (-1) 1 ×ˢ Set.Icc a b ⊆ O) (hinterior : ∀ η ∈ Set.Icc (-1) 1, ∀ y ∈ Set.Ioo a b, S (η, y) ≠ 0) {wL wR : ℝ} (hwL : 0 < wL) (hwR : 0 < wR) : have N := ReferencePath.Input.ofNatural hΛ F.profile.family; have L := StressActivation.FromReference.refLog N δ; have U := StressActivation.FromReference.refAxial N δ; have I := ActivationStocks.FromReference.initial N hδ hδlim P0 hP0; (∀ η ∈ Set.Icc (-1) 1, ∀ (x : ℝ), 0 < x → x < wL → leftChart a S (η, x) = ActivationCone.activatedStress h N.endpoint I L U T κ (x, η)) → (∀ η ∈ Set.Icc (-1) 1, ∀ (x : ℝ), 0 < x → x < wR → rightChart b S (η, x) = TerminalEdgeFactor.profileStress Ct dt y0 (η, x)) → WeightedBounds (Set.Icc (-1) 1) (T ^ 2) a b S

Equation (20) for a joined nominal stress with exact ACT and terminal edge identities. The only remaining global inputs are genuine smoothness and interior nonvanishing of that joined stress.