`PhysFunctionalAnalysis.sqrt_density_memLp` {α : Type*} [MeasurableSpace α] (μ : Measure α) (p : α → ℝ) (hp : Integrable p μ) (hp0 : 0 ≤ᵐ[μ] p) : MemLp (fun x => Real.sqrt (p x)) 2

Proved

PhysFunctionalAnalysis.sqrt_density_memLp

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from PhysFunctionalAnalysis.

PhysFunctionalAnalysis.sqrt_density_memLp {α : Type*} [MeasurableSpace α] (μ : Measure α) (p : α → ℝ) (hp : Integrable p μ) (hp0 : 0 ≤ᵐ[μ] p) : MemLp (fun x => Real.sqrt (p x)) 2 μ

Formalization note: Lean 4 identifier PhysFunctionalAnalysis.sqrt_density_memLp.

Preamble

-- Generated from PhysFunctionalAnalysis.lean — theorem PhysFunctionalAnalysis.sqrt_density_memLp
import Mathlib
import Definitions.Def_PhysFunctionalAnalysis
import Definitions.Def_ChapterA4
open PhysFunctionalAnalysis


open MeasureTheory Set
open scoped ENNReal lp

noncomputable section


open PhysMeasureBasis

Formal statement

theorem PhysFunctionalAnalysis.sqrt_density_memLp {α : Type*} [MeasurableSpace α] (μ : Measure α)
    (p : α → ℝ) (hp : Integrable p μ) (hp0 : 0 ≤ᵐ[μ] p) :
    MemLp (fun x => Real.sqrt (p x)) 2 μ := by sorry

View graph