Square roots and signed quotients from weighted derivative bounds

The estimates use genuine Fréchet derivatives. A normalization used in a pointwise estimate is constant in the differentiation variable: no regularity of the quotient by a variable flat weight is assumed.

Jointly smooth zero extension from locally uniform Gaussian bounds

The bounds concern the actual full Fréchet derivative tensors of a function on U × (0,∞). They are uniform in a neighborhood of each parameter point. Every tensor is extended by zero. One extra inverse power in the Gaussian bound proves that its derivative at the edge is zero, using δ ≤ ‖(p,δ) - (p₀,0)‖. No pointwise-to-joint limit inference is used.

noncomputable def NavierStokes.FlatZeroExtension.zeroExtension {E : Type u_1} {F : Type u_2} [Zero F] (f : E × ℝ → F) (p : E × ℝ) : F

Preserve positive edge distance and use zero on the other side.

Equations

• NavierStokes.FlatZeroExtension.zeroExtension f p = if 0 < p.2 then f p else 0

theorem NavierStokes.FlatZeroExtension.zeroExtension_of_pos {E : Type u_1} {F : Type u_2} [Zero F] (f : E × ℝ → F) {p : E × ℝ} (hp : 0 < p.2) : zeroExtension f p = f p

theorem NavierStokes.FlatZeroExtension.zeroExtension_of_nonpos {E : Type u_1} {F : Type u_2} [Zero F] (f : E × ℝ → F) {p : E × ℝ} (hp : p.2 ≤ 0) : zeroExtension f p = 0

@[simp]

theorem NavierStokes.FlatZeroExtension.zeroExtension_edge {E : Type u_1} {F : Type u_2} [Zero F] (f : E × ℝ → F) (x : E) : zeroExtension f (x, 0) = 0

theorem NavierStokes.FlatZeroExtension.zeroExtension_germ_pos {E : Type u_1} {F : Type u_2} [Zero F] [TopologicalSpace E] (f : E × ℝ → F) {p : E × ℝ} (hp : 0 < p.2) : zeroExtension f =ᶠ[nhds p] f

theorem NavierStokes.FlatZeroExtension.zeroExtension_germ_neg {E : Type u_1} {F : Type u_2} [Zero F] [TopologicalSpace E] (f : E × ℝ → F) {p : E × ℝ} (hp : p.2 < 0) : zeroExtension f =ᶠ[nhds p] fun (x : E × ℝ) => 0

def NavierStokes.FlatZeroExtension.LocalGaussianBound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] (c : ℝ) (U : Set E) (g : E × ℝ → F) : Prop

A locally uniform bound. The constant, inverse-power loss, and parameter neighborhood may depend on the parameter point. The interval (0,1) is only used near the edge.

Equations

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

def NavierStokes.FlatZeroExtension.LocalGaussianJets {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (U : Set E) (f : E × ℝ → F) : Prop

Every actual tensor is bounded, with constants and losses allowed to depend on its derivative order as well as the parameter point.

Equations

• NavierStokes.FlatZeroExtension.LocalGaussianJets c U f = ∀ (n : ℕ), NavierStokes.FlatZeroExtension.LocalGaussianBound c U (iteratedFDeriv ℝ n f)

theorem NavierStokes.FlatZeroExtension.LocalGaussianBound.of_uniform {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {c C : ℝ} {N : ℕ} {U : Set E} {g : E × ℝ → F} (hC : 0 ≤ C) (hbound : ∀ y ∈ U, ∀ δ ∈ Set.Ioo 0 1, ‖g (y, δ)‖ ≤ C * FlatCutoff.edge c δ / δ ^ N) : LocalGaussianBound c U g

theorem NavierStokes.FlatZeroExtension.LocalGaussianBound.of_exp_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {c : ℝ} {U : Set E} {g : E × ℝ → F} (hbound : ∀ x ∈ U, ∃ V ∈ nhds x, ∃ (C : ℝ), 0 ≤ C ∧ ∃ (N : ℕ), ∀ y ∈ V ∩ U, ∀ δ ∈ Set.Ioo 0 1, ‖g (y, δ)‖ ≤ C * Real.exp (-c / δ ^ 2) / δ ^ N) : LocalGaussianBound c U g

Adapter from the unextended exponential written in analytic estimates.

theorem NavierStokes.FlatZeroExtension.edge_div_pow_tendsto_zero {c : ℝ} (hc : 0 < c) (N : ℕ) : Filter.Tendsto (fun (δ : ℝ) => FlatCutoff.edge c δ / δ ^ N) (nhds 0) (nhds 0)

theorem NavierStokes.FlatZeroExtension.hasFDerivAt_zeroExtension_edge {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) {U : Set E} (hU : IsOpen U) {g : E × ℝ → F} (hB : LocalGaussianBound c U g) {x : E} (hx : x ∈ U) : HasFDerivAt (zeroExtension g) 0 (x, 0)

A bound on values alone, uniform in the parameter, proves a zero full derivative at the edge. This applies later to every actual tensor.

noncomputable def NavierStokes.FlatZeroExtension.extendedJets {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E × ℝ → F) (p : E × ℝ) : FormalMultilinearSeries ℝ (E × ℝ) F

Zero extension of each actual derivative tensor.

Equations

• NavierStokes.FlatZeroExtension.extendedJets f p n = NavierStokes.FlatZeroExtension.zeroExtension (iteratedFDeriv ℝ n f) p

theorem NavierStokes.FlatZeroExtension.iteratedFDeriv_hasFDerivAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E × ℝ → F} {p : E × ℝ} (hf : ContDiffAt ℝ (↑⊤) f p) (n : ℕ) : HasFDerivAt (iteratedFDeriv ℝ n f) (iteratedFDeriv ℝ (n + 1) f p).curryLeft p

theorem NavierStokes.FlatZeroExtension.extendedJets_hasFDerivAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) {U : Set E} (hU : IsOpen U) {f : E × ℝ → F} (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.Ioi 0)) (hB : LocalGaussianJets c U f) (n : ℕ) {p : E × ℝ} (hp : p ∈ U ×ˢ Set.univ) : HasFDerivAt (fun (q : E × ℝ) => extendedJets f q n) (extendedJets f p (n + 1)).curryLeft p

