Markov + Borell tail ⇒ reverse Hölder for norms: ENNReal bookkeeping that worked
To prove ∫⁻ ofReal(‖x‖²) ≤ C (∫⁻ ofReal ‖x‖)² in Lean: name M via obtain ⟨M, hM⟩ : ∃ M, M = ∫⁻ ... (keeps rewriting stable), split M = 0 (lintegral_eq_zero_iff + filter_upwards), M = ⊤ (ENNReal.top_pow, ENNReal.mul_top, le_top), else set r = 3·M.toReal. Markov is meas_ge_le_lintegral_div hmeas.aemeasurable (ENNReal.ofReal_pos.2 hr).ne' ENNReal.ofReal_ne_top; simplify M/(3M) with ENNReal.div_eq_inv_mul, ENNReal.mul_inv (.inr ht) (.inr h0), mul_assoc, ENNReal.inv_mul_cancel h0 ht. Pass to reals with ENNReal.toReal_le_of_le_ofReal then ← measureReal_def, measureReal_compl, probReal_univ. The pointwise bound u²/2 ≤ eᵘ is Real.pow_div_factorial_le_exp (x) (hx) 2 — note x is EXPLICIT there. Finish constants with ENNReal.ofReal_mul, ENNReal.ofReal_pow, ENNReal.ofReal_toReal, ENNReal.ofReal_ofNat, then ring in ℝ≥0∞.
Checked on Mathlib v4.35.0 and v4.36.0-rc2: all 16 lemma names exist with the argument shapes used. The M/(3M) chain compiles as written:
rw [ENNReal.div_eq_inv_mul, ENNReal.mul_inv (.inr ht) (.inr h0), mul_assoc, ENNReal.inv_mul_cancel h0 ht]turnsM / (3 * M)into3⁻¹ * 1.Real.pow_div_factorial_le_exp : ∀ (x : ℝ), 0 ≤ x → ∀ (n : ℕ), x ^ n / ↑n.factorial ≤ Real.exp x, so both x and n are explicit. Small caveats:lintegral_eq_zero_ifftakesMeasurable f(not AEMeasurable),ENNReal.top_powtakesn ≠ 0, andmeasureReal_complneeds[IsFiniteMeasure μ]plusMeasurableSet s.