Exact-weight exponent changes for finitely many initial bands

Only the band exponent changes. The weight, domain, polynomial degree, and finite band cutoff are preserved, including at the spatial edges.

noncomputable def NavierStokes.FiniteHeadClass.comparison {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (N : ℕ) (α β : ℝ) : ℝ

One constant, independent of the point and derivative order, compares the two exponents on the fixed finite set of bands.

Equations

• NavierStokes.FiniteHeadClass.comparison s N α β = 1 + ∑ n ∈ Finset.range N, s.epsilon n ^ (α - β)

theorem NavierStokes.FiniteHeadClass.one_le_comparison {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (N : ℕ) (α β : ℝ) : 1 ≤ comparison s N α β

theorem NavierStokes.FiniteHeadClass.comparison_nonneg {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (N : ℕ) (α β : ℝ) : 0 ≤ comparison s N α β

theorem NavierStokes.FiniteHeadClass.ratio_le_comparison {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) {N n : ℕ} (hn : n < N) (α β : ℝ) : s.epsilon n ^ (α - β) ≤ comparison s N α β

theorem NavierStokes.FiniteHeadClass.exponent_le {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) {N n : ℕ} (hn : n < N) (α β : ℝ) : s.epsilon n ^ α ≤ comparison s N α β * s.epsilon n ^ β

theorem NavierStokes.FiniteHeadClass.majorant_le {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β C : ℝ} {N n p : ℕ} {x : D} (hn : n < N) (hC : 0 ≤ C) (hw : 0 ≤ w n x) : WeightedClasses.majorant s w α C p n x ≤ WeightedClasses.majorant s w β (C * comparison s N α β) p n x

No derivative of the weight or spatial cutoff is used here.

theorem NavierStokes.FiniteHeadClass.jet_eq_zero {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {f : D → E} (hz : ∀ x ∈ s.domain, f x = 0) {x : D} (hx : x ∈ s.domain) (j : ℕ) : iteratedFDeriv ℝ j f x = 0

Vanishing on the same open domain gives vanishing of every actual ambient derivative there, without any global vanishing assumption.

theorem NavierStokes.FiniteHeadClass.jet_bound {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {f : ℕ → D → E} {N m p : ℕ} {α β C : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hC : 0 ≤ C) (hb : ∀ n < N, ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n) x‖ ≤ WeightedClasses.majorant s w α C p n x) (hz : ∀ (n : ℕ), N ≤ n → ∀ x ∈ s.domain, f n x = 0) (n : ℕ) (x : D) : x ∈ s.domain → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n) x‖ ≤ WeightedClasses.majorant s w β (C * comparison s N α β) p n x

Quantitative exponent transfer for a finite prefix of actual jets. The initial bound is needed only on n < N. Its degree p is unchanged. The multiplier works uniformly for any additional labels in the data.

theorem NavierStokes.FiniteHeadClass.memClass_of_finite_bands {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (N : ℕ) (hz : ∀ (n : ℕ), N ≤ n → ∀ x ∈ s.domain, f n x = 0) : WeightedClasses.MemClass s w β f

A weighted class supported in the fixed finite initial bands has any chosen exponent with exactly the original weight.

theorem NavierStokes.FiniteHeadClass.all_exponents {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (N : ℕ) (hz : ∀ (n : ℕ), N ≤ n → ∀ x ∈ s.domain, f n x = 0) (β : ℝ) : WeightedClasses.MemClass s w β f

theorem NavierStokes.FiniteHeadClass.meanClass_all_exponents {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MeanClass s α f) (N : ℕ) (hz : ∀ (n : ℕ), N ≤ n → ∀ x ∈ s.domain, f n x = 0) (β : ℝ) : WeightedClasses.MeanClass s β f

The radial weight zeta is retained at the same spatial edges.

theorem NavierStokes.FiniteHeadClass.waveClass_all_exponents {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.WaveClass s P α f) (N : ℕ) (hz : ∀ (n : ℕ), N ≤ n → ∀ x ∈ s.domain, f n x = 0) (β : ℝ) : WeightedClasses.WaveClass s P β f

Both the square-root radial weight and the given slot envelope remain exactly the same; no lower bound for either is required.

theorem NavierStokes.FiniteHeadClass.unweightedClass_all_exponents {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.UnweightedClass s α f) (N : ℕ) (hz : ∀ (n : ℕ), N ≤ n → ∀ x ∈ s.domain, f n x = 0) (β : ℝ) : WeightedClasses.UnweightedClass s β f