Coarse-graining support: Support.Book.Ch04.Internal.PartitionAverageMomentHelpers

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Audit tag (Ch4 rebuild contract CH04_REBUILD_SURFACE_2026-05-16.md)

Internal claim: L^p / eLpNorm and root-comparison helper lemmas that transport integrability and |·|^p integrals along Measure.map equalities and through a.e. translations. These are the algebraic substrate underneath the centered descendant-average finite-moment bounds.

Consumed by: Theorems/PartitionAverageMoments/Rosenthal.lean (integral_abs_finiteSum_pow_rpow_inv_le_rosenthal_uniform_descendants and the public Rosenthal-type endpoints it feeds).

If the single-claim summary above grows into three or more distinct claims, split or refactor per the rebuild contract.

theorem HCPolySupport.integrable_abs_pow_of_map_eq_map {d : ℕ} {P : MeasureTheory.Measure (RegCoeffField d)} {f g : RegCoeffField d → ℝ} {p : ℕ} (hf : Measurable f) (hg : Measurable g) (hmap : MeasureTheory.Measure.map f P = MeasureTheory.Measure.map g P) (hg_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |g a| ^ p) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |f a| ^ p) P

theorem HCPolySupport.integrable_abs_pow_of_map_eq_map_aemeasurable {d : ℕ} {P : MeasureTheory.Measure (RegCoeffField d)} {f g : RegCoeffField d → ℝ} {p : ℕ} (hf : AEMeasurable f P) (hg : AEMeasurable g P) (hmap : MeasureTheory.Measure.map f P = MeasureTheory.Measure.map g P) (hg_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |g a| ^ p) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |f a| ^ p) P

A.e.-measurable version of integrable_abs_pow_of_map_eq_map.

theorem HCPolySupport.integral_abs_pow_eq_of_map_eq_map {d : ℕ} {P : MeasureTheory.Measure (RegCoeffField d)} {f g : RegCoeffField d → ℝ} {p : ℕ} (hf : Measurable f) (hg : Measurable g) (hmap : MeasureTheory.Measure.map f P = MeasureTheory.Measure.map g P) : ∫ (a : RegCoeffField d), |f a| ^ p ∂P = ∫ (a : RegCoeffField d), |g a| ^ p ∂P

theorem HCPolySupport.integral_abs_pow_eq_of_map_eq_map_aemeasurable {d : ℕ} {P : MeasureTheory.Measure (RegCoeffField d)} {f g : RegCoeffField d → ℝ} {p : ℕ} (hf : AEMeasurable f P) (hg : AEMeasurable g P) (hmap : MeasureTheory.Measure.map f P = MeasureTheory.Measure.map g P) : ∫ (a : RegCoeffField d), |f a| ^ p ∂P = ∫ (a : RegCoeffField d), |g a| ^ p ∂P

A.e.-measurable version of integral_abs_pow_eq_of_map_eq_map.

theorem HCPolySupport.integral_abs_pow_rpow_inv_le_iff_of_map_eq_map {d : ℕ} {P : MeasureTheory.Measure (RegCoeffField d)} {f g : RegCoeffField d → ℝ} {p : ℕ} {K : ℝ} (hf : Measurable f) (hg : Measurable g) (hmap : MeasureTheory.Measure.map f P = MeasureTheory.Measure.map g P) : (∫ (a : RegCoeffField d), |f a| ^ p ∂P) ^ (1 / ↑p) ≤ K ↔ (∫ (a : RegCoeffField d), |g a| ^ p ∂P) ^ (1 / ↑p) ≤ K

theorem HCPolySupport.toReal_eLpNorm_eq_integral_abs_pow_rpow_inv {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f : Ω → ℝ} {p : ℕ} (hp : 1 ≤ p) (hf : Measurable f) (hLp_int : MeasureTheory.Integrable (fun (ω : Ω) => |f ω| ^ p) μ) : (MeasureTheory.eLpNorm f (↑p) μ).toReal = (∫ (ω : Ω), |f ω| ^ p ∂μ) ^ (1 / ↑p)

