awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : G
⊢ (↑(↑((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) c) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) 1 ⋯ hμs c) : α →ₘ[μ] G) : α → G)
have h : EventuallyEq.{u_1, u_4} (β := G) (ae μ)
  (fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 sorry hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      c)
  (s.indicator fun (x : α) ↦ c)
Tactic: grw [indicatorConstLp_coeFn, condExpInd_ae_eq_condExpIndSMul hm (hm s hs) hμs,
    condExpIndSMul_ae_eq_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : G
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (a : α) ↦
      HSMul.hSMul (α := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a)
        c)
    (s.indicator fun (x : α) ↦ c)
have h : EventuallyEq.{u_1, u_4} (β := G) (ae μ)
  (fun (a : α) ↦ HSMul.hSMul (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 sorry hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a) c)
  (s.indicator fun (x : α) ↦ c)
Tactic: rw [condExpL2_indicator_of_measurable hm hs hμs (1 : ℝ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : G
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (a : α) ↦ HSMul.hSMul (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 ⋯ hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a) c)
    (s.indicator fun (x : α) ↦ c)
have h : ∀ (x : α)
  (hx :
    Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 sorry hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)),
  HSMul.hSMul (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 sorry hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) c =
    s.indicator (fun (x : α) ↦ c) x
Tactic: filter_upwards [@indicatorConstLp_coeFn α _ _ 2 μ _ s (hm s hs) hμs (1 : ℝ)] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : G
x : α
hx : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 ⋯ hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)
⊢ HSMul.hSMul (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 ⋯ hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) c =
    s.indicator (fun (x : α) ↦ c) x
have h : HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) x) c = s.indicator (fun (x : α) ↦ c) x
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : G
x : α
hx : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 ⋯ hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)
⊢ HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) x) c = s.indicator (fun (x : α) ↦ c) x
have pos : ∀ (hx_mem : x ∈ s), HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) x) c = s.indicator (fun (x : α) ↦ c) x
Tactic: by_cases hx_mem : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : G
x : α
hx : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 ⋯ hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)
pos : ∀ (hx_mem : x ∈ s), HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) x) c = s.indicator (fun (x : α) ↦ c) x
⊢ HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) x) c = s.indicator (fun (x : α) ↦ c) x
have neg : ∀ (hx_mem : x ∉ s), HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) x) c = s.indicator (fun (x : α) ↦ c) x
Tactic: by_cases hx_mem : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
E : Type u_7
inst_1 : NormedAddCommGroup E
inst_2 : PartialOrder E
inst_3 : NormedSpace ℝ E
inst_4 : IsOrderedModule ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx : 0 ≤ x
⊢ LE.le (α := ↥(Lp E 1 μ)) (0 : ↥(Lp E 1 μ)) ((condExpInd E hm μ s : (a : E) → ↥(Lp E 1 μ)) x : ↥(Lp E 1 μ))
have rw : EventuallyLE.{u_1, u_7} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E)
  (↑(↑((condExpInd E hm μ s : (a : E) → ↥(Lp E 1 μ)) x) : α →ₘ[μ] E) : α → E)
Tactic: rw [← coeFn_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
E : Type u_7
inst_1 : NormedAddCommGroup E
inst_2 : PartialOrder E
inst_3 : NormedSpace ℝ E
inst_4 : IsOrderedModule ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx : 0 ≤ x
⊢ EventuallyLE.{u_1, u_7} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E)
    (↑(↑((condExpInd E hm μ s : (a : E) → ↥(Lp E 1 μ)) x) : α →ₘ[μ] E) : α → E)
