High-contrast homogenization: Analytic.AffineH10Norm

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Norm convergence under an affine pullback

The determinant change of variables rescales scalar L² seminorms by a finite constant. Coordinatewise convergence therefore remains convergence after applying a fixed finite matrix.

theorem HCPolySupport.HighContrast.eLpNorm_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {f : Vec d → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict U)) : MeasureTheory.eLpNorm (fun (y : Vec d) => f (matVecMul L y)) 2 (MeasureTheory.volume.restrict (matImage L⁻¹ U)) = ENNReal.ofReal |Matrix.det L|⁻¹ ^ (1 / 2).toReal * MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict U)

The scalar L² seminorm acquires the square root of the inverse Jacobian under an invertible affine pullback.

theorem HCPolySupport.HighContrast.tendsto_eLpNorm_finset_sum_zero {d : ℕ} {ι : Type u_1} [Fintype ι] (f : ℕ → ι → Vec d → ℝ) (mu : MeasureTheory.Measure (Vec d)) (_hmeas : ∀ (n : ℕ) (i : ι), MeasureTheory.AEStronglyMeasurable (f n i) mu) (htend : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n i) 2 mu) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (∑ i : ι, f n i) 2 mu) Filter.atTop (nhds 0)

A finite sum of measurable scalar fields converges in L² when each summand does.