The derivative recurrence holds for the extended tensors on both sides and at the edge. The edge case comes from the proved small-o bound.

theorem NavierStokes.FlatZeroExtension.hasFTaylorSeriesUpToOn_zeroExtension {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) {U : Set E} (hU : IsOpen U) {f : E × ℝ → F} (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.Ioi 0)) (hB : LocalGaussianJets c U f) : HasFTaylorSeriesUpToOn (↑⊤) (zeroExtension f) (extendedJets f) (U ×ˢ Set.univ)

The proved extended tensors form the actual Taylor family of the zero extension on the open set U × ℝ.

theorem NavierStokes.FlatZeroExtension.contDiffOn_zeroExtension {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) {U : Set E} (hU : IsOpen U) {f : E × ℝ → F} (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.Ioi 0)) (hB : LocalGaussianJets c U f) : ContDiffOn ℝ (↑⊤) (zeroExtension f) (U ×ˢ Set.univ)

Main gluing theorem. Neither the parameter space nor the target needs a finite-dimensionality or completeness hypothesis.

theorem NavierStokes.FlatZeroExtension.iteratedFDeriv_zeroExtension {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) {U : Set E} (hU : IsOpen U) {f : E × ℝ → F} (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.Ioi 0)) (hB : LocalGaussianJets c U f) (n : ℕ) {p : E × ℝ} (hp : p ∈ U ×ˢ Set.univ) : iteratedFDeriv ℝ n (zeroExtension f) p = zeroExtension (iteratedFDeriv ℝ n f) p

The ordinary full tensors of the extension equal the zero extensions of the original ordinary full tensors.

theorem NavierStokes.FlatZeroExtension.iteratedFDeriv_zeroExtension_nonpos {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) {U : Set E} (hU : IsOpen U) {f : E × ℝ → F} (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.Ioi 0)) (hB : LocalGaussianJets c U f) (n : ℕ) {p : E × ℝ} (hp : p.1 ∈ U) (hδ : p.2 ≤ 0) : iteratedFDeriv ℝ n (zeroExtension f) p = 0

theorem NavierStokes.FlatZeroExtension.iteratedFDeriv_zeroExtension_edge {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) {U : Set E} (hU : IsOpen U) {f : E × ℝ → F} (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.Ioi 0)) (hB : LocalGaussianJets c U f) (n : ℕ) {x : E} (hx : x ∈ U) : iteratedFDeriv ℝ n (zeroExtension f) (x, 0) = 0

In particular every mixed derivative at the joining edge is zero.

theorem NavierStokes.FlatZeroExtension.contDiffOn_zeroExtension_of_exp_bounds {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) {U : Set E} (hU : IsOpen U) {f : E × ℝ → F} (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.Ioi 0)) (hbound : ∀ (n : ℕ), ∀ x ∈ U, ∃ V ∈ nhds x, ∃ (C : ℝ), 0 ≤ C ∧ ∃ (N : ℕ), ∀ y ∈ V ∩ U, ∀ δ ∈ Set.Ioo 0 1, ‖iteratedFDeriv ℝ n f (y, δ)‖ ≤ C * Real.exp (-c / δ ^ 2) / δ ^ N) : ContDiffOn ℝ (↑⊤) (zeroExtension f) (U ×ˢ Set.univ)

The main theorem stated directly with local exponential estimates of every actual tensor. The interval and neighborhood bounds remain explicit.

