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∞)
x : G
⊢ Integrable (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) μ
have rw : MemLp (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) 1 μ
Tactic: rw [← memLp_one_iff_integrable]
-- 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∞)
x : G
⊢ ∫⁻ (a : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ =
    ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ
have refine : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ)
  fun (a : α) ↦ ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ
Tactic: refine lintegral_congr_ae ?_
-- 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∞)
x : G
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ)
    fun (a : α) ↦ ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ
have h : ∀ (z : α)
  (hz :
    (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z =
      (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z),
  ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ =
    ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ
Tactic: filter_upwards [condExpIndL1Fin_ae_eq_condExpIndSMul hm hs hμs x] with z hz
-- 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∞)
x : G
z : α
hz :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z =
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z
⊢ ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ =
    ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ
have h : ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ =
  ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ
Tactic: rw [hz]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
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∞)
x : G
⊢ ∫⁻ (x_1 : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) x_1‖ₑ ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal ‖x‖)
have h_eq : ∫⁻ (a : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ =
  ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ
Tactic: have h_eq :
    ∫⁻ a, ‖condExpIndL1Fin hm hs hμs x a‖ₑ ∂μ = ∫⁻ a, ‖condExpIndSMul hm hs hμs x a‖ₑ ∂μ := by
    refine lintegral_congr_ae ?_
    filter_upwards [condExpIndL1Fin_ae_eq_condExpIndSMul hm hs hμs x] with z hz
    rw [hz]
-- 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∞)
x : G
h_eq :
  ∫⁻ (a : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ =
    ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ
⊢ ∫⁻ (x_1 : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) x_1‖ₑ ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal ‖x‖)
have rw : ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ ≤
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ‖x‖ₑ
Tactic: rw [h_eq, ofReal_norm]
-- 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 t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
x : G
⊢ condExpIndL1Fin (s := s ∪ t) hm ⋯ ⋯ x =
    HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := t) hm ht hμt x)
have h : (↑(↑(condExpIndL1Fin (s := s ∪ t) hm sorry sorry x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := t) hm ht hμt x)) :
        α →ₘ[μ] G) :
    α → G)
Tactic: ext1
-- 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 t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
x : G
⊢ (↑(↑(condExpIndL1Fin (s := s ∪ t) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := t) hm ht hμt x)) :
          α →ₘ[μ] G) :
      α → G)
have h : (↑(↑(condExpIndSMul (s := s ∪ t) hm sorry sorry x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_add, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndL1Fin_ae_eq_condExpIndSMul]
-- 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 t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
x : G
⊢ (↑(↑(condExpIndSMul (s := s ∪ t) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
have h : (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
            (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s ∪ t) 2 sorry sorry 1)) :
              ↥(Lp ℝ 2 μ))) :
        α →ₘ[μ] G) :
    α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
Tactic: rw [condExpIndSMul]
-- 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 t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
x : G
⊢ (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s ∪ t) 2 ⋯ ⋯ 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
have h : (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
            (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                  (HAdd.hAdd (α := ↥(Lp ℝ 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)
                    (indicatorConstLp (s := t) 2 ht hμt 1))) :
              ↥(Lp ℝ 2 μ))) :
        α →ₘ[μ] G) :
    α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
