Indexed weighted classes of actual stripped derivatives

The index is a band, not a differentiable variable. Every derivative below is Mathlib's iteratedFDeriv of the actual coefficient on an open domain. Constants and polynomial degrees are chosen before the band and point.

The statements hold on real normed spaces, in particular on the Euclidean strips used by the construction. Radiality of the prescribed smooth weight is not needed for these closure results.

structure NavierStokes.WeightedClasses.StripData (D : Type u_5) [NormedAddCommGroup D] [NormedSpace ℝ D] : Type u_5

Geometry and positive indexed scales for a stripped coefficient family. epsilon may in particular be Q n ^ h.

• domain : Set D

  Domain of StripData, of type Set D.

• isOpen_domain : IsOpen self.domain
• epsilon : ℕ → ℝ

  Epsilon of StripData, of type ℕ → ℝ.

• epsilon_pos (n : ℕ) : 0 < self.epsilon n
• epsilon_le_one (n : ℕ) : self.epsilon n ≤ 1
• slow : ℕ → ℝ

  Slow of StripData, of type ℕ → ℝ.

• one_le_slow (n : ℕ) : 1 ≤ self.slow n
• delta : D → ℝ

  Delta of StripData, of type D → ℝ.

• delta_pos (x : D) : x ∈ self.domain → 0 < self.delta x
• zeta : D → ℝ

  Zeta of StripData, of type D → ℝ.

• zeta_smooth : ContDiffOn ℝ (↑⊤) self.zeta self.domain
• zeta_nonneg (x : D) : x ∈ self.domain → 0 ≤ self.zeta x

@[reducible, inline]

abbrev NavierStokes.WeightedClasses.EuclideanStripData (d : ℕ) : Type

Euclidean strip data: an abbreviation for StripData (EuclideanSpace ℝ (Fin d)).

Equations

• NavierStokes.WeightedClasses.EuclideanStripData d = NavierStokes.WeightedClasses.StripData (EuclideanSpace ℝ (Fin d))