theorem NavierStokes.FlatZeroExtension.contDiff_zeroExtension {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) {f : E × ℝ → F} (hf : ContDiffOn ℝ (↑⊤) f (Set.univ ×ˢ Set.Ioi 0)) (hB : LocalGaussianJets c Set.univ f) : ContDiff ℝ (↑⊤) (zeroExtension f)

theorem NavierStokes.WeightedQuotients.nat_le_infty (n : ℕ) : ↑n ≤ ↑⊤

noncomputable def NavierStokes.WeightedQuotients.rpowCoeff (p : ℝ) : ℕ → ℝ

Rpow coefficient as an element of ℕ → ℝ | 0 => 1 | n + 1 => rpowCoeff p n * (p - (n : ℝ)).

Equations

• NavierStokes.WeightedQuotients.rpowCoeff p 0 = 1
• NavierStokes.WeightedQuotients.rpowCoeff p n.succ = NavierStokes.WeightedQuotients.rpowCoeff p n * (p - ↑n)

theorem NavierStokes.WeightedQuotients.iteratedDeriv_rpow (p : ℝ) (n : ℕ) {t : ℝ} (ht : 0 < t) : iteratedDeriv n (fun (t : ℝ) => t ^ p) t = rpowCoeff p n * t ^ (p - ↑n)

Actual scalar derivatives of a real power on the positive half-line.

noncomputable def NavierStokes.WeightedQuotients.coeffBound (p : ℝ) (n : ℕ) : ℝ

Coeff bound, given by (∑ k ∈ Finset.range (n + 1), |rpowCoeff p k|) + 1.

Equations

• NavierStokes.WeightedQuotients.coeffBound p n = ∑ k ∈ Finset.range (n + 1), |NavierStokes.WeightedQuotients.rpowCoeff p k| + 1

theorem NavierStokes.WeightedQuotients.coeffBound_nonneg (p : ℝ) (n : ℕ) : 0 ≤ coeffBound p n

theorem NavierStokes.WeightedQuotients.abs_coeff_le (p : ℝ) {i n : ℕ} (hi : i ≤ n) : |rpowCoeff p i| ≤ coeffBound p n

theorem NavierStokes.WeightedQuotients.rpow_jet_bound (p : ℝ) {B t : ℝ} (hB : 1 ≤ B) (ht : 0 < t) (hp : t ^ p ≤ B) (hi : t⁻¹ ≤ B) {i n : ℕ} (hin : i ≤ n) : ‖iteratedFDeriv ℝ i (fun (t : ℝ) => t ^ p) t‖ ≤ coeffBound p n * B ^ (n + 1)

theorem NavierStokes.WeightedQuotients.sqrt_le_of_bounds {B t : ℝ} (hB : 1 ≤ B) (ht : 0 ≤ t) (hu : t ≤ B) : √t ≤ B

theorem NavierStokes.WeightedQuotients.half_power_bound {B t : ℝ} (hB : 1 ≤ B) (ht : 0 < t) (hu : t ≤ B) : t ^ (1 / 2) ≤ B

theorem NavierStokes.WeightedQuotients.neg_half_power_bound {B t : ℝ} (hB : 1 ≤ B) (ht : 0 < t) (hi : t⁻¹ ≤ B) : t ^ (-(1 / 2)) ≤ B

theorem NavierStokes.WeightedQuotients.comp_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {g : ℝ → ℝ} {s : Set E} {t : Set ℝ} (hs : IsOpen s) (ht : IsOpen t) (hf : ContDiffOn ℝ (↑⊤) f s) (hg : ContDiffOn ℝ (↑⊤) g t) (hmap : Set.MapsTo f s t) {x : E} (hx : x ∈ s) (n : ℕ) {C D : ℝ} (hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C) (hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ D ^ i) : ‖iteratedFDeriv ℝ n (g ∘ f) x‖ ≤ ↑n.factorial * C * D ^ n

The local-open form of the genuine Fréchet chain-rule estimate.

theorem NavierStokes.WeightedQuotients.rpow_comp_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) (hfpos : ∀ x ∈ s, 0 < f x) {x : E} (hx : x ∈ s) (p : ℝ) (n : ℕ) {B : ℝ} (hB : 1 ≤ B) (hp : f x ^ p ≤ B) (hi : (f x)⁻¹ ≤ B) (hjet : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ B) : ‖iteratedFDeriv ℝ n (fun (y : E) => f y ^ p) x‖ ≤ ↑n.factorial * coeffBound p n * B ^ (2 * n + 1)

theorem NavierStokes.WeightedQuotients.norm_jet_const_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ (↑⊤) f x) (c : ℝ) (n : ℕ) : ‖iteratedFDeriv ℝ n (fun (y : E) => c * f y) x‖ = |c| * ‖iteratedFDeriv ℝ n f x‖

