Power perspective from Holder with infinite moments allowed
AutoSamplingTheory.TechnicalLemmas.Measure.PowerPerspective.lintegral_perspective_le · theorem · Teaching coverage
Mathematical 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.
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) ∂μProof roadmap
- 1Reconstruct 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.
- 2Apply 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.
- 3Raise 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).
- 4Divide 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.
Full assumptions and notation
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 verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
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.PowerPerspectiveSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| SPHMC Lemma6.3(ii) invokes Gaussian reverse transport on Euclidean probability measures with marginal Pp membership. | Arbitrary measurable space and measure for the scalar Holder perspective. | generalization | Explicit expanded ingredient with independently proved denominator conditions; finite displacement does not imply marginal moments. |
| The full lemma first chooses one truncation proxy, then applies the Winfinity Gaussian reverse-transport bound for all q>1. | Scalar integral perspective only. | API-limitation | No truncation composition, complete Wasserstein/Renyi API, warmness recursion or sampler cost is claimed. |
| Positive heat time, q>1 and coefficient q/(2tau). | Real q>1; in the consumer tau>0,t>=0 and exact q(q-1)t^2/(2tau) moment and qt^2/(2tau) logarithm bounds. | same | Covariance tau I comes from sqrt(tau) noise. RN direction and denominator law agree. |
| Mixture density, Holder and finite-moment details omitted in the invoked standard reverse-transport step. | Positive finite denominator conditions explicit in shared leaf; all Gaussian mixture densities, actual laws, integrability and log positivity proved in consumer. | source-implicit | No assumed mixture inequality or Gaussian density/moment contract replaces the proof. |
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.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: Explicit generalization beyond Euclidean probability application. — Only MeasurableSpace X and Measure X domain data.
- scopes: Selected expanded prerequisite, not equivalence with complete printed Lemma6.3(ii). — Documentation and publication explicitly keep Gaussian application and truncation separate.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
Scope 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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib 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.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.