have refine : (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] E) : α → E)
Tactic: refine EventuallyLE.trans_eq ?_ (condExpInd_ae_eq_condExpIndSMul hm hs hμs x).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F'
inst_2 : NormedSpace 𝕜 F'
inst_3 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_4 : SigmaFinite (μ.trim hm)
inst_5 : CompleteSpace F'
c : 𝕜
f : ↥(Lp F' 1 μ)
⊢ (condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (c • f) =
    HSMul.hSMul (β := ↥(Lp F' 1 μ)) c ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f : ↥(Lp F' 1 μ))
have refine : ∀ (c : 𝕜) (s : Set α) (x : F'),
  (condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) (c • x) =
    HSMul.hSMul (β := ↥(Lp F' 1 μ)) c ((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) x : ↥(Lp F' 1 μ))
Tactic: refine L1.setToL1_smul (dominatedFinMeasAdditive_condExpInd F' hm μ) ?_ c f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : F'
⊢ Eq (α := ↥(Lp F' 1 μ))
    ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
        (↑(simpleFunc.indicatorConst 1 (s := s) hs hμs x) : ↥(Lp F' 1 μ)) :
      ↥(Lp F' 1 μ))
    ((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) x : ↥(Lp F' 1 μ))
have rw : Eq (α := ↥(Lp F' 1 μ))
  ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (indicatorConstLp (s := s) 1 hs hμs x) : ↥(Lp F' 1 μ))
  ((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) x : ↥(Lp F' 1 μ))
Tactic: rw [Lp.simpleFunc.coe_indicatorConst]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have refine_1 : ∀ (c : F') {s_1 : Set α} (hs : MeasurableSet s_1)
  (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (fun (f : ↥(Lp F' 1 μ)) ↦
      Eq.{u_3 + 1} (α := F')
        (∫ (x : α) in s,
          (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
        (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
    (↑(simpleFunc.indicatorConst 1 (s := s_1) hs sorry c) : ↥(Lp F' 1 μ))
Tactic: refine @Lp.induction _ _ _ _ _ _ _ ENNReal.one_ne_top
    (fun f : α →₁[μ] F' => ∫ x in s, condExpL1CLM F' hm μ f x ∂μ = ∫ x in s, f x ∂μ) ?_ ?_
    (isClosed_eq ?_ ?_) f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  ∀ (c : F') {s_1 : Set α} (hs : MeasurableSet s_1)
    (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (fun (f : ↥(Lp F' 1 μ)) ↦
        Eq.{u_3 + 1} (α := F')
          (∫ (x : α) in s,
            (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
          (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
      (↑(simpleFunc.indicatorConst 1 (s := s_1) hs ⋯ c) : ↥(Lp F' 1 μ))
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have refine_2 : ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
  Disjoint (Function.support f) (Function.support g) →
    (fun (f : ↥(Lp F' 1 μ)) ↦
          Eq.{u_3 + 1} (α := F')
            (∫ (x : α) in s,
              (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
            (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
        (MemLp.toLp f hf) →
      (fun (f : ↥(Lp F' 1 μ)) ↦
            Eq.{u_3 + 1} (α := F')
              (∫ (x : α) in s,
                (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
              (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
          (MemLp.toLp g hg) →
        (fun (f : ↥(Lp F' 1 μ)) ↦
            Eq.{u_3 + 1} (α := F')
              (∫ (x : α) in s,
                (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
              (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
          (MemLp.toLp f hf + MemLp.toLp g hg)
Tactic: refine @Lp.induction _ _ _ _ _ _ _ ENNReal.one_ne_top
    (fun f : α →₁[μ] F' => ∫ x in s, condExpL1CLM F' hm μ f x ∂μ = ∫ x in s, f x ∂μ) ?_ ?_
    (isClosed_eq ?_ ?_) f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  ∀ (c : F') {s_1 : Set α} (hs : MeasurableSet s_1)
    (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (fun (f : ↥(Lp F' 1 μ)) ↦
        Eq.{u_3 + 1} (α := F')
          (∫ (x : α) in s,
            (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
          (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
      (↑(simpleFunc.indicatorConst 1 (s := s_1) hs ⋯ c) : ↥(Lp F' 1 μ))
refine_2 :
  ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      (fun (f : ↥(Lp F' 1 μ)) ↦
            Eq.{u_3 + 1} (α := F')
              (∫ (x : α) in s,
                (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
              (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
          (MemLp.toLp f hf) →
        (fun (f : ↥(Lp F' 1 μ)) ↦
              Eq.{u_3 + 1} (α := F')
                (∫ (x : α) in s,
                  (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
                (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
            (MemLp.toLp g hg) →
          (fun (f : ↥(Lp F' 1 μ)) ↦
              Eq.{u_3 + 1} (α := F')
                (∫ (x : α) in s,
                  (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
                (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
            (MemLp.toLp f hf + MemLp.toLp g hg)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have refine_3 : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp F' 1 μ)) ↦
  ∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ
Tactic: refine @Lp.induction _ _ _ _ _ _ _ ENNReal.one_ne_top
    (fun f : α →₁[μ] F' => ∫ x in s, condExpL1CLM F' hm μ f x ∂μ = ∫ x in s, f x ∂μ) ?_ ?_
    (isClosed_eq ?_ ?_) f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  ∀ (c : F') {s_1 : Set α} (hs : MeasurableSet s_1)
    (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (fun (f : ↥(Lp F' 1 μ)) ↦
        Eq.{u_3 + 1} (α := F')
          (∫ (x : α) in s,
            (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
          (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
      (↑(simpleFunc.indicatorConst 1 (s := s_1) hs ⋯ c) : ↥(Lp F' 1 μ))
refine_2 :
  ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      (fun (f : ↥(Lp F' 1 μ)) ↦
            Eq.{u_3 + 1} (α := F')
              (∫ (x : α) in s,
                (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
              (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
          (MemLp.toLp f hf) →
        (fun (f : ↥(Lp F' 1 μ)) ↦
              Eq.{u_3 + 1} (α := F')
                (∫ (x : α) in s,
                  (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
                (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
            (MemLp.toLp g hg) →
          (fun (f : ↥(Lp F' 1 μ)) ↦
              Eq.{u_3 + 1} (α := F')
                (∫ (x : α) in s,
                  (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
                (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
            (MemLp.toLp f hf + MemLp.toLp g hg)
refine_3 :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp F' 1 μ)) ↦
    ∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have refine_4 : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp F' 1 μ)) ↦
  ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
Tactic: refine @Lp.induction _ _ _ _ _ _ _ ENNReal.one_ne_top
    (fun f : α →₁[μ] F' => ∫ x in s, condExpL1CLM F' hm μ f x ∂μ = ∫ x in s, f x ∂μ) ?_ ?_
    (isClosed_eq ?_ ?_) f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : F'
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x_1 : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
                  (↑(simpleFunc.indicatorConst 1 (s := t) ht ⋯ x) : ↥(Lp F' 1 μ))) :
              α →ₘ[μ] F') :
          α → F')
        x_1 ∂μ)
    (∫ (x_1 : α) in s,
      (↑(↑(↑(simpleFunc.indicatorConst 1 (s := t) ht ⋯ x) : ↥(Lp F' 1 μ)) : α →ₘ[μ] F') : α → F') x_1 ∂μ)
have refine_1 : Eq.{u_3 + 1} (α := F')
  (∫ (x_1 : α) in s, (↑(↑((condExpInd F' hm μ t : (a : F') → ↥(Lp F' 1 μ)) x) : α →ₘ[μ] F') : α → F') x_1 ∂μ)
  (∫ (x_1 : α) in s, (↑(↑(↑(simpleFunc.indicatorConst 1 (s := t) ht sorry x) : ↥(Lp F' 1 μ)) : α →ₘ[μ] F') : α → F') x_1 ∂μ)
Tactic: simp_rw [condExpL1CLM_indicatorConst ht hμt.ne x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : F'
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x_1 : α) in s, (↑(↑((condExpInd F' hm μ t : (a : F') → ↥(Lp F' 1 μ)) x) : α →ₘ[μ] F') : α → F') x_1 ∂μ)
    (∫ (x_1 : α) in s,
      (↑(↑(↑(simpleFunc.indicatorConst 1 (s := t) ht ⋯ x) : ↥(Lp F' 1 μ)) : α →ₘ[μ] F') : α → F') x_1 ∂μ)
have refine_1 : ∫ (x_1 : α) in s, (↑(↑((condExpInd F' hm μ t : (a : F') → ↥(Lp F' 1 μ)) x) : α →ₘ[μ] F') : α → F') x_1 ∂μ =
  μ.real (t ∩ s) • x
Tactic: rw [Lp.simpleFunc.coe_indicatorConst, setIntegral_indicatorConstLp (hm _ hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f_1 : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
hg :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp)) :
              α →ₘ[μ] F') :
          α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
have refine_2 : Eq.{u_3 + 1} (α := F')
  (∫ (x : α) in s,
    (↑(↑(HAdd.hAdd (α := ↥(Lp F' 1 μ)) (β := ↥(Lp F' 1 μ))
                ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp) : ↥(Lp F' 1 μ))
                ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp) : ↥(Lp F' 1 μ))) :
            α →ₘ[μ] F') :
        α → F')
      x ∂μ)
  (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
Tactic: simp_rw [(condExpL1CLM F' hm μ).map_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f_1 : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
hg :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑(HAdd.hAdd (α := ↥(Lp F' 1 μ)) (β := ↥(Lp F' 1 μ))
                  ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp) : ↥(Lp F' 1 μ))
                  ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp) : ↥(Lp F' 1 μ))) :
              α →ₘ[μ] F') :
          α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
have refine_2 : Eq.{u_3 + 1} (α := F')
  (∫ (x : α) in s,
    HAdd.hAdd (α := α → F') (β := α → F')
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
      x ∂μ)
  (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
Tactic: rw [setIntegral_congr_ae (hm s hs) ((Lp.coeFn_add (condExpL1CLM F' hm μ (hf_Lp.toLp f))
      (condExpL1CLM F' hm μ (hg_Lp.toLp g))).mono fun x hx _ => hx)]