noncomputable def NavierStokes.WeightedQuotients.normalizeAt {E : Type u_1} (w : ℝ) (f : E → ℝ) : E → ℝ

The multiplier here is a fixed scalar at the point being estimated.

Equations

• NavierStokes.WeightedQuotients.normalizeAt w f y = w⁻¹ * f y

theorem NavierStokes.WeightedQuotients.normalized_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → ℝ} {s : Set E} (hs : IsOpen s) (hg : ContDiffOn ℝ (↑⊤) g s) {x : E} (hx : x ∈ s) {w B : ℝ} (hw : 0 < w) (n : ℕ) (hjet : ‖iteratedFDeriv ℝ n g x‖ ≤ w * B) : ‖iteratedFDeriv ℝ n (normalizeAt w g) x‖ ≤ B

theorem NavierStokes.WeightedQuotients.normalized_pos {E : Type u_1} {g : E → ℝ} {s : Set E} {w : ℝ} (hw : 0 < w) (hg : ∀ x ∈ s, 0 < g x) {x : E} (hx : x ∈ s) : 0 < normalizeAt w g x

theorem NavierStokes.WeightedQuotients.normalized_bounds {E : Type u_1} {g : E → ℝ} {s : Set E} {w B : ℝ} (hw : 0 < w) (hB : 1 ≤ B) (hg : ∀ x ∈ s, 0 < g x) {x : E} (hx : x ∈ s) (hlo : w / B ≤ g x) (hhi : g x ≤ w * B) : normalizeAt w g x ≤ B ∧ (normalizeAt w g x)⁻¹ ≤ B

theorem NavierStokes.WeightedQuotients.normalized_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → ℝ} {s : Set E} (hg : ContDiffOn ℝ (↑⊤) g s) (w : ℝ) : ContDiffOn ℝ (↑⊤) (normalizeAt w g) s

theorem NavierStokes.WeightedQuotients.jet_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} (h : f =ᶠ[nhds x] g) (n : ℕ) : iteratedFDeriv ℝ n f x = iteratedFDeriv ℝ n g x

theorem NavierStokes.WeightedQuotients.rpow_rescale_eventually {E : Type u_1} [NormedAddCommGroup E] {g : E → ℝ} {s : Set E} (hs : IsOpen s) (hpos : ∀ x ∈ s, 0 < g x) {x : E} (hx : x ∈ s) {w : ℝ} (hw : 0 < w) (p : ℝ) : (fun (y : E) => g y ^ p) =ᶠ[nhds x] fun (y : E) => w ^ p * normalizeAt w g y ^ p

Actual powers separate from a fixed positive rescaling on the given open domain.

theorem NavierStokes.WeightedQuotients.rescaled_rpow_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → ℝ} {s : Set E} (hs : IsOpen s) (hg : ContDiffOn ℝ (↑⊤) g s) (hpos : ∀ x ∈ s, 0 < g x) {x : E} (hx : x ∈ s) {w B : ℝ} (hw : 0 < w) (hB : 1 ≤ B) (p : ℝ) (n : ℕ) (hpow : normalizeAt w g x ^ p ≤ B) (hinv : (normalizeAt w g x)⁻¹ ≤ B) (hjet : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g x‖ ≤ w * B) : ‖iteratedFDeriv ℝ n (fun (y : E) => g y ^ p) x‖ ≤ w ^ p * (↑n.factorial * coeffBound p n) * B ^ (2 * n + 1)

theorem NavierStokes.WeightedQuotients.sqrt_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → ℝ} {s : Set E} (hs : IsOpen s) (hg : ContDiffOn ℝ (↑⊤) g s) (hpos : ∀ x ∈ s, 0 < g x) {x : E} (hx : x ∈ s) {w B : ℝ} (hw : 0 < w) (hB : 1 ≤ B) (n : ℕ) (hlo : w / B ≤ g x) (hjet : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g x‖ ≤ w * B) : ‖iteratedFDeriv ℝ n (fun (y : E) => √(g y)) x‖ ≤ √w * (↑n.factorial * coeffBound (1 / 2) n) * B ^ (2 * n + 1)

Square-root estimates retain exactly the square root of the small weight.

noncomputable def NavierStokes.WeightedQuotients.orderBound (p : ℝ) (n : ℕ) : ℝ

Order bound, given by ∑ k ∈ Finset.range (n + 1), k.factorial * coeffBound p k.

Equations

• NavierStokes.WeightedQuotients.orderBound p n = ∑ k ∈ Finset.range (n + 1), ↑k.factorial * NavierStokes.WeightedQuotients.coeffBound p k

theorem NavierStokes.WeightedQuotients.orderBound_nonneg (p : ℝ) (n : ℕ) : 0 ≤ orderBound p n

theorem NavierStokes.WeightedQuotients.orderBound_le (p : ℝ) {i n : ℕ} (hi : i ≤ n) : ↑i.factorial * coeffBound p i ≤ orderBound p n

