Theorem Real.exists_measure_rpow_eq_integral

Modification history

2026-04-08 13:59
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
feat(ContinuousFunctionalCalculus): add integral representation for `x ↦ x ^ p` for `p ∈ (1, 2)` (#37612) …
Deleted Real.exists_measure_rpow_eq_integralView on Github →
2025-05-08 00:39
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
feat(SpecialFunctions): Integral representation of `rpow` over `Ioo 0 1` (#24393) …
Added Real.exists_measure_rpow_eq_integralView on Github →