High-contrast homogenization: Entry.Source.GaugeMoments

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

Source moments from the gauge tail

HC Lemma C.1 (Steps 1–4) supplies the printed route. We use CG's proved growth/doubling calculus, Mathlib's layer cake, and an integrable power-tail envelope to obtain the paper's C(p) * K^C(p) consequence (l.source.whitney). The coefficient here is deliberately nonsharp; HC's sharper coefficient and its sequence triangle inequality are not asserted.

Finiteness is proved in the nonnegative extended integral before deriving MemLp and the real moment bound. The constant precedes every law, gauge and source. The final consumer uses exactly the same Q and p = 2*(d+Q). No new definition or global measurability assumption on the gauge is introduced.

theorem HCPolySupport.HighContrast.Source.source_lintegral_layercake {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (S : Ω → ℝ) (hS : Measurable S) (hS0 : ∀ (ω : Ω), 0 ≤ S ω) {p : ℝ} (hp : 0 < p) : ∫⁻ (ω : Ω), ENNReal.ofReal (S ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, μ (IndependentSums.upperTailEvent S t) * ENNReal.ofReal (t ^ (p - 1))

Layer cake for a nonnegative source, before any finiteness assumption. The pinned Mathlib theorem is MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul in Mathlib.Analysis.SpecialFunctions.Pow.Integral.

theorem HCPolySupport.HighContrast.Source.two_le_twoGrowthWitness (K : ℝ) : 2 ≤ growthBar K

theorem HCPolySupport.HighContrast.Source.one_lt_twoGrowthWitness (K : ℝ) : 1 < growthBar K

theorem HCPolySupport.HighContrast.Source.le_twoGrowthWitness_of_one_lt {K : ℝ} (_hK : 1 < K) : K ≤ growthBar K

theorem HCPolySupport.HighContrast.Source.hasPsiGrowth_twoGrowthWitness_of_growth {Ψ : ℝ → ℝ} {K : ℝ} (hAdmissible : IndependentSums.AdmissiblePsi Ψ) (hK : 1 < K) (hGrowth : IndependentSums.HasPsiGrowth Ψ K) : IndependentSums.HasPsiGrowth Ψ (growthBar K)

theorem HCPolySupport.HighContrast.Source.gauge_inverse_rpow_bound {Ψ : ℝ → ℝ} {K q t : ℝ} (hΨ : IndependentSums.AdmissiblePsi Ψ) (hK : 1 < K) (hg : IndependentSums.HasPsiGrowth Ψ K) (hq : 2 ≤ q) (ht : 1 ≤ t) : (Ψ t)⁻¹ ≤ growthBar K ^ (3 * q ^ 2) * t ^ (-q)

HC C.1 growth gives a global power-tail envelope above one, also for 1 < K < 2.

theorem HCPolySupport.HighContrast.Source.source_lintegral_moment_le_of_power_tail {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (S : Ω → ℝ) (hS : Measurable S) (hS0 : ∀ (ω : Ω), 0 ≤ S ω) {p A : ℝ} (hp : 1 ≤ p) (hA : 0 ≤ A) (htail : ∀ (t : ℝ), 1 ≤ t → μ.real (IndependentSums.upperTailEvent S t) ≤ A * t ^ (-(p + 1))) : ∫⁻ (ω : Ω), ENNReal.ofReal (S ω ^ p) ∂μ ≤ ENNReal.ofReal (p * (1 + A))

A power tail one order above the moment gives a finite layer-cake integral. The elementary bound on (0,1] costs a factor p; no sharp HC coefficient is asserted.

theorem HCPolySupport.HighContrast.Source.source_moment_bound_of_gauge_tail {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Ψ : ℝ → ℝ) (K : ℝ) (S : Ω → ℝ) {p : ℝ} (hp : 1 ≤ p) (hΨ : IndependentSums.AdmissiblePsi Ψ) (hK : 1 < K) (hg : IndependentSums.HasPsiGrowth Ψ K) (hS : Measurable S) (hS0 : ∀ (ω : Ω), 0 ≤ S ω) (htail : ∀ (t : ℝ), 0 < t → μ.real (IndependentSums.upperTailEvent S t) ≤ (Ψ t)⁻¹) : MeasureTheory.MemLp S (ENNReal.ofReal p) μ ∧ MeasureTheory.Integrable (fun (ω : Ω) => S ω ^ p) μ ∧ ∫ (ω : Ω), S ω ^ p ∂μ ≤ p * (1 + growthBar K ^ (3 * (p + 1) ^ 2))

HC C.1's tail-to-moment consequence, with a deliberately nonsharp explicit coefficient. The bound is proved in the nonnegative extended integral before asserting either integrability or membership in L^p. No measurability of the gauge on negative arguments is needed.

theorem HCPolySupport.HighContrast.Source.source_moment_bound (p : ℝ) (hp : 1 ≤ p) : ∃ (C : ℝ), 0 < C ∧ ∀ {Ω : Type u_2} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Ψ : ℝ → ℝ) (K : ℝ) (S : Ω → ℝ), IndependentSums.AdmissiblePsi Ψ → 1 < K → IndependentSums.HasPsiGrowth Ψ K → Measurable S → (∀ (ω : Ω), 0 ≤ S ω) → (∀ (t : ℝ), 0 < t → μ.real (IndependentSums.upperTailEvent S t) ≤ (Ψ t)⁻¹) → MeasureTheory.MemLp S (ENNReal.ofReal p) μ ∧ MeasureTheory.Integrable (fun (ω : Ω) => S ω ^ p) μ ∧ ∫ (ω : Ω), S ω ^ p ∂μ ≤ C * K ^ C

The moment endpoint of the proof of e.source.adapted.bound, with the constant chosen before the probability space, gauge, growth witness and source. One possible constant is C = p * (1 + 2 ^ a) + a + 1, where a = 3 * (p + 1)^2. The fixed enlargement max 2 K ≤ 2 K is absorbed explicitly, so the endpoint retains K > 1.

theorem HCPolySupport.HighContrast.Source.CoarseEllipticityDagger.source_moment_bound (p : ℝ) (hp : 1 ≤ p) : ∃ (C : ℝ), 0 < C ∧ ∀ {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), CoarseEllipticityDagger P γ E Ψ K S → MeasureTheory.MemLp S (ENNReal.ofReal p) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => S a ^ p) P ∧ ∫ (a : CoeffSpace d), S a ^ p ∂P ≤ C * K ^ C

The moment estimate specialized to precisely the dagger fields and probability. The constant still depends only on the moment order.

theorem HCPolySupport.HighContrast.Source.source_selection_moment_bound (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (C : ℝ), 0 < C ∧ 1 ≤ Multiscale.sourceMomentExponent d γ ∧ ↑d + ↑(bigQ d γ) ≤ ↑(Multiscale.sourceMomentExponent d γ) - ↑d ∧ ↑d + ↑(bigQ d γ) ≤ ↑(Multiscale.sourceMomentExponent d γ) - ↑(bigQ d γ) * γ ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), CoarseEllipticityDagger P γ E Ψ K S → MeasureTheory.MemLp S (ENNReal.ofReal ↑(Multiscale.sourceMomentExponent d γ)) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => S a ^ ↑(Multiscale.sourceMomentExponent d γ)) P ∧ ∫ (a : CoeffSpace d), S a ^ ↑(Multiscale.sourceMomentExponent d γ) ∂P ≤ C * K ^ C

The source-moment endpoint: p = 2*(d+Q), with explicit geometric-tail margins d+Q. Substitution in source_moment_bound fixes C from d, γ alone. Neither stationarity, independence, an integrability premise nor ellipticity constants enter.