theorem NavierStokes.WeightedQuotients.rpow_comp_jets_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) (hfpos : ∀ x ∈ s, 0 < f x) {x : E} (hx : x ∈ s) (p : ℝ) (n : ℕ) {B : ℝ} (hB : 1 ≤ B) (hp : f x ^ p ≤ B) (hi : (f x)⁻¹ ≤ B) (hjet : ∀ i ≤ n, ‖iteratedFDeriv ℝ i f x‖ ≤ B) {i : ℕ} (hin : i ≤ n) : ‖iteratedFDeriv ℝ i (fun (y : E) => f y ^ p) x‖ ≤ orderBound p n * B ^ (2 * n + 1)

def NavierStokes.WeightedQuotients.chooseSum (n : ℕ) : ℝ

Choose sum, given by ∑ i ∈ Finset.range (n + 1), (n.choose i : ℝ).

Equations

• NavierStokes.WeightedQuotients.chooseSum n = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i)

theorem NavierStokes.WeightedQuotients.chooseSum_nonneg (n : ℕ) : 0 ≤ chooseSum n

theorem NavierStokes.WeightedQuotients.mul_jets_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {s : Set E} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) (hg : ContDiffOn ℝ (↑⊤) g s) {x : E} (hx : x ∈ s) (n : ℕ) {C D : ℝ} (hC : 0 ≤ C) (_hD : 0 ≤ D) (hfj : ∀ i ≤ n, ‖iteratedFDeriv ℝ i f x‖ ≤ C) (hgj : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g x‖ ≤ D) : ‖iteratedFDeriv ℝ n (fun (y : E) => f y * g y) x‖ ≤ chooseSum n * C * D

A common bound for each input jet yields the usual Leibniz bound.

theorem NavierStokes.WeightedQuotients.signed_rescale_eventually {E : Type u_1} [NormedAddCommGroup E] {g r : E → ℝ} {s : Set E} (hs : IsOpen s) (hpos : ∀ x ∈ s, 0 < g x) {x : E} (hx : x ∈ s) {w : ℝ} (hw : 0 < w) : (fun (y : E) => r y / (2 * √(g y))) =ᶠ[nhds x] fun (y : E) => √w / 2 * (normalizeAt w r y * normalizeAt w g y ^ (-(1 / 2)))

theorem NavierStokes.WeightedQuotients.signed_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g r : E → ℝ} {s : Set E} (hs : IsOpen s) (hg : ContDiffOn ℝ (↑⊤) g s) (hr : ContDiffOn ℝ (↑⊤) r s) (hpos : ∀ x ∈ s, 0 < g x) {x : E} (hx : x ∈ s) {w B : ℝ} (hw : 0 < w) (hB : 1 ≤ B) (n : ℕ) (hlo : w / B ≤ g x) (hgj : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g x‖ ≤ w * B) (hrj : ∀ i ≤ n, ‖iteratedFDeriv ℝ i r x‖ ≤ w * B) : ‖iteratedFDeriv ℝ n (fun (y : E) => r y / (2 * √(g y))) x‖ ≤ √w * (chooseSum n * orderBound (-(1 / 2)) n / 2) * B ^ (2 * n + 2)

Signed updates inherit the same half-weight as the primary square root.

def NavierStokes.WeightedQuotients.PolyBound {X : Type u_1} (s : Set X) (S T f : X → ℝ) : Prop

An upper bound with a fixed finite power of each allowed large scale. The controlled function need not have any regularity.

Equations

• NavierStokes.WeightedQuotients.PolyBound s S T f = ∃ (C : ℝ), 1 ≤ C ∧ ∃ (K : ℕ) (N : ℕ), ∀ x ∈ s, f x ≤ C * S x ^ K * T x ^ N

theorem NavierStokes.WeightedQuotients.PolyBound.mono {X : Type u_1} {s : Set X} {S T f g : X → ℝ} (hf : PolyBound s S T f) (h : ∀ x ∈ s, g x ≤ f x) : PolyBound s S T g

theorem NavierStokes.WeightedQuotients.polyBound_one {X : Type u_1} {s : Set X} {S T : X → ℝ} : PolyBound s S T fun (x : X) => 1

theorem NavierStokes.WeightedQuotients.polyBound_zero {X : Type u_1} {s : Set X} {S T : X → ℝ} : PolyBound s S T fun (x : X) => 0

theorem NavierStokes.WeightedQuotients.PolyBound.add {X : Type u_1} {s : Set X} {S T f g : X → ℝ} (hS : ∀ x ∈ s, 1 ≤ S x) (hT : ∀ x ∈ s, 1 ≤ T x) (hf : PolyBound s S T f) (hg : PolyBound s S T g) : PolyBound s S T fun (x : X) => f x + g x

