mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ∞ →
        ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯)) x ∂μ =
          ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) x ∂μ

pp: case refine_3
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯))) μ

pp: case refine_4
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
⊢ AEStronglyMeasurable (↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp)) μ

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ∞ →
        ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯)) x ∂μ =
          ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) x ∂μ
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: case inl
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Finite ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)

pp: case inr
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Infinite ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)

Tactic:
·

Goal state after:
case inl
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Finite ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_3
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯))) μ

pp: case refine_4
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
⊢ AEStronglyMeasurable (↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp)) μ

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯))) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_4
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
⊢ AEStronglyMeasurable (↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp)) μ

Tactic:
·

Goal state after:
case refine_4
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
⊢ AEStronglyMeasurable (↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp)) μ
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: case inr
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Infinite ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)

Tactic:
·

Goal state after:
case inr
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Infinite ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ Integrable (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) (μ.restrict s)

pp: case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∀ (c : E'), ∫ (x : α) in s, ⟪c, (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) x⟫ ∂μ = 0

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ Integrable (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦
    ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ

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

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦
    ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_4
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
·

Goal state after:
case refine_4
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ ∫ (x : α) in s, ↑↑f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ∞ →
        ∫ (x : α) in s, ↑↑↑((condExpL2 E'' 𝕜' hm) (T.compLp f)) x ∂μ =
          ∫ (x : α) in s, ↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f)) x ∂μ

pp: case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 E'' 𝕜' hm) (T.compLp f))) μ

pp: case refine_3
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable (↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f))) μ

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ∞ →
        ∫ (x : α) in s, ↑↑↑((condExpL2 E'' 𝕜' hm) (T.compLp f)) x ∂μ =
          ∫ (x : α) in s, ↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f)) x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
⊢ (if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯
    else 0) =ᵐ[μ]
    ↑↑(condExpL1 hm μ f)

pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : ¬Integrable f μ
⊢ (if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯
    else 0) =ᵐ[μ]
    ↑↑(condExpL1 hm μ f)

Tactic:
·

Goal state after:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
⊢ (if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯
    else 0) =ᵐ[μ]
    ↑↑(condExpL1 hm μ f)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
⊢ (if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯) =ᵐ[μ] ↑↑(condExpL1 hm μ f)

Tactic:
by_cases hfm : StronglyMeasurable[m] f

Goal state after:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ (if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯) =ᵐ[μ] ↑↑(condExpL1 hm μ f)

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
⊢ (if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯) =ᵐ[μ] ↑↑(condExpL1 hm μ f)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 E'' 𝕜' hm) (T.compLp f))) μ

pp: case refine_3
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable (↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f))) μ

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 E'' 𝕜' hm) (T.compLp f))) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ (if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯) =ᵐ[μ] ↑↑(condExpL1 hm μ f)

pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
⊢ (if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯) =ᵐ[μ] ↑↑(condExpL1 hm μ f)

Tactic:
·

Goal state after:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ (if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯) =ᵐ[μ] ↑↑(condExpL1 hm μ f)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_3
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable (↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f))) μ

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable (↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f))) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: case refine_1
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun x ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g
f : α → F
hf : MemLp f p μ
hfm : AEStronglyMeasurable f μ
f_Lp : ↥(Lp F p μ) := toLp f hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
⊢ ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑↑↑(Lp.simpleFunc.indicatorConst p ⋯ ⋯ c)

pp: case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun x ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g
f : α → F
hf : MemLp f p μ
hfm : AEStronglyMeasurable f μ
f_Lp : ↥(Lp F p μ) := toLp f hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
⊢ ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P ↑↑(toLp f hf) → P ↑↑(toLp g hg) → P ↑↑(toLp f hf + toLp g hg)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun x ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g
f : α → F
hf : MemLp f p μ
hfm : AEStronglyMeasurable f μ
f_Lp : ↥(Lp F p μ) := toLp f hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
⊢ ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑↑↑(Lp.simpleFunc.indicatorConst p ⋯ ⋯ c)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
⊢ (if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯) =ᵐ[μ] ↑↑(condExpL1 hm μ f)

Tactic:
·

Goal state after:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
⊢ (if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯) =ᵐ[μ] ↑↑(condExpL1 hm μ f)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : ¬m ≤ m₀
⊢ μ[f | m] = 0

pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
⊢ μ[f | m] = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : ¬m ≤ m₀
⊢ μ[f | m] = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] = 0

pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f | m] = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] = 0