theorem HCPolySupport.toReal_eLpNorm_eq_integral_abs_pow_rpow_inv_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f : Ω → ℝ} {p : ℕ} (hp : 1 ≤ p) (hf : AEMeasurable f μ) (hLp_int : MeasureTheory.Integrable (fun (ω : Ω) => |f ω| ^ p) μ) : (MeasureTheory.eLpNorm f (↑p) μ).toReal = (∫ (ω : Ω), |f ω| ^ p ∂μ) ^ (1 / ↑p)

A.e.-measurable version of toReal_eLpNorm_eq_integral_abs_pow_rpow_inv.

theorem HCPolySupport.integral_abs_finsetSum_pow_rpow_inv_le_sum {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f : ι → Ω → ℝ} {s : Finset ι} {p : ℕ} (hp : 1 ≤ p) (h_meas : ∀ i ∈ s, Measurable (f i)) (hLp_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => |f i ω| ^ p) μ) : (∫ (ω : Ω), |∑ i ∈ s, f i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ ∑ i ∈ s, (∫ (ω : Ω), |f i ω| ^ p ∂μ) ^ (1 / ↑p)

theorem HCPolySupport.integral_abs_finsetSum_pow_rpow_inv_le_sum_aemeasurable {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f : ι → Ω → ℝ} {s : Finset ι} {p : ℕ} (hp : 1 ≤ p) (h_aemeas : ∀ i ∈ s, AEMeasurable (f i) μ) (hLp_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => |f i ω| ^ p) μ) : (∫ (ω : Ω), |∑ i ∈ s, f i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ ∑ i ∈ s, (∫ (ω : Ω), |f i ω| ^ p ∂μ) ^ (1 / ↑p)

A.e.-measurable finite-sum root triangle inequality.

theorem HCPolySupport.integral_abs_sq_rpow_half_le_integral_abs_pow_rpow_inv {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ℝ} {p : ℕ} (hp : 2 ≤ p) (hf : Measurable f) (hLp_int : MeasureTheory.Integrable (fun (ω : Ω) => |f ω| ^ p) μ) : (∫ (ω : Ω), |f ω| ^ 2 ∂μ) ^ (1 / 2) ≤ (∫ (ω : Ω), |f ω| ^ p ∂μ) ^ (1 / ↑p)

theorem HCPolySupport.integral_abs_sq_rpow_half_le_integral_abs_pow_rpow_inv_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ℝ} {p : ℕ} (hp : 2 ≤ p) (hf : AEMeasurable f μ) (hLp_int : MeasureTheory.Integrable (fun (ω : Ω) => |f ω| ^ p) μ) : (∫ (ω : Ω), |f ω| ^ 2 ∂μ) ^ (1 / 2) ≤ (∫ (ω : Ω), |f ω| ^ p ∂μ) ^ (1 / ↑p)

A.e.-measurable version of integral_abs_sq_rpow_half_le_integral_abs_pow_rpow_inv.

theorem HCPolySupport.integral_abs_le_integral_abs_sq_rpow_half {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ℝ} (hf : Measurable f) (hL2_int : MeasureTheory.Integrable (fun (ω : Ω) => |f ω| ^ 2) μ) : ∫ (ω : Ω), |f ω| ∂μ ≤ (∫ (ω : Ω), |f ω| ^ 2 ∂μ) ^ (1 / 2)

theorem HCPolySupport.integral_abs_le_integral_abs_sq_rpow_half_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ℝ} (hf : AEMeasurable f μ) (hL2_int : MeasureTheory.Integrable (fun (ω : Ω) => |f ω| ^ 2) μ) : ∫ (ω : Ω), |f ω| ∂μ ≤ (∫ (ω : Ω), |f ω| ^ 2 ∂μ) ^ (1 / 2)

A.e.-measurable version of integral_abs_le_integral_abs_sq_rpow_half.

theorem HCPolySupport.sum_rpow_inv_le_card_rpow_mul_rpow_sum {ι : Type u_1} {s : Finset ι} {p : ℕ} {f : ι → ℝ} (hp : 1 ≤ p) (hf : ∀ i ∈ s, 0 ≤ f i) : ∑ i ∈ s, f i ^ (1 / ↑p) ≤ ↑s.card ^ (1 - 1 / ↑p) * (∑ i ∈ s, f i) ^ (1 / ↑p)