theorem NavierStokes.WeightedQuotients.PolyBound.sum {X : Type u_1} {s : Set X} {S T : X → ℝ} {ι : Type u_2} (u : Finset ι) (F : ι → X → ℝ) (hS : ∀ x ∈ s, 1 ≤ S x) (hT : ∀ x ∈ s, 1 ≤ T x) (hF : ∀ i ∈ u, PolyBound s S T (F i)) : PolyBound s S T fun (x : X) => ∑ i ∈ u, F i x

theorem NavierStokes.WeightedQuotients.PolyBound.pow {X : Type u_1} {s : Set X} {S T f : X → ℝ} (_hS : ∀ x ∈ s, 1 ≤ S x) (_hT : ∀ x ∈ s, 1 ≤ T x) (hf : PolyBound s S T f) (hf0 : ∀ x ∈ s, 0 ≤ f x) (k : ℕ) : PolyBound s S T fun (x : X) => f x ^ k

theorem NavierStokes.WeightedQuotients.PolyBound.const_mul {X : Type u_1} {s : Set X} {S T f : X → ℝ} (hS : ∀ x ∈ s, 1 ≤ S x) (hT : ∀ x ∈ s, 1 ≤ T x) (hf : PolyBound s S T f) {a : ℝ} (ha : 0 ≤ a) : PolyBound s S T fun (x : X) => a * f x