noncomputable def NavierStokes.WeightedClasses.StripData.growth {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (n : ℕ) (x : D) : ℝ

A common polynomial degree in S and the inverse edge distance is enough: separate finite degrees can always be increased to their sum. The maximum permits arbitrary positive delta, agreeing with delta⁻¹ when delta ≤ 1.

Equations

• s.growth n x = s.slow n * max 1 (s.delta x)⁻¹

theorem NavierStokes.WeightedClasses.StripData.one_le_growth {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (n : ℕ) (x : D) : 1 ≤ s.growth n x

theorem NavierStokes.WeightedClasses.StripData.growth_nonneg {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (n : ℕ) (x : D) : 0 ≤ s.growth n x

theorem NavierStokes.WeightedClasses.StripData.slow_le_growth {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (n : ℕ) (x : D) : s.slow n ≤ s.growth n x

theorem NavierStokes.WeightedClasses.StripData.separate_powers_le_growth {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (p q n : ℕ) (x : D) : s.slow n ^ p * max 1 (s.delta x)⁻¹ ^ q ≤ s.growth n x ^ (p + q)

noncomputable def NavierStokes.WeightedClasses.majorant {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (w : ℕ → D → ℝ) (α C : ℝ) (p n : ℕ) (x : D) : ℝ

Majorant, given by C * s.epsilon n ^ α * s.growth n x ^ p * w n x.

Equations

• NavierStokes.WeightedClasses.majorant s w α C p n x = C * s.epsilon n ^ α * s.growth n x ^ p * w n x

theorem NavierStokes.WeightedClasses.majorant_nonneg {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (w : ℕ → D → ℝ) (α : ℝ) {C : ℝ} (hC : 0 ≤ C) (p n : ℕ) (x : D) (hw : 0 ≤ w n x) : 0 ≤ majorant s w α C p n x

theorem NavierStokes.WeightedClasses.majorant_mono_degree {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (w : ℕ → D → ℝ) (α : ℝ) {C : ℝ} (hC : 0 ≤ C) {p q : ℕ} (hpq : p ≤ q) (n : ℕ) (x : D) (hw : 0 ≤ w n x) : majorant s w α C p n x ≤ majorant s w α C q n x

theorem NavierStokes.WeightedClasses.majorant_mul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (w v : ℕ → D → ℝ) (α β A B : ℝ) (p q n : ℕ) (x : D) : majorant s w α A p n x * majorant s v β B q n x = majorant s (fun (n : ℕ) (x : D) => w n x * v n x) (α + β) (A * B) (p + q) n x

structure NavierStokes.WeightedClasses.MemClass {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : StripData D) (w : ℕ → D → ℝ) (α : ℝ) (f : ℕ → D → E) : Prop

Actual all-order bounds, uniform in band and point. The finite prefix in the last quantifier is useful for the higher Leibniz inequality.

• weight_nonneg (n : ℕ) (x : D) : x ∈ s.domain → 0 ≤ w n x
• smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (f n) s.domain
• bounds (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n) x‖ ≤ majorant s w α C p n x

@[reducible, inline]

abbrev NavierStokes.WeightedClasses.MeanClass {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : StripData D) (α : ℝ) (f : ℕ → D → E) : Prop

Mean class: an abbreviation for MemClass s (fun _ x => s.zeta x) α f.

Equations

• NavierStokes.WeightedClasses.MeanClass s α f = NavierStokes.WeightedClasses.MemClass s (fun (x : ℕ) (x_1 : D) => s.zeta x_1) α f

@[reducible, inline]

abbrev NavierStokes.WeightedClasses.WaveClass {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : StripData D) (P : ℕ → D → ℝ) (α : ℝ) (f : ℕ → D → E) : Prop

Wave class: an abbreviation for MemClass s (fun n x => Real.sqrt (s.zeta x) * P n x) α f.

Equations

• NavierStokes.WeightedClasses.WaveClass s P α f = NavierStokes.WeightedClasses.MemClass s (fun (n : ℕ) (x : D) => √(s.zeta x) * P n x) α f

@[reducible, inline]

abbrev NavierStokes.WeightedClasses.UnweightedClass {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : StripData D) (α : ℝ) (f : ℕ → D → E) : Prop

Unweighted class: an abbreviation for MemClass s (fun _ _ => 1) α f.

Equations

• NavierStokes.WeightedClasses.UnweightedClass s α f = NavierStokes.WeightedClasses.MemClass s (fun (x : ℕ) (x_1 : D) => 1) α f

def NavierStokes.WeightedClasses.StageClasses {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : StripData D) (w : ℕ → D → ℝ) (α : ℕ → ℝ) (f : ℕ → ℕ → D → E) : Prop

Stage constants are deliberately not uniform in the stage index.

Equations

• NavierStokes.WeightedClasses.StageClasses s w α f = ∀ (stage : ℕ), NavierStokes.WeightedClasses.MemClass s w (α stage) (f stage)

def NavierStokes.WeightedClasses.BandBound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (β : ℝ) (a : ℕ → ℝ) : Prop

A bound on a band-dependent scalar. There is no spatial derivative of the discrete band index.

Equations

• NavierStokes.WeightedClasses.BandBound s β a = ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), ‖a n‖ ≤ C * s.epsilon n ^ β * s.slow n ^ p

theorem NavierStokes.WeightedClasses.MemClass.contDiffAt {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : MemClass s w α f) (n : ℕ) {x : D} (hx : x ∈ s.domain) (m : ℕ) : ContDiffAt ℝ (↑m) (f n) x

theorem NavierStokes.WeightedClasses.MemClass.of_separate_bounds {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hsmooth : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) s.domain) (hb : ∀ (m : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ) (q : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n) x‖ ≤ C * s.epsilon n ^ α * s.slow n ^ p * max 1 (s.delta x)⁻¹ ^ q * w n x) : MemClass s w α f

The common-degree definition accepts the manuscript's separate logarithmic and inverse-edge polynomial degrees.

theorem NavierStokes.WeightedClasses.MemClass.zero {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) : MemClass s w α fun (x : ℕ) (x_1 : D) => 0

theorem NavierStokes.WeightedClasses.MemClass.mono_weight {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w v : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : MemClass s w α f) (hv : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ v n x) (hwv : ∀ (n : ℕ), ∀ x ∈ s.domain, w n x ≤ v n x) : MemClass s v α f

theorem NavierStokes.WeightedClasses.MemClass.mono_exponent {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → E} (hf : MemClass s w α f) (hβα : β ≤ α) : MemClass s w β f

theorem NavierStokes.WeightedClasses.MemClass.add {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → D → E} (hf : MemClass s w α f) (hg : MemClass s w α g) : MemClass s w α fun (n : ℕ) (x : D) => f n x + g n x

theorem NavierStokes.WeightedClasses.MemClass.add_min {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {f g : ℕ → D → E} (hf : MemClass s w α f) (hg : MemClass s w β g) : MemClass s w (min α β) fun (n : ℕ) (x : D) => f n x + g n x

theorem NavierStokes.WeightedClasses.MemClass.fderiv {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : MemClass s w α f) : MemClass s w α fun (n : ℕ) => _root_.fderiv ℝ (f n)

theorem NavierStokes.WeightedClasses.MemClass.map {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : MemClass s w α f) (L : E →L[ℝ] F) : MemClass s w α fun (n : ℕ) (x : D) => L (f n x)

theorem NavierStokes.WeightedClasses.MemClass.directional {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : MemClass s w α f) (v : D) : MemClass s w α fun (n : ℕ) (x : D) => (_root_.fderiv ℝ (f n) x) v

theorem NavierStokes.WeightedClasses.MemClass.bilinear {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {s : StripData D} {w v : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → E} {u : ℕ → D → F} (hf : MemClass s w α f) (hu : MemClass s v β u) (L : E →L[ℝ] F →L[ℝ] G) : MemClass s (fun (n : ℕ) (x : D) => w n x * v n x) (α + β) fun (n : ℕ) (x : D) => (L (f n x)) (u n x)

Actual higher Leibniz estimates add the two decay exponents.

theorem NavierStokes.WeightedClasses.MemClass.smul {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w v : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → E} {a : ℕ → D → ℝ} (ha : MemClass s v β a) (hf : MemClass s w α f) : MemClass s (fun (n : ℕ) (x : D) => v n x * w n x) (β + α) fun (n : ℕ) (x : D) => a n x • f n x

theorem NavierStokes.WeightedClasses.MemClass.mul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : StripData D} {w v : ℕ → D → ℝ} {α β : ℝ} {a b : ℕ → D → ℝ} (ha : MemClass s w α a) (hb : MemClass s v β b) : MemClass s (fun (n : ℕ) (x : D) => w n x * v n x) (α + β) fun (n : ℕ) (x : D) => a n x * b n x

theorem NavierStokes.WeightedClasses.MemClass.band_smul {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → E} {a : ℕ → ℝ} (hf : MemClass s w α f) (ha : BandBound s β a) : MemClass s w (α + β) fun (n : ℕ) (x : D) => a n • f n x

theorem NavierStokes.WeightedClasses.MemClass.sum {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α : ℝ} {ι : Type u_5} (t : Finset ι) (u : ι → ℕ → D → E) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hu : ∀ i ∈ t, MemClass s w α (u i)) : MemClass s w α fun (n : ℕ) (x : D) => ∑ i ∈ t, u i n x

theorem NavierStokes.WeightedClasses.unweighted_const {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : StripData D) (c : E) : UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => c

Constant coefficients give nonzero examples of the unweighted class.

theorem NavierStokes.WeightedClasses.unweighted_of_finiteJetBounds {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : StripData D) (a : D → E) (ha : ContDiffOn ℝ (↑⊤) a s.domain) (hb : ∀ (m : ℕ), ∃ (C : ℝ), JetBounds.FiniteJetBound m a s.domain C) : UnweightedClass s 0 fun (x : ℕ) => a

A fixed coefficient with uniform finite jet bounds is an order-zero unweighted coefficient. This connects the class directly to JetBounds.

theorem NavierStokes.WeightedClasses.bandBound_rpow {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : StripData D) (β : ℝ) : BandBound s β fun (n : ℕ) => s.epsilon n ^ β

theorem NavierStokes.WeightedClasses.WaveClass.bilinear_mean {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {s : StripData D} {P : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → E} {g : ℕ → D → F} (hf : WaveClass s P α f) (hg : WaveClass s P β g) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) (L : E →L[ℝ] F →L[ℝ] G) : MeanClass s (α + β) fun (n : ℕ) (x : D) => (L (f n x)) (g n x)

Wave products have the mean weight. This uses the actual Leibniz estimate on coefficients, followed by (sqrt ζ * P)^2 ≤ ζ; no derivative identity for the envelope P is postulated.

theorem NavierStokes.WeightedClasses.WaveClass.mul_mean {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : StripData D} {P : ℕ → D → ℝ} {α β : ℝ} {f g : ℕ → D → ℝ} (hf : WaveClass s P α f) (hg : WaveClass s P β g) (hP0 : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P n x) (hP1 : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ 1) : MeanClass s (α + β) fun (n : ℕ) (x : D) => f n x * g n x

theorem NavierStokes.WeightedClasses.MeanClass.bilinear {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {s : StripData D} {α β : ℝ} {f : ℕ → D → E} {g : ℕ → D → F} (hf : MeanClass s α f) (hg : MeanClass s β g) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (L : E →L[ℝ] F →L[ℝ] G) : MeanClass s (α + β) fun (n : ℕ) (x : D) => (L (f n x)) (g n x)

A normalized bounded radial weight makes the mean class an algebra.

theorem NavierStokes.WeightedClasses.MeanClass.bilinear_wave {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {s : StripData D} {P : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → E} {g : ℕ → D → F} (hf : MeanClass s α f) (hg : WaveClass s P β g) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (L : E →L[ℝ] F →L[ℝ] G) : WaveClass s P (α + β) fun (n : ℕ) (x : D) => (L (f n x)) (g n x)

noncomputable def NavierStokes.WeightedClasses.graphDerivative {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℕ → ℝ) (a : D → ℝ) (e v : D) (f : ℕ → D → E) : ℕ → D → E

An explicit radial graph operator with a band coefficient M and a spatial coefficient a. The two directions can be radial and auxiliary.

Equations

• NavierStokes.WeightedClasses.graphDerivative M a e v f n x = (fderiv ℝ (f n) x) e + M n • a x • (fderiv ℝ (f n) x) v

theorem NavierStokes.WeightedClasses.graphDerivative_eq_along {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℕ → ℝ) (a : D → ℝ) (e v : D) (f : ℕ → D → E) (n : ℕ) (x : D) : graphDerivative M a e v f n x = (fderiv ℝ (f n) x) (e + M n • a x • v)

The expanded operator really is differentiation along its graph vector.

theorem NavierStokes.WeightedClasses.MemClass.graphDerivative {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} {f : ℕ → D → E} {M : ℕ → ℝ} {a : D → ℝ} (hf : MemClass s w α f) (ha : UnweightedClass s 0 fun (x : ℕ) => a) (hM : BandBound s (-κ) M) (hκ : 0 ≤ κ) (e v : D) : MemClass s w (α - κ) (WeightedClasses.graphDerivative M a e v f)

One explicit graph derivative loses at most κ in the band exponent. The coefficient hypothesis is an actual all-jet bound on a, not a claim about the desired output.

noncomputable def NavierStokes.WeightedClasses.graphIterate {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℕ → ℝ) (a : D → ℝ) (e v : D) (f : ℕ → D → E) : ℕ → ℕ → D → E

Graph iterate as an element of ℕ → ℕ → D → E | 0 => f | j + 1 => graphDerivative M a e v (graphIterate M a e v f j).

Equations

• NavierStokes.WeightedClasses.graphIterate M a e v f 0 = f
• NavierStokes.WeightedClasses.graphIterate M a e v f j.succ = NavierStokes.WeightedClasses.graphDerivative M a e v (NavierStokes.WeightedClasses.graphIterate M a e v f j)

theorem NavierStokes.WeightedClasses.MemClass.graphIterate {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} {f : ℕ → D → E} {M : ℕ → ℝ} {a : D → ℝ} (hf : MemClass s w α f) (ha : UnweightedClass s 0 fun (x : ℕ) => a) (hM : BandBound s (-κ) M) (hκ : 0 ≤ κ) (e v : D) (j : ℕ) : MemClass s w (α - ↑j * κ) (WeightedClasses.graphIterate M a e v f j)

Every finite number of explicit graph derivatives has its finite loss. Arbitrarily high additional stripped jets are still controlled at the same resulting exponent, as recorded by MemClass.