Source indexedtheorem · leanprover/lean4:v4.32.0

RCLike.aestronglyMeasurable_iff_aestronglyMeasurable_embedRCLike

Carleson.ToMathlib.Analysis.RCLike.Misc · Carleson/ToMathlib/Analysis/RCLike/Misc.lean:19 to 32

Mathematical statement

Exact Lean statement

theorem aestronglyMeasurable_iff_aestronglyMeasurable_embedRCLike {α : Type*}
  {m : MeasurableSpace α} {μ : Measure α} {𝕂 : Type*} [RCLike 𝕂] {f : α → ℝ≥0} :
    AEStronglyMeasurable (⇑(algebraMap ℝ 𝕂) ∘ toReal ∘ f) μ ↔ AEStronglyMeasurable f μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem aestronglyMeasurable_iff_aestronglyMeasurable_embedRCLike {α : Type*}  {m : MeasurableSpace α} {μ : Measure α} {𝕂 : Type*} [RCLike 𝕂] {f : α → ℝ≥0} :    AEStronglyMeasurable (⇑(algebraMap ℝ 𝕂) ∘ toReal ∘ f) μ ↔ AEStronglyMeasurable f μ := by  constructor  · intro hf    have comp_eq : (⇑(algebraMap ℝ 𝕂) ∘ toReal ∘ f) = fun x ↦ ⇑(algebraMap ℝ 𝕂) (f x).toReal := by      ext x      simp    rw [comp_eq] at hf    rwa [IsEmbedding.aestronglyMeasurable_comp_iff, IsEmbedding.aestronglyMeasurable_comp_iff] at hf    · exact (Isometry.isEmbedding fun _ ↦ congrFun rfl)    · exact (algebraMap_isometry ℝ 𝕂).isEmbedding  · intro hf    fun_prop