awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ s φ
hφ_cont : UpperSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
a : α
h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a
ha : μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a
⊢ μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a

Tactic:
simp_all [Pi.neg_comp]

Premises used: Pi.neg_comp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ univ φ
hφ_cont : LowerSemicontinuous φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) univ (f a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hφ_cont : UpperSemicontinuous φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
h :
  ∀ (a : α) (h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a) (ha : μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a),
    μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a
⊢ μ[φ ∘ f | m] ≤ᶠ[ae μ] φ ∘ μ[f | m]

Tactic:
filter_upwards [hφ_cvx.neg.map_condExp_le_univ hm hφ_cont.neg hf_int hφ_int.neg,
    condExp_neg (φ ∘ f) m] with a h ha

Premises used: ConvexOn.map_condExp_le_univ, MeasureTheory.Integrable.neg, MeasureTheory.condExp_neg, Function.comp, ConcaveOn.neg, UpperSemicontinuous.neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hφ_cont : UpperSemicontinuous φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
a : α
h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a
ha : μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a
⊢ μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a

Tactic:
simp_all [Pi.neg_comp]

Premises used: Pi.neg_comp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
pos : ∀ (hm : ¬m ≤ mα), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
neg : ∀ (hm : m ≤ mα), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]

Tactic:
by_cases! hm : ¬ m ≤ mα
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : ¬m ≤ mα
pos : (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ 0) 0
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]

Tactic:
simp [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : ¬m ≤ mα
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ 0) 0

Tactic:
aesop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
pos :
  ∀ (hμm : ¬SigmaFinite (μ.trim hm)),
    (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
neg :
  ∀ (hμm : SigmaFinite (μ.trim hm)),
    (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]

Tactic:
by_cases! hμm : ¬ SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
hμm : ¬SigmaFinite (μ.trim hm)
pos : (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ 0) 0
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]

Tactic:
simp [condExp_of_not_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
hμm : ¬SigmaFinite (μ.trim hm)
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ 0) 0

Tactic:
aesop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
pos : ∀ (hf_int : ¬Integrable f μ), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
neg : ∀ (hf_int : Integrable f μ), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]

Tactic:
by_cases! hf_int : ¬ Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
pos : (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ 0) μ[fun (x : α) ↦ ‖f x‖ | m]
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]

Tactic:
simp only [condExp_of_not_integrable hf_int, Pi.zero_apply, norm_zero]

Premises used: norm_zero, Pi.zero_apply, MeasureTheory.condExp_of_not_integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
pos : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖f x‖
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ 0) μ[fun (x : α) ↦ ‖f x‖ | m]

Tactic:
apply condExp_nonneg

Premises used: MeasureTheory.condExp_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
pos : ∀ (a : α), 0 a ≤ ‖f a‖
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖f x‖

Tactic:
filter_upwards with a
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
a : α
⊢ 0 a ≤ ‖f a‖

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]

Tactic:
convexOn_univ_norm.map_condExp_le_univ hm continuous_norm.lowerSemicontinuous hf_int
    hf_int.norm

Premises used: ConvexOn.map_condExp_le_univ, convexOn_univ_norm, Continuous.lowerSemicontinuous, MeasureTheory.Integrable.norm, continuous_norm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]

Tactic:
exact convexOn_univ_norm.map_condExp_le_univ hm continuous_norm.lowerSemicontinuous hf_int
    hf_int.norm

Premises used: ConvexOn.map_condExp_le_univ, convexOn_univ_norm, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
inst_3 : FiniteDimensional ℝ E
hm : m ≤ mα
inst_4 : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ univ φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]

Tactic:
hφ_cvx.map_condExp_le_univ hm
    (continuousOn_univ.1 (hφ_cvx.continuousOn isOpen_univ)).lowerSemicontinuous hf_int hφ_int

Premises used: ConvexOn.map_condExp_le_univ, isOpen_univ, Iff.mp, Continuous.lowerSemicontinuous, continuousOn_univ, ConvexOn.continuousOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
inst_3 : FiniteDimensional ℝ E
hm : m ≤ mα
inst_4 : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
h :
  ∀ (a : α) (h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a) (ha : μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a),
    μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a
