Sharp factorial resummation in the averaged composition estimate.

noncomputable def AVenhance.Infra.Ergodic.compositionPartitionBound {n : ℕ} (c : OrderedFinpartition n) (Cf r CX R : ℝ) : ℝ

The uniform coefficient attached to one ordered partition.

Equations

• AVenhance.Infra.Ergodic.compositionPartitionBound c Cf r CX R = (∏ b : Fin c.length, CX * ↑(c.partSize b).factorial * R ^ c.partSize b) * (Cf * ↑c.length.factorial / r ^ c.length)

theorem AVenhance.Infra.Ergodic.compositionPartitionBound_nonneg {n : ℕ} (c : OrderedFinpartition n) {Cf r CX R : ℝ} (hCf : 0 ≤ Cf) (hr : 0 < r) (hCX : 0 ≤ CX) (hR : 0 ≤ R) : 0 ≤ compositionPartitionBound c Cf r CX R

theorem AVenhance.Infra.Ergodic.compositionJetTerm_bound {d n : ℕ} (hn : 0 < n) (X : PeriodicVolumePreservingDiffeomorphism d) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hper : Torus.IsZdPeriodic f) {Cf r CX R : ℝ} (hCX : 0 ≤ CX) (hR : 0 ≤ R) {p : ENNReal} (hp0 : p ≠ 0) (hpt : p ≠ ⊤) (hfbound : ∀ (k : ℕ) (j : Fin k → Fin d), 0 < k → MeasureTheory.eLpNorm (spatialJet k f j) p (MeasureTheory.volume.restrict (Torus.unitCell d)) ≤ ENNReal.ofReal (Cf * ↑k.factorial / r ^ k)) (hXbound : ∀ (k : ℕ) (v : Fin k → Fin d), 0 < k → ∀ (x : Homogenization.Vec d) (i : Fin d), |spatialJet k X.toFun v x i| ≤ CX * ↑k.factorial * R ^ k) (w : Fin n → Fin d) (c : OrderedFinpartition n) (j : Fin c.length → Fin d) : MeasureTheory.eLpNorm (compositionJetTerm f X.toFun w c j) p (MeasureTheory.volume.restrict (Torus.unitCell d)) ≤ ENNReal.ofReal (compositionPartitionBound c Cf r CX R)

Each term has precisely one averaged outer derivative.

theorem AVenhance.Infra.Ergodic.compositionPartitionBound_sum {d n : ℕ} (hn : 0 < n) {Cf r CX R : ℝ} (hr : 0 < r) : ∑ c : OrderedFinpartition n, ∑ _j : Fin c.length → Fin d, compositionPartitionBound c Cf r CX R = Cf * R ^ n * ↑n.factorial * (↑d * CX / r) * (1 + ↑d * CX / r) ^ (n - 1)

Finite coordinate assignments contribute d^k, and partition weights resum to n! A(1+A)^(n-1).

theorem AVenhance.Infra.Ergodic.compositionPartitionBound_sum_le {d n : ℕ} (hn : 0 < n) {Cf r CX R : ℝ} (hCf : 0 ≤ Cf) (hr : 0 < r) (hCX : 0 ≤ CX) (hR : 0 ≤ R) : ∑ c : OrderedFinpartition n, ∑ _j : Fin c.length → Fin d, compositionPartitionBound c Cf r CX R ≤ Cf * ↑n.factorial / (r / (R * (r + ↑d * CX))) ^ n

The exact factorial envelope at the composed radius.

theorem AVenhance.Infra.Ergodic.spatialJet_comp_eLpNorm_le {d n : ℕ} (hn : 0 < n) (X : PeriodicVolumePreservingDiffeomorphism d) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hper : Torus.IsZdPeriodic f) {Cf r CX R : ℝ} (hCf : 0 ≤ Cf) (hr : 0 < r) (hCX : 0 ≤ CX) (hR : 0 ≤ R) {p : ENNReal} (hp : 1 ≤ p) (hpt : p ≠ ⊤) (hfbound : ∀ (k : ℕ) (j : Fin k → Fin d), 0 < k → MeasureTheory.eLpNorm (spatialJet k f j) p (MeasureTheory.volume.restrict (Torus.unitCell d)) ≤ ENNReal.ofReal (Cf * ↑k.factorial / r ^ k)) (hXbound : ∀ (k : ℕ) (v : Fin k → Fin d), 0 < k → ∀ (x : Homogenization.Vec d) (i : Fin d), |spatialJet k X.toFun v x i| ≤ CX * ↑k.factorial * R ^ k) (w : Fin n → Fin d) : MeasureTheory.eLpNorm (spatialJet n (f ∘ X.toFun) w) p (MeasureTheory.volume.restrict (Torus.unitCell d)) ≤ ENNReal.ofReal (Cf * ↑n.factorial / (r / (R * (r + ↑d * CX))) ^ n)

Mixed averaged derivative bounds compose without a supremum bound on f.