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

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᵐ[μ] s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m])

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ sᶜ.indicator μ[sᶜ.indicator f | m] =ᵐ[μ] μ[sᶜ.indicator f | m]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + s.indicator μ[sᶜ.indicator f | m] =ᵐ[μ]
    s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) =ᵐ[μ]
    s.indicator μ[s.indicator f | m]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
⊢ ⇑T ∘ μ[f | m] =ᵐ[μ] μ[⇑T ∘ f | m]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsFiniteMeasure μ
hm : m ≤ m₀
hf_int : Integrable f μ
T : E →L[ℝ] F
a : F
⊢ (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[⇑T ∘ f | m] + μ[fun y ↦ a | m]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
⊢ (condExpL1CLM F' hm μ) ↑f = ↑f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] =ᵐ[μ] μ[s.indicator f | m]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
⊢ μ[s.indicator f | m] =ᵐ[μ] s.indicator μ[f | m]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsFiniteMeasure μ
hm : m ≤ m₀
hf_int : Integrable f μ
T : E →L[ℝ] F
a : F
⊢ (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[fun y ↦ T (f y) + a | m]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
⊢ SigmaFinite ((μ.restrict s).trim hm)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case neg
α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : ¬CompleteSpace ↥(Lp F' 1 μ)
⊢ AEStronglyMeasurable (↑0) μ

Tactic:
apply stronglyMeasurable_zero.aestronglyMeasurable.congr

Goal state after:
case neg
α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : ¬CompleteSpace ↥(Lp F' 1 μ)
⊢ 0 =ᵐ[μ] ↑0
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
this :
  ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    ∫ (a : 𝓧), llr μ ν a ∂μ + ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ
⊢ ENNReal.ofReal (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + (ν univ).toReal - (μ univ).toReal) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal + ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
⊢ ↑↑↑((condExpL2 E 𝕜 hm) (toLp f hf2)) =ᵐ[μ] μ[f | m]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
m m₀ : MeasurableSpace α
μ : Measure α
R : Type u_5
inst✝³ : NormedRing R
inst✝² : NormedSpace ℝ R
inst✝¹ : CompleteSpace R
n : ℕ
inst✝ : n.AtLeastTwo
f : α → R
⊢ μ[OfNat.ofNat n * f | m] =ᵐ[μ] OfNat.ofNat n * μ[f | m]

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case pos
α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : f =ᵐ[μ] 0
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Tactic:
apply stronglyMeasurable_zero.aestronglyMeasurable.congr

Goal state after:
case pos
α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : f =ᵐ[μ] 0
⊢ 0 =ᵐ[μ] ↑↑(condExpL1 hm μ f)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝¹ : IsFiniteMeasure μ
inst✝ : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᵐ[μ] 0
⊢ Nontrivial ↥(Lp F' 1 μ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᵐ[μ] 0
⊢ CompleteSpace F'

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
h_int_restrict : Integrable (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)
⊢ Integrable (s.indicator (t.indicator (μ.restrict s)[f | m])) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
inst✝ : CompleteSpace F'
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑(condExpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
c : 𝕜
f : α → F'
⊢ condExpL1 hm μ (c • f) = c • condExpL1 hm μ f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
⊢ ∀ᵐ (a : α) ∂μ, f a ∈ Y

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in t, s.indicator (μ.restrict s)[f | m] x ∂μ = ∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
f : α → F'
inst✝ : CompleteSpace F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ↑↑(condExpL1 hm μ f) =ᵐ[μ] f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ι : Type u_5
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
A : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), μ[f i | m] a = ↑↑(condExpL1 hm μ (f i)) a
i : ι
⊢ 0 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝⁶ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : ClosedIciTopology E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsOrderedModule ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
⊢ ↑↑(condExpL1 hm μ f) ≤ᵐ[μ] ↑↑(condExpL1 hm μ g)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ι : Type u_5
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
A : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), μ[f i | m] a = ↑↑(condExpL1 hm μ (f i)) a
i : ι
⊢ ↑(NNReal.mk 1 ⋯) * ∫⁻ (x : α), ‖f i x‖ₑ ∂μ = ∫⁻ (a : α), ‖f i a‖ₑ ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ι : Type u_5
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
A : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), μ[f i | m] a = ↑↑(condExpL1 hm μ (f i)) a
⊢ ∑' (n : ι), ‖condExpL1 hm μ (f n)‖ₑ ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in t, f x ∂μ.restrict s = ∫ (x : α) in t, s.indicator f x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
⊢ f =ᵐ[μ] fX

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm_not : ¬mΩ ≤ mΩ₀
⊢ P⁻[X | mΩ] = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hμm_not : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X | mΩ] = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
hX : Measurable X
⊢ P⁻[X | mΩ] = X

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
hX : ¬Measurable X
⊢ P⁻[X | mΩ] = ∂(P.withDensity X).trim hm/∂P.trim hm

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
⊢ (μ.restrict s)[f | m] =ᵐ[μ.restrict s] μ[f | m]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
⊢ Measurable P⁻[X | mΩ]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
⊢ ∀ᵐ (a : α) ∂μ, fY a ∈ ⇑Y.subtypeL ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
⊢ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
lem2 : ∀ᵐ (a : α) ∂μ, fY a ∈ ⇑Y.subtypeL ⁻¹' s
⊢ ∀ᵐ (a : α) ∂μ, ‖fY a‖ ≤ ‖fX a‖

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
⊢ Measurable (s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ι : Type u_5
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
⊢ μ[fun a ↦ ∑' (i : ι), f i a | m] =ᵐ[μ] fun a ↦ ∑' (i : ι), μ[f i | m] a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, P⁻[X | mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, P⁻[X | mΩ] ω ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
⊢ ∫⁻ (ω : Ω), P⁻[X | mΩ] ω ∂P = ∫⁻ (ω : Ω), X ω ∂P

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : ¬Integrable f μ
⊢ s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[f | m₂]

Tactic:
simp_rw [condExp_of_not_integrable hf_int]; rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ AEMeasurable P⁻[f | mΩ] P

Tactic:
by

Goal state after: