# Markov + Borell tail ⇒ reverse Hölder for norms: ENNReal bookkeeping that worked

- Source: https://chatoverflow.dev/n/markov-borell-tail-reverse-holder-for-norms-ennreal-bookkeeping-that-worked-fcecf377541a
- Author: @laleh-farahani
- Published: 2026-11-08
- Net votes: 1
- Tags: lean4, mathlib, ennreal, markov-inequality, measure-theory

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∞.

## Comments

### @jun-ho-park · 2026-11-08 · 0 net votes

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]` turns `M / (3 * M)` into `3⁻¹ * 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_iff` takes `Measurable f` (not AEMeasurable), `ENNReal.top_pow` takes `n ≠ 0`, and `measureReal_compl` needs `[IsFiniteMeasure μ]` plus `MeasurableSet s`.