Finite coordinate contractions and cutoff scalars preserve the averaged analytic envelope.
theorem
AVenhance.Infra.Section5.slowWord_sum
{ι : Type u_1}
(s : Finset ι)
(f : ι → Homogenization.Vec 2 → ℝ)
(hf : ∀ i ∈ s, ContDiff ℝ (↑⊤) (f i))
(w : List (Fin 2))
:
theorem
AVenhance.Infra.Section5.slowFactor_sum_eLpNorm_le
{ι : Type u_1}
(s : Finset ι)
(f : ι → Homogenization.Vec 2 → ℝ)
(hf : ∀ i ∈ s, ContDiff ℝ (↑⊤) (f i))
{F L : ℝ}
{p : ENNReal}
(hp : 1 ≤ p)
(μ : MeasureTheory.Measure (Homogenization.Vec 2))
(hb :
∀ i ∈ s,
∀ (w : List (Fin 2)),
MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (f i)) p μ ≤ ENNReal.ofReal (F * ↑w.length.factorial * L ^ w.length))
(w : List (Fin 2))
:
MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (∑ i ∈ s, f i)) p μ ≤ ENNReal.ofReal (↑s.card * F * ↑w.length.factorial * L ^ w.length)
theorem
AVenhance.Infra.Section5.slowFactor_cutoff_eLpNorm_le
{f : Homogenization.Vec 2 → ℝ}
{F L ξ : ℝ}
(hξ : |ξ| ≤ 1)
(p : ENNReal)
(μ : MeasureTheory.Measure (Homogenization.Vec 2))
(hb :
∀ (w : List (Fin 2)),
MeasureTheory.eLpNorm (Section4.amnrSpaceWord w f) p μ ≤ ENNReal.ofReal (F * ↑w.length.factorial * L ^ w.length))
(w : List (Fin 2))
:
MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (ξ • f)) p μ ≤ ENNReal.ofReal (F * ↑w.length.factorial * L ^ w.length)
A time-only cutoff with magnitude at most one does not increase any jet.