awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
⊢ (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] E) : α → E)

Tactic:
exact (coeFn_zero E 1 μ).trans_le (condExpIndSMul_nonneg hs hμs x hx)

Premises used: Filter.EventuallyEq.trans_le, MeasureTheory.condExpIndSMul_nonneg, MeasureTheory.Lp.coeFn_zero, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 μ))

Tactic:
L1.setToL1_smul (dominatedFinMeasAdditive_condExpInd F' hm μ) ?_ c f

Premises used: Set.Mem, MeasureTheory.dominatedFinMeasAdditive_condExpInd, MeasureTheory.L1.setToL1_smul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 μ)
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 μ))
⊢ (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 μ))

Tactic:
refine L1.setToL1_smul (dominatedFinMeasAdditive_condExpInd F' hm μ) ?_ c f

Premises used: MeasureTheory.dominatedFinMeasAdditive_condExpInd, MeasureTheory.L1.setToL1_smul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 μ)
⊢ ∀ (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:
fun c s x => condExpInd_smul' c x

Premises used: MeasureTheory.condExpInd_smul'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 μ)
⊢ ∀ (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:
exact fun c s x => condExpInd_smul' c x

Premises used: MeasureTheory.condExpInd_smul'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 μ)) (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:
L1.setToL1_indicatorConstLp (dominatedFinMeasAdditive_condExpInd F' hm μ) hs hμs x

Premises used: MeasureTheory.L1.setToL1_indicatorConstLp, Set.Mem, MeasureTheory.dominatedFinMeasAdditive_condExpInd
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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'
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 μ))
⊢ 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 μ))

Tactic:
rw [Lp.simpleFunc.coe_indicatorConst]

Premises used: MeasureTheory.Lp.simpleFunc.coe_indicatorConst
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 μ)) (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:
condExpL1CLM_indicatorConstLp hs hμs x

Premises used: MeasureTheory.condExpL1CLM_indicatorConstLp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 μ)) (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:
exact condExpL1CLM_indicatorConstLp hs hμs x

Premises used: MeasureTheory.condExpL1CLM_indicatorConstLp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 ∂μ)

Tactic:
@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

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.condExpL1CLM, MeasureTheory.Measure.restrict, isClosed_eq, MeasureTheory.integral, MeasureTheory.Lp.induction, Subtype.val, Eq, DFunLike.coe, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 ∂μ
refine_4 :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp F' 1 μ)) ↦
    ∫ (x : α) in s, (↑(↑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 ∂μ)

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

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.condExpL1CLM, MeasureTheory.Measure.restrict, isClosed_eq, MeasureTheory.integral, MeasureTheory.Lp.induction, Subtype.val, Eq, DFunLike.coe, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
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 ⋯ x) : ↥(Lp F' 1 μ)) : α →ₘ[μ] F') : α → F') x_1 ∂μ)
⊢ 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 ∂μ)

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

Premises used: MeasureTheory.condExpL1CLM_indicatorConst, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
refine_1 :
  ∫ (x_1 : α) in s, (↑(↑((condExpInd F' hm μ t : (a : F') → ↥(Lp F' 1 μ)) x) : α →ₘ[μ] F') : α → F') x_1 ∂μ =
    μ.real (t ∩ s) • x
⊢ 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 ∂μ)

Tactic:
rw [Lp.simpleFunc.coe_indicatorConst, setIntegral_indicatorConstLp (hm _ hs)]

Premises used: MeasureTheory.setIntegral_indicatorConstLp, MeasureTheory.Lp.simpleFunc.coe_indicatorConst
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
⊢ ∫ (x_1 : α) in s, (↑(↑((condExpInd F' hm μ t : (a : F') → ↥(Lp F' 1 μ)) x) : α →ₘ[μ] F') : α → F') x_1 ∂μ =
    μ.real (t ∩ s) • x

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

Premises used: MeasureTheory.setIntegral_condExpInd, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
⊢ ∫ (x_1 : α) in s, (↑(↑((condExpInd F' hm μ t : (a : F') → ↥(Lp F' 1 μ)) x) : α →ₘ[μ] F') : α → F') x_1 ∂μ =
    μ.real (t ∩ s) • x

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

Premises used: MeasureTheory.setIntegral_condExpInd, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 μ
refine_2 :
  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_Lp) →
      (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_Lp) →
        (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_Lp + MemLp.toLp g hg_Lp)
⊢ 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_Lp) →
      (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_Lp) →
        (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_Lp + MemLp.toLp g hg_Lp)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 ∂μ)
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 ∂μ)
⊢ 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 ∂μ)

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

Premises used: MeasureTheory.condExpL1CLM, ContinuousLinearMap.map_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 ∂μ)
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 ∂μ)
⊢ 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:
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)]

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.setIntegral_congr_ae, MeasureTheory.condExpL1CLM, Filter.Eventually.mono, MeasureTheory.MemLp.toLp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 ∂μ)
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) : α →ₘ[μ] F') : α → F') + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F')) x ∂μ)
⊢ 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 (hf_Lp.toLp f) (hg_Lp.toLp g)).mono fun x hx _ => hx)]

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.setIntegral_congr_ae, Filter.Eventually.mono, MeasureTheory.MemLp.toLp