-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem setIntegral_condExpL1CLM_of_measure_ne_top (f : α →₁[μ] F') (hs : MeasurableSet[m] s)
    (hμs : μ s ≠ ∞) : ∫ x in s, condExpL1CLM F' hm μ f x ∂μ = ∫ x in s, f x ∂μ

Proof state:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp))) x ∂μ =
    ∫ (x : α) in s, (↑↑(MemLp.toLp f hf_Lp) + ↑↑(MemLp.toLp g hg_Lp)) x ∂μ

Tactic:
simp_rw [Pi.add_apply]

Result:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x + ↑↑(MemLp.toLp g hg_Lp) x ∂μ

Proof state:
case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ Continuous fun f => ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ

Tactic:
exact (continuous_setIntegral s).comp (condExpL1CLM F' hm μ).continuous

Result:
no goals

Proof state:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F'
t : Set α
ht : MeasurableSet t
hμt : μ t < ⊤
⊢ ∫ (x_1 : α) in s, ↑↑((condExpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 ht ⋯ x)) x_1 ∂μ =
    ∫ (x_1 : α) in s, ↑↑↑(simpleFunc.indicatorConst 1 ht ⋯ x) x_1 ∂μ

Tactic:
simp_rw [condExpL1CLM_indicatorConst ht hμt.ne x]

Result:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F'
t : Set α
ht : MeasurableSet t
hμt : μ t < ⊤
⊢ ∫ (x_1 : α) in s, ↑↑((condExpInd F' hm μ t) x) x_1 ∂μ =
    ∫ (x_1 : α) in s, ↑↑↑(simpleFunc.indicatorConst 1 ht ⋯ x) x_1 ∂μ

Proof state:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F'
t : Set α
ht : MeasurableSet t
hμt : μ t < ⊤
⊢ ∫ (x_1 : α) in s, ↑↑((condExpInd F' hm μ t) x) x_1 ∂μ = (μ (t ∩ s)).toReal • x

Tactic:
exact setIntegral_condExpInd hs ht hμs hμt.ne x

Result:
no goals

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑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

Result:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∀ (c : F') {s_1 : Set α} (hs : MeasurableSet s_1) (hμs : μ s_1 < ⊤),
    (fun f => ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ)
      ↑(simpleFunc.indicatorConst 1 hs ⋯ c)

case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      (fun f => ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ) (MemLp.toLp f hf) →
        (fun f => ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ) (MemLp.toLp g hg) →
          (fun f => ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ)
            (MemLp.toLp f hf + MemLp.toLp g hg)

case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ Continuous fun f => ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ

case refine_4
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ Continuous fun f => ∫ (x : α) in s, ↑↑f x ∂μ

Proof state:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ

Tactic:
simp_rw [(condExpL1CLM F' hm μ).map_add]

Result:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp) + (condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