awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hμst : μ (s ∪ t) ≠ ∞ :=
    ((measure_union_le s t).trans_lt (lt_top_iff_ne_top.mpr (ENNReal.add_ne_top.mpr ⟨hμs, hμt⟩))).ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  condExpIndL1Fin (s := s ∪ t) hm ⋯ hμst x =
    HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := t) hm ht hμt x)
⊢ condExpIndL1 hm μ (s ∪ t) x = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ t x)

Tactic:
rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs x,
    condExpIndL1_of_measurableSet_of_measure_ne_top ht hμt x,
    condExpIndL1_of_measurableSet_of_measure_ne_top (hs.union ht) hμst x]

Premises used: MeasurableSet.union, MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1Fin (s := s ∪ t) hm ⋯ hμst x =
    HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := t) hm ht hμt x)

Tactic:
condExpIndL1Fin_disjoint_union hs ht hμs hμt hst x

Premises used: MeasureTheory.condExpIndL1Fin_disjoint_union
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1Fin (s := s ∪ t) hm ⋯ hμst x =
    HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := t) hm ht hμt x)

Tactic:
exact condExpIndL1Fin_disjoint_union hs ht hμs hμt hst x

Premises used: MeasureTheory.condExpIndL1Fin_disjoint_union
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
grw :
  (↑(↑((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)

Tactic:
grw [← condExpIndL1Fin_ae_eq_condExpIndSMul]

Premises used: MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
⊢ (↑(↑((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)

Tactic:
simp [condExpInd, condExpIndL1, hs, hμs]

Premises used: MeasureTheory.condExpInd, MeasureTheory.condExpIndL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
⊢ AEStronglyMeasurable.{u_1, u_4} (β := G) (↑(↑((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G) μ

Tactic:
(aestronglyMeasurable_condExpIndSMul hm hs hμs x).congr
    (condExpInd_ae_eq_condExpIndSMul hm hs hμs x).symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.condExpInd_ae_eq_condExpIndSMul, MeasureTheory.aestronglyMeasurable_condExpIndSMul, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
h :
  ∀ (x : G),
    EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑((condExpInd G hm μ ∅ : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
      (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
⊢ Eq (α := G →L[ℝ] ↥(Lp G 1 μ)) (condExpInd G hm μ ∅) 0

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
x : G
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
x : G
h :
  (↑(↑(condExpIndSMul (s := ∅) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
h₁ :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑0 : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
h₂ : EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑0 : α →ₘ[μ] G) : α → G) (↑(↑0 : α →ₘ[μ] G) : α → G)
h₃ : EventuallyEq.{u_1, u_4} (β := G) (ae μ) 0 (↑(↑0 : α →ₘ[μ] G) : α → G)
h₄ h₅ : EventuallyEq.{u_1, u_4} (β := G) (ae μ) 0 0
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑((condExpInd G hm μ ∅ : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)

Tactic:
grw [condExpInd_ae_eq_condExpIndSMul hm MeasurableSet.empty (by simp), condExpIndSMul_empty,
    zero_apply, Lp.coeFn_zero, Lp.coeFn_zero]

Premises used: MeasureTheory.condExpInd_ae_eq_condExpIndSMul, MeasurableSet.empty, MeasureTheory.condExpIndSMul_empty, MeasureTheory.Lp.coeFn_zero, ContinuousLinearMap.zero_apply
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : NormedSpace ℝ F
inst_5 : SMulCommClass ℝ 𝕜 F
c : 𝕜
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:
condExpIndL1_smul' c x

Premises used: MeasureTheory.condExpIndL1_smul', dite, MeasureTheory.condExpIndL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 : G
⊢ norm (E := ↥(Lp G 1 μ)) ((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) x : ↥(Lp G 1 μ)) ≤ μ.real s * ‖x‖

Tactic:
norm_condExpIndL1_le x

Premises used: MeasureTheory.norm_condExpIndL1_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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)
⊢ norm (E := G →L[ℝ] ↥(Lp G 1 μ)) (condExpInd G hm μ s) ≤ μ.real s

Tactic:
ContinuousLinearMap.opNorm_le_bound _ ENNReal.toReal_nonneg norm_condExpInd_apply_le

Premises used: ENNReal.toReal_nonneg, ContinuousLinearMap.opNorm_le_bound, MeasureTheory.norm_condExpInd_apply_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
⊢ (condExpInd G hm μ (s ∪ t) : (a : G) → ↥(Lp G 1 μ)) x =
    HAdd.hAdd (α := ↥(Lp G 1 μ)) (β := ↥(Lp G 1 μ)) ((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) x : ↥(Lp G 1 μ))
      ((condExpInd G hm μ t : (a : G) → ↥(Lp G 1 μ)) x : ↥(Lp G 1 μ))

Tactic:
condExpIndL1_disjoint_union hs ht hμs hμt hst x

Premises used: dite, MeasureTheory.condExpIndL1_disjoint_union, MeasureTheory.condExpIndL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
h :
  ∀ (x : G),
    Eq (α := ↥(Lp G 1 μ)) ((condExpInd G hm μ (s ∪ t) : (a : G) → ↥(Lp G 1 μ)) x : ↥(Lp G 1 μ))
      ((HAdd.hAdd (α := G →L[ℝ] ↥(Lp G 1 μ)) (condExpInd G hm μ s) (condExpInd G hm μ t) : (a : G) → ↥(Lp G 1 μ)) x :
        ↥(Lp G 1 μ))
⊢ condExpInd G hm μ (s ∪ t) = HAdd.hAdd (α := G →L[ℝ] ↥(Lp G 1 μ)) (condExpInd G hm μ s) (condExpInd G hm μ t)

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
⊢ (condExpInd G hm μ (s ∪ t) : (a : G) → ↥(Lp G 1 μ)) x =
    HAdd.hAdd (α := (a : G) → ↥(Lp G 1 μ)) (β := (a : G) → ↥(Lp G 1 μ)) (⇑(condExpInd G hm μ s) : (a : G) → ↥(Lp G 1 μ))
      (⇑(condExpInd G hm μ t) : (a : G) → ↥(Lp G 1 μ)) x

Tactic:
condExpInd_disjoint_union_apply hs ht hμs hμt hst x

Premises used: Set.Mem, MeasureTheory.condExpInd_disjoint_union_apply
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
⊢ (condExpInd G hm μ (s ∪ t) : (a : G) → ↥(Lp G 1 μ)) x =
    HAdd.hAdd (α := (a : G) → ↥(Lp G 1 μ)) (β := (a : G) → ↥(Lp G 1 μ)) (⇑(condExpInd G hm μ s) : (a : G) → ↥(Lp G 1 μ))
      (⇑(condExpInd G hm μ t) : (a : G) → ↥(Lp G 1 μ)) x

Tactic:
exact condExpInd_disjoint_union_apply hs ht hμs hμt hst x

Premises used: MeasureTheory.condExpInd_disjoint_union_apply
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
μ : Measure α
inst_2 : SigmaFinite (μ.trim hm)
⊢ DominatedFinMeasAdditive (β := G →L[ℝ] ↥(Lp G 1 μ)) μ (condExpInd G hm μ) 1

Tactic:
⟨fun _ _ => condExpInd_disjoint_union, fun _ _ _ => norm_condExpInd_le.trans (one_mul _).symm.le⟩

Premises used: MeasureTheory.Measure.real, MeasureTheory.condExpInd_disjoint_union, Eq.le, MeasureTheory.DominatedFinMeasAdditive, And.intro, MeasureTheory.norm_condExpInd_le, LE.le.trans, Eq.symm, one_mul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
G' : Type u_5
inst : NormedAddCommGroup G'
inst_1 : NormedSpace ℝ G'
inst_2 : CompleteSpace G'
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
inst_3 : 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∞)
x : G'
⊢ ∫ (a : α) in s, (↑(↑((condExpInd G' hm μ t : (a : G') → ↥(Lp G' 1 μ)) x) : α →ₘ[μ] G') : α → G') a ∂μ =
    μ.real (t ∩ s) • x

Tactic:
calc
    ∫ a in s, condExpInd G' hm μ t x a ∂μ = ∫ a in s, condExpIndSMul hm ht hμt x a ∂μ :=
      setIntegral_congr_ae (hm s hs)
        ((condExpInd_ae_eq_condExpIndSMul hm ht hμt x).mono fun _ hx _ => hx)
    _ = μ.real (t ∩ s) • x := setIntegral_condExpIndSMul hs ht hμs hμt x

Premises used: MeasureTheory.condExpInd_ae_eq_condExpIndSMul, Trans.trans, MeasureTheory.setIntegral_congr_ae, MeasureTheory.setIntegral_condExpIndSMul, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
h :
  (↑(↑((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) c) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) 1 ⋯ hμs c) : α →ₘ[μ] G) : α → G)
⊢ Eq (α := ↥(Lp G 1 μ)) ((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) c : ↥(Lp G 1 μ))
    (indicatorConstLp (s := s) 1 ⋯ hμs c : ↥(Lp G 1 μ))

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
h :
  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)
⊢ (↑(↑((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) c) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) 1 ⋯ hμs c) : α →ₘ[μ] G) : α → G)

Tactic:
grw [indicatorConstLp_coeFn, condExpInd_ae_eq_condExpIndSMul hm (hm s hs) hμs,
    condExpIndSMul_ae_eq_smul]

Premises used: MeasureTheory.condExpInd_ae_eq_condExpIndSMul, MeasureTheory.condExpIndSMul_ae_eq_smul, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
h :
  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)
⊢ 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)

Tactic:
rw [condExpL2_indicator_of_measurable hm hs hμs (1 : ℝ)]

Premises used: MeasureTheory.condExpL2_indicator_of_measurable, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
h :
  ∀ (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
⊢ 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)

Tactic:
filter_upwards [@indicatorConstLp_coeFn α _ _ 2 μ _ s (hm s hs) hμs (1 : ℝ)] with x hx

Premises used: MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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)
h : HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) x) c = s.indicator (fun (x : α) ↦ c) x
⊢ HSMul.hSMul (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 ⋯ hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) c =
    s.indicator (fun (x : α) ↦ c) x

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
neg : ∀ (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

Tactic:
by_cases hx_mem : x ∈ s
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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)
hx_mem : x ∈ s
⊢ HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) x) c = s.indicator (fun (x : α) ↦ c) x

Tactic:
simp [hx_mem]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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)
hx_mem : x ∉ s
⊢ HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) x) c = s.indicator (fun (x : α) ↦ c) x

