Fixed derivative shifts in factorial analytic bounds.

theorem AVenhance.Infra.Section5.slowFactor_shift_factorial_le (n j : ℕ) : ↑(n + j).factorial ≤ ↑j.factorial * 2 ^ j * ↑n.factorial * 2 ^ n

A fixed derivative shift costs a fixed factorial and doubles the rate.

theorem AVenhance.Infra.Section5.slowFactor_rate_mono {F L L' : ℝ} (hF : 0 ≤ F) (hL : 0 ≤ L) (hLL' : L ≤ L') (n : ℕ) : F * ↑n.factorial * L ^ n ≤ F * ↑n.factorial * L' ^ n

Moving to a larger derivative rate preserves the analytic envelope.

theorem AVenhance.Infra.Section5.slowFactor_word_shift_eLpNorm_le {f : Homogenization.Vec 2 → ℝ} {F L : ℝ} (hF : 0 ≤ F) (hL : 0 ≤ L) (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 (Section4.amnrSpaceWord η f)) p μ ≤ ENNReal.ofReal (F * ↑η.length.factorial * (2 * L) ^ η.length * ↑w.length.factorial * (2 * L) ^ w.length)

Shifting an averaged analytic field by a fixed ordered word.

theorem AVenhance.Infra.Section5.slowFactor_positive_temperature_shift {T : Homogenization.Vec 2 → ℝ} {M L : ℝ} (hM : 0 ≤ M) (hL : 0 ≤ L) (p : ENNReal) (μ : MeasureTheory.Measure (Homogenization.Vec 2)) (hT : ∀ (w : List (Fin 2)), 0 < w.length → MeasureTheory.eLpNorm (Section4.amnrSpaceWord w T) p μ ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)) (η : List (Fin 2)) (hη : 0 < η.length) (w : List (Fin 2)) : MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (Section4.amnrSpaceWord η T)) p μ ≤ ENNReal.ofReal (M * ↑η.length.factorial * (2 * L) ^ η.length * ↑w.length.factorial * (2 * L) ^ w.length)

Only positive T jets are consumed, even when w is empty.