Compact-family uniformity and stability of the stress cone

The input functions are actual continuous functions on a compact parameter set. Uniform margins, a single amplitude threshold, and a common perturbation radius are conclusions of the theorems, not assumptions.

theorem NavierStokes.UniformCone.positive_uniform_margin {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {g : X → ℝ} (hg : ContinuousOn g K) (hpos : ∀ x ∈ K, 0 < g x) : ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ K, ε ≤ g x

The positive minimum of a continuous positive function on a compact set. This also covers the empty parameter set.

theorem NavierStokes.UniformCone.compact_source_margins {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {a b w : X → ℝ} (ha : ContinuousOn a K) (hb : ContinuousOn b K) (hw : ContinuousOn w K) (hapos : ∀ x ∈ K, 0 < a x) (hfirst : ∀ x ∈ K, 0 < a x - b x * w x) (hsecond : ∀ x ∈ K, 2 * b x * w x + b x ^ 2 / a x + (a x - 2) * w x ^ 2 < 2) : ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ K, ε ≤ a x ∧ ε ≤ a x - b x * w x ∧ ε ≤ 2 - (2 * b x * w x + b x ^ 2 / a x + (a x - 2) * w x ^ 2)

All three strict source inequalities in (11) have a common positive margin on a continuous compact parameter family.

theorem NavierStokes.UniformCone.compact_normalized_cone {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {c j v : X → ℝ} (hc : ContinuousOn c K) (hj : ContinuousOn j K) (hv : ContinuousOn v K) (hcpos : ∀ x ∈ K, 0 < c x) (hmargin : ∀ x ∈ K, (v x - 2) * j x ^ 2 < 2 * c x ^ 2) : ∃ (ε : ℝ) (p₀ : ℝ), 0 < ε ∧ 0 ≤ p₀ ∧ (∀ x ∈ K, ε ≤ c x ∧ ε ≤ 2 * c x ^ 2 - (v x - 2) * j x ^ 2) ∧ ∀ (p : ℝ), p₀ < p → ∀ x ∈ K, 2 < p * c x ∧ v x < ConeAlgebra.coneBound (p * c x) (p * j x)

Compact normalized data give one amplitude threshold for the entire family.

theorem NavierStokes.UniformCone.compact_normalized_cone_gap {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {c j v : X → ℝ} (hc : ContinuousOn c K) (hj : ContinuousOn j K) (hv : ContinuousOn v K) (hcpos : ∀ x ∈ K, 0 < c x) (hmargin : ∀ x ∈ K, (v x - 2) * j x ^ 2 < 2 * c x ^ 2) : ∃ (η : ℝ) (p₀ : ℝ), 0 < η ∧ 0 ≤ p₀ ∧ ∀ (p : ℝ), p₀ < p → ∀ x ∈ K, 2 + η < p * c x ∧ v x + η < ConeAlgebra.coneBound (p * c x) (p * j x)

The eventual relaxed-cone inequalities have uniform positive additive gaps, independent both of the parameter and of the large amplitude.

theorem NavierStokes.UniformCone.compact_equation_eleven {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {a b w : X → ℝ} (ha : ContinuousOn a K) (hb : ContinuousOn b K) (hw : ContinuousOn w K) (hapos : ∀ x ∈ K, 0 < a x) (hfirst : ∀ x ∈ K, 0 < a x - b x * w x) (hsecond : ∀ x ∈ K, 2 * b x * w x + b x ^ 2 / a x + (a x - 2) * w x ^ 2 < 2) : ∃ (ε : ℝ) (p₀ : ℝ), 0 < ε ∧ 0 ≤ p₀ ∧ (∀ x ∈ K, ε ≤ 1 - b x * w x / a x ∧ ε ≤ 2 * (1 - b x * w x / a x) ^ 2 - (a x * (1 + (b x / a x) ^ 2) - 2) * (w x + b x / a x) ^ 2) ∧ ∀ (p : ℝ), p₀ < p → ∀ x ∈ K, 2 < p * (1 - b x * w x / a x) ∧ a x * (1 + (b x / a x) ^ 2) < ConeAlgebra.coneBound (p * (1 - b x * w x / a x)) (p * (w x + b x / a x))

The manuscript's strict source criterion (11), uniformly on any compact parameter family. The conclusion supplies uniform normalized margins and a single threshold for all stress amplitudes above it.

theorem NavierStokes.UniformCone.compact_equation_eleven_gap {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {a b w : X → ℝ} (ha : ContinuousOn a K) (hb : ContinuousOn b K) (hw : ContinuousOn w K) (hapos : ∀ x ∈ K, 0 < a x) (hfirst : ∀ x ∈ K, 0 < a x - b x * w x) (hsecond : ∀ x ∈ K, 2 * b x * w x + b x ^ 2 / a x + (a x - 2) * w x ^ 2 < 2) : ∃ (η : ℝ) (p₀ : ℝ), 0 < η ∧ 0 ≤ p₀ ∧ ∀ (p : ℝ), p₀ < p → ∀ x ∈ K, 2 + η < p * (1 - b x * w x / a x) ∧ a x * (1 + (b x / a x) ^ 2) + η < ConeAlgebra.coneBound (p * (1 - b x * w x / a x)) (p * (w x + b x / a x))

Equation (11), with a common positive additive gap in both relaxed-cone inequalities for every parameter and every sufficiently large amplitude.

@[reducible, inline]

abbrev NavierStokes.UniformCone.ConeDatum : Type

Coordinates (P,J,v) for a stress cone datum, with the product metric.

Equations

• NavierStokes.UniformCone.ConeDatum = (ℝ × ℝ × ℝ)

def NavierStokes.UniformCone.trueCone : Set ConeDatum

The exact open true cone, retaining the square-root inequality.

Equations

• NavierStokes.UniformCone.trueCone = {z : NavierStokes.UniformCone.ConeDatum | 2 < z.2.2 ∧ 2 < z.1 ∧ z.2.2 < NavierStokes.ConeAlgebra.coneBound z.1 z.2.1}

theorem NavierStokes.UniformCone.continuous_coneBound : Continuous fun (z : ConeDatum) => ConeAlgebra.coneBound z.1 z.2.1

theorem NavierStokes.UniformCone.isOpen_trueCone : IsOpen trueCone

theorem NavierStokes.UniformCone.compact_trueCone_margins {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {P J v : X → ℝ} (hP : ContinuousOn P K) (hJ : ContinuousOn J K) (hv : ContinuousOn v K) (hcone : ∀ x ∈ K, 2 < v x ∧ 2 < P x ∧ v x < ConeAlgebra.coneBound (P x) (J x)) : ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ K, ε ≤ v x - 2 ∧ ε ≤ P x - 2 ∧ ε ≤ ConeAlgebra.coneBound (P x) (J x) - v x

A continuous compact family inside the true cone stays a uniformly positive distance from each of its three defining scalar boundaries.

theorem NavierStokes.UniformCone.compact_trueCone_stable {S : Set ConeDatum} (hS : IsCompact S) (hcone : S ⊆ trueCone) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ z ∈ S, ∀ (z' : ConeDatum), dist z' z ≤ ρ → z' ∈ trueCone

Every compact subset of the true cone has one positive metric perturbation tolerance, including perturbations outside the original image.

theorem NavierStokes.UniformCone.compact_family_trueCone_stable {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {P J v : X → ℝ} (hP : ContinuousOn P K) (hJ : ContinuousOn J K) (hv : ContinuousOn v K) (hcone : ∀ x ∈ K, 2 < v x ∧ 2 < P x ∧ v x < ConeAlgebra.coneBound (P x) (J x)) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ x ∈ K, ∀ (P' J' v' : ℝ), dist (P', J', v') (P x, J x, v x) ≤ ρ → 2 < v' ∧ 2 < P' ∧ v' < ConeAlgebra.coneBound P' J'

A continuous compact family in the true cone has uniform perturbation tolerance. The competing datum need not depend continuously on the parameter.

theorem NavierStokes.UniformCone.compact_family_quadratic_stable {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {P J v : X → ℝ} (hP : ContinuousOn P K) (hJ : ContinuousOn J K) (hv : ContinuousOn v K) (hcone : ∀ x ∈ K, 2 < v x ∧ 2 < P x ∧ v x < ConeAlgebra.coneBound (P x) (J x)) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ x ∈ K, ∀ (P' J' v' : ℝ), |P' - P x| ≤ ρ → |J' - J x| ≤ ρ → |v' - v x| ≤ ρ → 2 < v' ∧ v' < P' ∧ (v' - 2) * J' ^ 2 < 2 * (P' - v') ^ 2

Coordinatewise perturbations of a compact true-cone family preserve the exact quadratic criterion as well as the lower bound v > 2.