Tactic:
simp [hx_mem]
-- 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
rw :
  EventuallyLE.{u_1, u_7} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E)
    (↑(↑((condExpInd E hm μ s : (a : E) → ↥(Lp E 1 μ)) x) : α →ₘ[μ] E) : α → E)
⊢ LE.le (α := ↥(Lp E 1 μ)) (0 : ↥(Lp E 1 μ)) ((condExpInd E hm μ s : (a : E) → ↥(Lp E 1 μ)) x : ↥(Lp E 1 μ))

Tactic:
rw [← coeFn_le]

Premises used: MeasureTheory.Lp.coeFn_le
-- 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
⊢ EventuallyLE.{u_1, u_7} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E)
    (↑(↑((condExpInd E hm μ s : (a : E) → ↥(Lp E 1 μ)) x) : α →ₘ[μ] E) : α → E)

Tactic:
EventuallyLE.trans_eq ?_ (condExpInd_ae_eq_condExpIndSMul hm hs hμs x).symm

Premises used: MeasureTheory.condExpInd_ae_eq_condExpIndSMul, Filter.EventuallyLE.trans_eq, Filter.EventuallyEq.symm
-- 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
refine : (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] E) : α → E)
⊢ EventuallyLE.{u_1, u_7} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E)
    (↑(↑((condExpInd E hm μ s : (a : E) → ↥(Lp E 1 μ)) x) : α →ₘ[μ] E) : α → E)

Tactic:
refine EventuallyLE.trans_eq ?_ (condExpInd_ae_eq_condExpIndSMul hm hs hμs x).symm

Premises used: MeasureTheory.condExpInd_ae_eq_condExpIndSMul, Filter.EventuallyLE.trans_eq, Filter.EventuallyEq.symm
-- 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:
(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