The actual similarity scale at the singular point

The coordinate solves q - z^2 q^a = tau. Its positive branch tends to zero when tau and z tend to zero together. The value assigned outside the positive-time domain is never used in this assertion.

noncomputable def NavierStokes.SimilarityApproach.upperScale (a : ℝ) (p : ℝ × ℝ) : ℝ

Upper scale, given by 2 * p.1 + (2 * p.2 ^ 2) ^ (1 - a)⁻¹.

Equations

• NavierStokes.SimilarityApproach.upperScale a p = 2 * p.1 + (2 * p.2 ^ 2) ^ (1 - a)⁻¹

theorem NavierStokes.SimilarityApproach.coordinateQ_le_upperScale {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : SimilarityCoordinates.coordinateQ a p ≤ upperScale a p

theorem NavierStokes.SimilarityApproach.upperScale_continuous {a : ℝ} (ha1 : a < 1) : Continuous (upperScale a)

@[simp]

theorem NavierStokes.SimilarityApproach.upperScale_origin {a : ℝ} (ha1 : a < 1) : upperScale a (0, 0) = 0

theorem NavierStokes.SimilarityApproach.coordinateQ_tendsto_zero {α : Type u_1} {l : Filter α} {tau z : α → ℝ} {a : ℝ} (ha : 0 < a) (ha1 : a < 1) (htau : Filter.Tendsto tau l (nhds 0)) (hz : Filter.Tendsto z l (nhds 0)) (hpos : ∀ᶠ (i : α) in l, 0 < tau i) : Filter.Tendsto (fun (i : α) => SimilarityCoordinates.coordinateQ a (tau i, z i)) l (nhds 0)

Joint approach; neither a fixed axial coordinate nor a prescribed path is required. Positive time is required eventually.

theorem NavierStokes.SimilarityApproach.physical_q_bound {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) : SimilarityProfile.q h p ≤ 2 * (1 - p.1) + (2 * p.2.2 ^ 2) ^ (1 - 2 * h)⁻¹

theorem NavierStokes.SimilarityApproach.physical_q_tendsto_zero {α : Type u_1} {l : Filter α} {p : α → SimilarityProfile.PhysicalPoint} {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ht : Filter.Tendsto (fun (i : α) => (p i).1) l (nhds 1)) (hz : Filter.Tendsto (fun (i : α) => (p i).2.2) l (nhds 0)) (hbefore : ∀ᶠ (i : α) in l, (p i).1 < 1) : Filter.Tendsto (fun (i : α) => SimilarityProfile.q h (p i)) l (nhds 0)

theorem NavierStokes.SimilarityApproach.jet_tendsto_zero {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter D} {q : D → ℝ} {f : D → V} {m : ℕ} (hjet : DiagonalResidual.JetRate l q f m 1) (hq : Filter.Tendsto q l (nhds 0)) : Filter.Tendsto (iteratedFDeriv ℝ m f) l (nhds 0)

A proved positive-order estimate of an actual derivative gives its zero limit once the actual scale has the joint limit above.