noncomputable def NavierStokes.WeightedQuotients.envelope {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (w g r : E → ℝ) (n : ℕ) (x : E) : ℝ

A finite envelope of the input jets and the positive denominator lower bound. This function is never differentiated.

Equations

• NavierStokes.WeightedQuotients.envelope w g r n x = 1 + w x / g x + ∑ i ∈ Finset.range (n + 1), (‖iteratedFDeriv ℝ i g x‖ / w x + ‖iteratedFDeriv ℝ i r x‖ / w x)

theorem NavierStokes.WeightedQuotients.envelope_bounds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {w g r : E → ℝ} {x : E} (hw : 0 < w x) (hg : 0 < g x) (n : ℕ) : 1 ≤ envelope w g r n x ∧ w x / envelope w g r n x ≤ g x ∧ (∀ i ≤ n, ‖iteratedFDeriv ℝ i g x‖ ≤ w x * envelope w g r n x) ∧ ∀ i ≤ n, ‖iteratedFDeriv ℝ i r x‖ ≤ w x * envelope w g r n x

theorem NavierStokes.WeightedQuotients.envelope_polyBound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {S T w g r : E → ℝ} (hS : ∀ x ∈ s, 1 ≤ S x) (hT : ∀ x ∈ s, 1 ≤ T x) (hlower : PolyBound s S T fun (x : E) => w x / g x) (hg : ∀ (n : ℕ), PolyBound s S T fun (x : E) => ‖iteratedFDeriv ℝ n g x‖ / w x) (hr : ∀ (n : ℕ), PolyBound s S T fun (x : E) => ‖iteratedFDeriv ℝ n r x‖ / w x) (n : ℕ) : PolyBound s S T (envelope w g r n)

theorem NavierStokes.WeightedQuotients.weighted_half_control {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {S T w g r : E → ℝ} (hs : IsOpen s) (hS : ∀ x ∈ s, 1 ≤ S x) (hT : ∀ x ∈ s, 1 ≤ T x) (hw : ∀ x ∈ s, 0 < w x) (hpos : ∀ x ∈ s, 0 < g x) (hg : ContDiffOn ℝ (↑⊤) g s) (hr : ContDiffOn ℝ (↑⊤) r s) (hlower : PolyBound s S T fun (x : E) => w x / g x) (hgj : ∀ (n : ℕ), PolyBound s S T fun (x : E) => ‖iteratedFDeriv ℝ n g x‖ / w x) (hrj : ∀ (n : ℕ), PolyBound s S T fun (x : E) => ‖iteratedFDeriv ℝ n r x‖ / w x) : (∀ (n : ℕ), PolyBound s S T fun (x : E) => ‖iteratedFDeriv ℝ n (fun (y : E) => √(g y)) x‖ / √(w x)) ∧ ∀ (n : ℕ), PolyBound s S T fun (x : E) => ‖iteratedFDeriv ℝ n (fun (y : E) => r y / (2 * √(g y))) x‖ / √(w x)

All input jets carry w; the square root and arbitrary signed quotient carry exactly sqrt w, with only polynomial changes in the allowed scales.

theorem NavierStokes.WeightedQuotients.polyBound_of_lower {E : Type u_1} {s : Set E} {S T w g : E → ℝ} (hS : ∀ x ∈ s, 1 ≤ S x) (hT : ∀ x ∈ s, 1 ≤ T x) (hg : ∀ x ∈ s, 0 < g x) {c₀ : ℝ} (hc₀ : 0 < c₀) (K N : ℕ) (hlower : ∀ x ∈ s, c₀ * w x / (S x ^ K * T x ^ N) ≤ g x) : PolyBound s S T fun (x : E) => w x / g x

An explicit weighted lower estimate supplies the reciprocal envelope. This assumption is pointwise, with no normalized smooth factor.

theorem NavierStokes.WeightedQuotients.polyBound_of_weighted {E : Type u_1} {s : Set E} {S T w F : E → ℝ} (hS : ∀ x ∈ s, 1 ≤ S x) (hT : ∀ x ∈ s, 1 ≤ T x) (hw : ∀ x ∈ s, 0 < w x) {C : ℝ} (hC : 0 ≤ C) (K N : ℕ) (hbound : ∀ x ∈ s, F x ≤ C * S x ^ K * T x ^ N * w x) : PolyBound s S T fun (x : E) => F x / w x

Convert the usual weighted upper inequality to the envelope notation.

@[reducible, inline]

abbrev NavierStokes.WeightedQuotients.edgeStrip {E : Type u_1} (U : Set E) : Set (E × ℝ)

Edge strip: an abbreviation for U ×ˢ Ioo 0 1.

Equations

• NavierStokes.WeightedQuotients.edgeStrip U = U ×ˢ Set.Ioo 0 1

def NavierStokes.WeightedQuotients.WeightedJets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (U : Set E) (S f : E × ℝ → ℝ) : Prop

All full derivative tensors satisfy an exponential weight times fixed powers of the allowed scale and inverse edge distance.

Equations

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

def NavierStokes.WeightedQuotients.LocallyBoundedScale {E : Type u_1} [NormedAddCommGroup E] (U : Set E) (S : E × ℝ → ℝ) : Prop

An external scale may vary with parameters, but is locally bounded at the edge. Any fixed S ≥ 1 satisfies this condition.

Equations

• NavierStokes.WeightedQuotients.LocallyBoundedScale U S = ∀ x ∈ U, ∃ V ∈ nhds x, ∃ (M : ℝ), 1 ≤ M ∧ ∀ y ∈ V ∩ U, ∀ δ ∈ Set.Ioo 0 1, S (y, δ) ≤ M

theorem NavierStokes.WeightedQuotients.locallyBoundedScale_const {E : Type u_1} [NormedAddCommGroup E] (U : Set E) {S : ℝ} (hS : 1 ≤ S) : LocallyBoundedScale U fun (x : E × ℝ) => S

theorem NavierStokes.WeightedQuotients.sqrt_edge (c δ : ℝ) : √(FlatCutoff.edge c δ) = FlatCutoff.edge (c / 2) δ

theorem NavierStokes.WeightedQuotients.inverse_distance_one_le {E : Type u_1} {U : Set E} {p : E × ℝ} (hp : p ∈ edgeStrip U) : 1 ≤ p.2⁻¹

theorem NavierStokes.WeightedQuotients.WeightedJets.of_bounds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} {U : Set E} {S f : E × ℝ → ℝ} (hS : ∀ p ∈ edgeStrip U, 1 ≤ S p) (h : ∀ (n : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (K : ℕ) (N : ℕ), ∀ p ∈ edgeStrip U, ‖iteratedFDeriv ℝ n f p‖ ≤ C * S p ^ K * FlatCutoff.edge c p.2 / p.2 ^ N) : WeightedJets c U S f

The hypotheses are inequalities for the input's actual derivatives.

theorem NavierStokes.WeightedQuotients.weighted_half_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} {U : Set E} (hU : IsOpen U) {S g r : E × ℝ → ℝ} (hS : ∀ p ∈ edgeStrip U, 1 ≤ S p) (hpos : ∀ p ∈ U ×ˢ Set.Ioi 0, 0 < g p) (hg : ContDiffOn ℝ (↑⊤) g (U ×ˢ Set.Ioi 0)) (hr : ContDiffOn ℝ (↑⊤) r (U ×ˢ Set.Ioi 0)) (hlower : PolyBound (edgeStrip U) S (fun (p : E × ℝ) => p.2⁻¹) fun (p : E × ℝ) => FlatCutoff.edge c p.2 / g p) (hgj : WeightedJets c U S g) (hrj : WeightedJets c U S r) : (WeightedJets (c / 2) U S fun (p : E × ℝ) => √(g p)) ∧ WeightedJets (c / 2) U S fun (p : E × ℝ) => r p / (2 * √(g p))

theorem NavierStokes.WeightedQuotients.WeightedJets.localGaussian {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} {U : Set E} {S f : E × ℝ → ℝ} (hS : ∀ p ∈ edgeStrip U, 1 ≤ S p) (hscale : LocallyBoundedScale U S) (hf : WeightedJets c U S f) : FlatZeroExtension.LocalGaussianJets c U f

theorem NavierStokes.WeightedQuotients.weighted_zero_extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) {U : Set E} (hU : IsOpen U) {S g r : E × ℝ → ℝ} (hS : ∀ p ∈ edgeStrip U, 1 ≤ S p) (hscale : LocallyBoundedScale U S) (hpos : ∀ p ∈ U ×ˢ Set.Ioi 0, 0 < g p) (hg : ContDiffOn ℝ (↑⊤) g (U ×ˢ Set.Ioi 0)) (hr : ContDiffOn ℝ (↑⊤) r (U ×ˢ Set.Ioi 0)) (hlower : PolyBound (edgeStrip U) S (fun (p : E × ℝ) => p.2⁻¹) fun (p : E × ℝ) => FlatCutoff.edge c p.2 / g p) (hgj : WeightedJets c U S g) (hrj : WeightedJets c U S r) : ContDiffOn ℝ (↑⊤) (FlatZeroExtension.zeroExtension fun (p : E × ℝ) => √(g p)) (U ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) (FlatZeroExtension.zeroExtension fun (p : E × ℝ) => r p / (2 * √(g p))) (U ×ˢ Set.univ) ∧ ∀ (n : ℕ), ∀ x ∈ U, iteratedFDeriv ℝ n (FlatZeroExtension.zeroExtension fun (p : E × ℝ) => √(g p)) (x, 0) = 0 ∧ iteratedFDeriv ℝ n (FlatZeroExtension.zeroExtension fun (p : E × ℝ) => r p / (2 * √(g p))) (x, 0) = 0

