Averaged norms of the finite coordinate chain-rule terms.
theorem
AVenhance.Infra.Ergodic.continuous_unitCell_memLp
{d : ℕ}
{F : Type u_1}
[NormedAddCommGroup F]
{u : Homogenization.Vec d → F}
(hu : Continuous u)
(p : ENNReal)
:
Smooth functions have every finite Lp norm on the bounded unit cell.
theorem
AVenhance.Infra.Ergodic.eLpNorm_comp_flow_eq
{d : ℕ}
{u : Homogenization.Vec d → ℂ}
(hu : Continuous u)
(hper : Torus.IsZdPeriodic u)
(X : PeriodicVolumePreservingDiffeomorphism d)
{p : ENNReal}
(hp0 : p ≠ 0)
(hpt : p ≠ ⊤)
:
MeasureTheory.eLpNorm (u ∘ X.toFun) p (MeasureTheory.volume.restrict (Torus.unitCell d)) = MeasureTheory.eLpNorm u p (MeasureTheory.volume.restrict (Torus.unitCell d))
Periodic volume-preserving composition preserves finite averaged Lp norms.
theorem
AVenhance.Infra.Ergodic.compositionJetTerm_eLpNorm_le
{d n : ℕ}
{f : Homogenization.Vec d → ℂ}
{X : Homogenization.Vec d → Homogenization.Vec d}
(hf : ContDiff ℝ (↑⊤) f)
(hXs : ContDiff ℝ (↑⊤) X)
(w : Fin n → Fin d)
(c : OrderedFinpartition n)
(j : Fin c.length → Fin d)
{CX R : ℝ}
(hCX : 0 ≤ CX)
(hR : 0 ≤ R)
(hX :
∀ (a : ℕ) (v : Fin a → Fin d),
0 < a → ∀ (x : Homogenization.Vec d) (i : Fin d), |spatialJet a X v x i| ≤ CX * ↑a.factorial * R ^ a)
(p : ENNReal)
(μ : MeasureTheory.Measure (Homogenization.Vec d))
:
MeasureTheory.eLpNorm (compositionJetTerm f X w c j) p μ ≤ ENNReal.ofReal (∏ b : Fin c.length, CX * ↑(c.partSize b).factorial * R ^ c.partSize b) * MeasureTheory.eLpNorm (fun (x : Homogenization.Vec d) => spatialJet c.length f j (X x)) p μ
Uniform flow factors are placed outside the averaged norm.