Power perspective from Holder with infinite moments allowed
AutoSamplingTheory.TechnicalLemmas.Measure.PowerPerspective.lintegral_perspective_le · theorem · Teaching coverage
Statement
Let mu be any measure on a measurable space and a,b be almost-everywhere measurable extended nonnegative functions. Suppose b is positive and finite almost everywhere and its integral B is positive and finite. For real q>1, the qth power of integral a divided by B^(q-1) is at most the integral of a^q/b^(q-1). Neither the numerator integral nor the right-hand integral is assumed finite.
All objects and hypotheses
- Any measurable space and measure mu; no probability or sigma-finiteness assumption is required for this scalar inequality.
- a,b are ENNReal-valued and a.e. measurable. The denominator b is nonzero and finite mu-a.e.
- The integral of b is nonzero and finite, and real q>1.
- The integral of a and of a^q/b^(q-1) may be infinite. This general measure inequality is an expanded ingredient, not a printed paper theorem.
Mathematical proof
1. Reconstruct the numerator pointwise
Set F=a^q/b^(q-1), alpha=1/q and beta=1-1/q. Positive finite b permits cancellation of b^beta, while a may be zero or infinite. Therefore F^alpha b^beta=a almost everywhere.
Corresponding Lean step
ENNReal.div_rpow_of_nonneg, rpow_mul and div_mul_cancel with explicit nonzero/finite denominator.
2. Apply nonnegative integral Holder
The exponents alpha,beta are nonnegative and sum to one. Extended nonnegative Holder gives A<=C^(1/q) B^beta for A=integral a and C=integral F. This theorem does not require either A or C finite.
Corresponding Lean step
ENNReal.lintegral_mul_norm_pow_le and lintegral_congr_ae use the reconstruction, retaining infinite branches.
3. Raise the inequality to q
Since q>0, raising both sides preserves order. Real-power multiplication identities hold in ENNReal for these nonnegative powers and give A^q<=C B^(q-1).
Corresponding Lean step
ENNReal.rpow_le_rpow, mul_rpow_of_nonneg and rpow_mul; exact scalar exponent identities.
4. Divide by the positive finite denominator integral
B is positive and finite, so B^(q-1) is nonzero and finite. The extended-real division equivalence gives the claimed perspective inequality without converting an infinite quantity to a real number.
Corresponding Lean step
ENNReal.div_le_iff, rpow_pos and rpow_ne_top_of_nonneg.
Lean statement · lintegral_perspective_le
The extended nonnegative integral power-perspective inequality with only positive finite denominator conditions.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem lintegral_perspective_le {X : Type*} [MeasurableSpace X] (μ : Measure X)
(a b : X → ℝ≥0∞) (ha : AEMeasurable a μ) (hb : AEMeasurable b μ)
(hbpos : ∀ᵐ x ∂μ, b x ≠ 0 ∧ b x ≠ ⊤)
(hB0 : (∫⁻ x, b x ∂μ) ≠ 0) (hBtop : (∫⁻ x, b x ∂μ) ≠ ⊤)
(q : ℝ) (hq : 1 < q) :
(∫⁻ x, a x ∂μ)^q / (∫⁻ x, b x ∂μ)^(q-1) ≤
∫⁻ x, a x^q / b x^(q-1) ∂μLean proof · lintegral_perspective_le
Direct Holder, pointwise reconstruction and exact power/division algebra; no assumed perspective or moment inequality.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem lintegral_perspective_le {X : Type*} [MeasurableSpace X] (μ : Measure X)
(a b : X → ℝ≥0∞) (ha : AEMeasurable a μ) (hb : AEMeasurable b μ)
(hbpos : ∀ᵐ x ∂μ, b x ≠ 0 ∧ b x ≠ ⊤)
(hB0 : (∫⁻ x, b x ∂μ) ≠ 0) (hBtop : (∫⁻ x, b x ∂μ) ≠ ⊤)
(q : ℝ) (hq : 1 < q) :
(∫⁻ x, a x ∂μ)^q / (∫⁻ x, b x ∂μ)^(q-1) ≤
∫⁻ x, a x^q / b x^(q-1) ∂μ := by
have hq0 : 0 < q := by linarith
have hi : 0 ≤ 1/q := by positivity
have hj : 0 ≤ 1-1/q := by rw [sub_nonneg,div_le_one hq0]; linarith
have he1 : q*(1/q) = 1 := by field_simp
have he2 : (q-1)*(1/q) = 1-1/q := by field_simp
have he3 : (1-1/q)*q = q-1 := by field_simp
have hrec : (fun x => (a x^q / b x^(q-1))^(1/q) * b x^(1-1/q)) =ᵐ[μ] a := by
filter_upwards [hbpos] with x hx
rw [ENNReal.div_rpow_of_nonneg _ _ hi, ← ENNReal.rpow_mul,
← ENNReal.rpow_mul,he1,he2,ENNReal.rpow_one]
exact ENNReal.div_mul_cancel
(ne_of_gt (ENNReal.rpow_pos (pos_iff_ne_zero.mpr hx.1) hx.2))
(ENNReal.rpow_ne_top_of_nonneg hj hx.2)
have h := ENNReal.lintegral_mul_norm_pow_le
((ha.pow_const q).div (hb.pow_const (q-1))) hb hi hj (by ring : 1/q+(1-1/q)=1)
change (∫⁻ x, (a x^q / b x^(q-1))^(1/q) * b x^(1-1/q) ∂μ) ≤
(∫⁻ x, a x^q / b x^(q-1) ∂μ)^(1/q) * (∫⁻ x, b x ∂μ)^(1-1/q) at h
rw [lintegral_congr_ae hrec] at h
have hh := ENNReal.rpow_le_rpow h hq0.le
rw [ENNReal.mul_rpow_of_nonneg _ _ hq0.le, ← ENNReal.rpow_mul,
← ENNReal.rpow_mul,he3,mul_comm (1/q) q,he1,ENNReal.rpow_one] at hh
exact (ENNReal.div_le_iff
(ne_of_gt (ENNReal.rpow_pos (pos_iff_ne_zero.mpr hB0) hBtop))
(ENNReal.rpow_ne_top_of_nonneg (by linarith) hBtop)).mpr hh
end AutoSamplingTheory.TechnicalLemmas.Measure.PowerPerspectiveScope and omitted-condition boundaries
- Expanded bounded-displacement Gaussian mixture ingredient of SPHMC Lemma6.3(ii). The actual coupling is supplied; choosing a single truncation proxy before all q remains separate. No marginal moment conclusion, complete Wasserstein/Renyi API, proxy-warmness, sampler or query-cost theorem.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- ENNReal.lintegral_mul_norm_pow_le
- ENNReal.div_le_iff
- ENNReal.rpow_mul
Mathematical sources
- Chen, Chewi, Lu and Zhang, SPHMC v1 Lemma6.3(ii) — Expanded proof of the bounded-displacement Gaussian reverse-transport ingredient; original truncation composition separate.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.