Joint smooth zero extension, and vanishing of every full edge tensor, derived solely from weighted input-jet inequalities and a positive lower bound.

theorem NavierStokes.WeightedQuotients.weighted_zero_extension_of_bounds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) {U : Set E} (hU : IsOpen U) {S g r : E × ℝ → ℝ} (hS : ∀ p ∈ edgeStrip U, 1 ≤ S p) (hscale : LocallyBoundedScale U S) (hpos : ∀ p ∈ U ×ˢ Set.Ioi 0, 0 < g p) (hg : ContDiffOn ℝ (↑⊤) g (U ×ˢ Set.Ioi 0)) (hr : ContDiffOn ℝ (↑⊤) r (U ×ˢ Set.Ioi 0)) {c₀ : ℝ} (hc₀ : 0 < c₀) (K₀ N₀ : ℕ) (hlower : ∀ p ∈ edgeStrip U, c₀ * FlatCutoff.edge c p.2 / (S p ^ K₀ * p.2⁻¹ ^ N₀) ≤ g p) (hgBounds : ∀ (n : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (K : ℕ) (N : ℕ), ∀ p ∈ edgeStrip U, ‖iteratedFDeriv ℝ n g p‖ ≤ C * S p ^ K * FlatCutoff.edge c p.2 / p.2 ^ N) (hrBounds : ∀ (n : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (K : ℕ) (N : ℕ), ∀ p ∈ edgeStrip U, ‖iteratedFDeriv ℝ n r p‖ ≤ C * S p ^ K * FlatCutoff.edge c p.2 / p.2 ^ N) : ContDiffOn ℝ (↑⊤) (FlatZeroExtension.zeroExtension fun (p : E × ℝ) => √(g p)) (U ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) (FlatZeroExtension.zeroExtension fun (p : E × ℝ) => r p / (2 * √(g p))) (U ×ˢ Set.univ) ∧ ∀ (n : ℕ), ∀ x ∈ U, iteratedFDeriv ℝ n (FlatZeroExtension.zeroExtension fun (p : E × ℝ) => √(g p)) (x, 0) = 0 ∧ iteratedFDeriv ℝ n (FlatZeroExtension.zeroExtension fun (p : E × ℝ) => r p / (2 * √(g p))) (x, 0) = 0

Direct interface using only the original weighted input inequalities.

theorem NavierStokes.WeightedQuotients.zeroExtension_sqrt_sq {E : Type u_1} {U : Set E} {g : E × ℝ → ℝ} (hpos : ∀ p ∈ U ×ˢ Set.Ioi 0, 0 < g p) {p : E × ℝ} (hp : p.1 ∈ U) : FlatZeroExtension.zeroExtension (fun (p : E × ℝ) => √(g p)) p ^ 2 = FlatZeroExtension.zeroExtension g p

theorem NavierStokes.WeightedQuotients.zeroExtension_signed_identity {E : Type u_1} {U : Set E} {g r : E × ℝ → ℝ} (hpos : ∀ p ∈ U ×ˢ Set.Ioi 0, 0 < g p) {p : E × ℝ} (hp : p.1 ∈ U) : 2 * FlatZeroExtension.zeroExtension (fun (p : E × ℝ) => √(g p)) p * FlatZeroExtension.zeroExtension (fun (p : E × ℝ) => r p / (2 * √(g p))) p = FlatZeroExtension.zeroExtension r p