Tactic: rw [indicatorConstLp_disjoint_union hs ht hμs hμt hst (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 t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
x : G
⊢ (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                    (HAdd.hAdd (α := ↥(Lp ℝ 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)
                      (indicatorConstLp (s := t) 2 ht hμt 1))) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
have h : (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
            (↑(HAdd.hAdd (α := ↥(lpMeas ℝ ℝ m 2 μ)) (β := ↥(lpMeas ℝ ℝ m 2 μ))
                  ((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1) :
                    ↥(lpMeas ℝ ℝ m 2 μ))
                  ((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := t) 2 ht hμt 1) :
                    ↥(lpMeas ℝ ℝ m 2 μ))) :
              ↥(Lp ℝ 2 μ))) :
        α →ₘ[μ] G) :
    α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
Tactic: rw [map_add]
-- 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 t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
x : G
⊢ (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑(HAdd.hAdd (α := ↥(lpMeas ℝ ℝ m 2 μ)) (β := ↥(lpMeas ℝ ℝ m 2 μ))
                    ((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                        (indicatorConstLp (s := s) 2 hs hμs 1) :
                      ↥(lpMeas ℝ ℝ m 2 μ))
                    ((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                        (indicatorConstLp (s := t) 2 ht hμt 1) :
                      ↥(lpMeas ℝ ℝ m 2 μ))) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
have h : (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
            (HAdd.hAdd (α := ↥(Lp ℝ 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := t) 2 ht hμt 1)) :
                ↥(Lp ℝ 2 μ)))) :
        α →ₘ[μ] G) :
    α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
Tactic: push_cast
-- 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 t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
x : G
⊢ (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (HAdd.hAdd (α := ↥(Lp ℝ 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := t) 2 ht hμt 1)) :
                  ↥(Lp ℝ 2 μ)))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
have h : (↑(↑(HAdd.hAdd (α := ↥(Lp G 2 μ))
            ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ)))
            ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := t) 2 ht hμt 1)) :
                ↥(Lp ℝ 2 μ)))) :
        α →ₘ[μ] G) :
    α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
Tactic: rw [map_add]
-- 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 t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
x : G
⊢ (↑(↑(HAdd.hAdd (α := ↥(Lp G 2 μ))
              ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)))
              ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := t) 2 ht hμt 1)) :
                  ↥(Lp ℝ 2 μ)))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
have h : HAdd.hAdd (α := α → G)
    (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G)
    (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := t) 2 ht hμt 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
  HAdd.hAdd (α := α → G)
    (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G)
    (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := t) 2 ht hμt 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G)
Tactic: grw [Lp.coeFn_add]
-- 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)
x y : G
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
have pos : ∀ (hs : MeasurableSet s),
  condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
Tactic: by_cases hs : MeasurableSet 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)
x y : G
pos :
  ∀ (hs : MeasurableSet s),
    condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
have neg : ∀ (hs : ¬MeasurableSet s),
  condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
Tactic: by_cases hs : MeasurableSet 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)
x y : G
hs : ¬MeasurableSet s
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
have neg : 0 = HAdd.hAdd (α := ↥(Lp G 1 μ)) 0 0
Tactic: simp_rw [condExpIndL1_of_not_measurableSet hs]
-- 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)
x y : G
hs : ¬MeasurableSet s
⊢ 0 = HAdd.hAdd (α := ↥(Lp G 1 μ)) 0 0
have neg : Eq (α := ↥(Lp G 1 μ)) 0 0
Tactic: rw [zero_add]
-- 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)
x y : G
hs : MeasurableSet s
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
have pos : ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
Tactic: by_cases hμs : μ 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)
x y : G
hs : MeasurableSet s
pos :
  ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
have neg : ∀ (hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
Tactic: by_cases hμs : μ 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)
x y : G
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
have pos : 0 = HAdd.hAdd (α := ↥(Lp G 1 μ)) 0 0
Tactic: simp_rw [condExpIndL1_of_measure_eq_top hμ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)
x y : G
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 = HAdd.hAdd (α := ↥(Lp G 1 μ)) 0 0
have pos : Eq (α := ↥(Lp G 1 μ)) 0 0
Tactic: rw [zero_add]
-- 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)
x y : G
hs : MeasurableSet s
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
have neg : condExpIndL1Fin (s := s) hm hs hμs (x + y) =
  HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := s) hm hs hμs y)
Tactic: simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμ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)
c : ℝ
x : G
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
have pos : ∀ (hs : MeasurableSet s), condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
Tactic: by_cases hs : MeasurableSet 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)
c : ℝ
x : G
pos : ∀ (hs : MeasurableSet s), condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
have neg : ∀ (hs : ¬MeasurableSet s), condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
Tactic: by_cases hs : MeasurableSet s