Differentiation and estimates for the actual locally finite cutoff-flow sum.

theorem AVenhance.Infra.Section4.amnr_cutoff_word_sum {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {U : Set AmnrSpace} (hU : IsOpen U) {N : ℕ} {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiffOn ℝ (↑N) b U) (F : ℤ → AmnrSpace → ℝ) (hF : ∀ (l : ℤ), ContDiffOn ℝ (↑N) (F l) U) (w : List (Option (Fin 2))) (hw : w.length ≤ N) {z : AmnrSpace} (hz : z ∈ U) : ∃ (s : Finset ℤ), s.card ≤ 3 ∧ amnrWord b w (fun (y : AmnrSpace) => ∑' (l : ℤ), I.hatXiML m l y.1 * F l y) z = ∑ l ∈ s, amnrWord b w ((fun (y : AmnrSpace) => I.hatXiML m l y.1) * F l) z

A finite local representation of every ordered derivative of a cutoff sum.

theorem AVenhance.Infra.Section4.amnr_cutoff_tsum_contDiffOn {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {U : Set AmnrSpace} (hU : IsOpen U) {N : ℕ} (F : ℤ → AmnrSpace → ℝ) (hF : ∀ (l : ℤ), ContDiffOn ℝ (↑N) (F l) U) : ContDiffOn ℝ (↑N) (fun (y : AmnrSpace) => ∑' (l : ℤ), I.hatXiML m l y.1 * F l y) U

Local finite sums inherit the regularity of the actual summands.

theorem AVenhance.Infra.Section4.amnrFlowAverageA0Plus_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {U : Set AmnrSpace} (hU : IsOpen U) {N : ℕ} (j k i p : Fin 2) (hleft : ∀ (l : ℤ), ContDiffOn ℝ (↑N) (fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2 j i) U) (hright : ∀ (l : ℤ), ContDiffOn ℝ (↑N) (fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2 k p) U) : ContDiffOn ℝ (↑N) (amnrFlowAverageA0Plus I hΦ m j k i p) U

Joint smoothness of the actual left-Jacobian flow-product average.

theorem AVenhance.Infra.Section4.amnrWord_mul_abs_le_at {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f g : AmnrSpace → ℝ} {N : ℕ} (hb : ContDiffOn ℝ (↑N) b U) (hf : ContDiffOn ℝ (↑N) f U) (hg : ContDiffOn ℝ (↑N) g U) {S H F G : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hF : 0 ≤ F) (_hG : 0 ≤ G) (w : List (Option (Fin 2))) (hw : amnrBudget w ≤ N) {z : AmnrSpace} (hz : z ∈ U) (hfb : ∀ (v : List (Option (Fin 2))), v.Sublist w → |amnrWord b v f z| ≤ F * amnrWeight S H v) (hgb : ∀ (v : List (Option (Fin 2))), v.Sublist w → |amnrWord b v g z| ≤ G * amnrWeight S H v) : |amnrWord b w (f * g) z| ≤ 2 ^ w.length * F * G * amnrWeight S H w

Pointwise mixed Leibniz bounds require quantitative hypotheses only at that point; regularity is local on the surrounding open set.

theorem AVenhance.Infra.Section4.amnr_cutoff_word_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiffOn ℝ (↑(Nstar β)) b U) (F : ℤ → AmnrSpace → ℝ) (hF : ∀ (l : ℤ), ContDiffOn ℝ (↑(Nstar β)) (F l) U) {S X : ℝ} (hS : 0 ≤ S) (hX : 0 ≤ X) (hbound : ∀ (l : ℤ) (v : List (Option (Fin 2))), IsAmnrMixedWord v → amnrBudget v ≤ Nstar β → ∀ z ∈ U, |z.1 - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m → |amnrWord b v (F l) z| ≤ X * amnrWeight S (tauP β I.Λ m)⁻¹ v) (w : List (Option (Fin 2))) (hw : IsAmnrMixedWord w) (hbudget : amnrBudget w ≤ Nstar β) {z : AmnrSpace} (hz : z ∈ U) : |amnrWord b w (fun (y : AmnrSpace) => ∑' (l : ℤ), I.hatXiML m l y.1 * F l y) z| ≤ 3 * 2 ^ Nstar β * I.Chat * X * amnrWeight S (tauP β I.Λ m)⁻¹ w

Higher cutoff-sum bound from localized bounds on its primitive factors. The actual cutoff jets and their support are proved, rather than assumed.