⊢ μ[φ ∘ f | m] ≤ᶠ[ae μ] φ ∘ μ[f | m]

Tactic:
filter_upwards [hφ_cvx.neg.map_condExp_le_of_finiteDimensional hm hf_int hφ_int.neg,
    condExp_neg (φ ∘ f) m] with a h ha

Premises used: MeasureTheory.Integrable.neg, ConvexOn.map_condExp_le_of_finiteDimensional, MeasureTheory.condExp_neg, Function.comp, ConcaveOn.neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
inst_3 : FiniteDimensional ℝ E
hm : m ≤ mα
inst_4 : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
a : α
h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a
ha : μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a
⊢ μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a

Tactic:
simp_all [Pi.neg_comp]

Premises used: Pi.neg_comp
-- 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
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)

Tactic:
(integrable_condExpIndSMul hm hs hμs x).coeFn_toL1

Premises used: MeasureTheory.Integrable.coeFn_toL1, MeasureTheory.integrable_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
rw : Integrable (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) μ
⊢ MemLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) 1 μ

Tactic:
rw [memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- 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
⊢ Integrable (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) μ

Tactic:
apply integrable_condExpIndSMul

Premises used: MeasureTheory.integrable_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 y : G
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := s) hm hs hμs y)) :
          α →ₘ[μ] G) :
      α → G)
⊢ 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:
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∞)
x y : G
h :
  (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯ +
              MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) :
          α →ₘ[μ] G) :
      α → G)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := s) hm hs hμs y)) :
          α →ₘ[μ] G) :
      α → G)

Tactic:
unfold condExpIndL1Fin Integrable.toL1

Premises used: MeasureTheory.condExpIndL1Fin, MeasureTheory.Integrable.toL1
-- 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 y : G
h :
  (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₂ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₃ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G)
h₄ :
  (↑(↑(HAdd.hAdd (α := ↥(Lp G 2 μ)) (condExpIndSMul (s := s) hm hs hμs x) (condExpIndSMul (s := s) hm hs hμs y)) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G)
h₅ h₆ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯ +
              MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) :
          α →ₘ[μ] G) :
      α → G)

Tactic:
grw [Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp, MemLp.coeFn_toLp, condExpIndSMul_add,
    Lp.coeFn_add]

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.condExpIndSMul_add, MeasureTheory.MemLp.coeFn_toLp
-- 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 : ℝ
x : G
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G)
⊢ condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)

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 : ℝ
x : G
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
h₂ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
h₃ :
  (↑(↑(HSMul.hSMul (β := ↥(Lp G 2 μ)) c (condExpIndSMul (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
h₄ h₅ :
  c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G)

Tactic:
grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]

Premises used: MeasureTheory.condExpIndSMul_smul, MeasureTheory.Lp.coeFn_smul, MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F)
⊢ condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)

Tactic:
ext1
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
h₂ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
h₃ :
  (↑(↑(HSMul.hSMul (β := ↥(Lp F 2 μ)) c (condExpIndSMul (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
h₄ h₅ :
  c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F)

Tactic:
grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]

Premises used: MeasureTheory.condExpIndSMul_smul, MeasureTheory.Lp.coeFn_smul, 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
rw :
  ∫⁻ (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‖)
rw₁ : Integrable (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) μ
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) ≤ μ.real s * ‖x‖

Tactic:
rw [L1.norm_eq_integral_norm, ← ENNReal.toReal_ofReal (norm_nonneg x), measureReal_def,
    ← ENNReal.toReal_mul,
    ← ENNReal.ofReal_le_iff_le_toReal (ENNReal.mul_ne_top hμs ENNReal.ofReal_ne_top),
    ofReal_integral_norm_eq_lintegral_enorm]

Premises used: ENNReal.ofReal_le_iff_le_toReal, ENNReal.mul_ne_top, ENNReal.toReal_ofReal, MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm, ENNReal.toReal_mul, MeasureTheory.measureReal_def, ENNReal.ofReal_ne_top, norm_nonneg, MeasureTheory.L1.norm_eq_integral_norm
-- 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
rw : MemLp (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) 1 μ
⊢ Integrable (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) μ

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable