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

Goal state before:
pp: case refine_1
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ AEStronglyMeasurable (↑↑(condExpIndSMul hm hs hμs x)) μ

pp: case refine_2
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 → μ s_1 ≠ ∞ → ∫⁻ (x_1 : α) in s_1, ‖↑↑(condExpIndSMul hm hs hμs x) x_1‖ₑ ∂μ ≤ μ s * ↑‖x‖₊

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ AEStronglyMeasurable (↑↑(condExpIndSMul hm hs hμs x)) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 → μ s_1 ≠ ∞ → ∫⁻ (x_1 : α) in s_1, ‖↑↑(condExpIndSMul hm hs hμs x) x_1‖ₑ ∂μ ≤ μ s * ↑‖x‖₊

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 → μ s_1 ≠ ∞ → ∫⁻ (x_1 : α) in s_1, ‖↑↑(condExpIndSMul hm hs hμs x) x_1‖ₑ ∂μ ≤ μ s * ↑‖x‖₊
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_1
α : 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 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
⊢ ∀ (c : F') {s : Set α} (hs : MeasurableSet s) (hμs : (μ.trim hm) s < ∞),
    (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm ↑(simpleFunc.indicatorConst 1 hs ⋯ c)) =
      ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm ↑(simpleFunc.indicatorConst 1 hs ⋯ c))

pp: case refine_2
α : 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 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
⊢ ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 (μ.trim hm)) (hg : MemLp g 1 (μ.trim hm)),
    Disjoint (Function.support f) (Function.support g) →
      (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) =
          ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) →
        (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) =
            ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) →
          (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg)) =
            ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg))

pp: case refine_3
α : 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 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
⊢ IsClosed
    {f | (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm f) = ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm f)}

Tactic:
·

Goal state after:
case refine_1
α : 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 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
⊢ ∀ (c : F') {s : Set α} (hs : MeasurableSet s) (hμs : (μ.trim hm) s < ∞),
    (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm ↑(simpleFunc.indicatorConst 1 hs ⋯ c)) =
      ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm ↑(simpleFunc.indicatorConst 1 hs ⋯ c))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case inl
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ 0[f | ⊥] =ᵐ[0] fun x ↦ (Measure.real 0 Set.univ)⁻¹ • ∫ (x : α), f x ∂0

pp: case inr
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hμ : NeZero μ
⊢ μ[f | ⊥] =ᵐ[μ] fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
·

Goal state after:
case inl
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ 0[f | ⊥] =ᵐ[0] fun x ↦ (Measure.real 0 Set.univ)⁻¹ • ∫ (x : α), f x ∂0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case inr
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hμ : NeZero μ
⊢ μ[f | ⊥] =ᵐ[μ] fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
·

Goal state after:
case inr
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hμ : NeZero μ
⊢ μ[f | ⊥] =ᵐ[μ] fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      (μ.trim hm) s_1 < ∞ →
        IntegrableOn (AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h) s_1 (μ.trim hm)

pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      (μ.trim hm) s_1 < ∞ →
        0 ≤
          ∫ (x : α) in s_1,
            AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ.trim hm

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      (μ.trim hm) s_1 < ∞ →
        IntegrableOn (AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h) s_1 (μ.trim hm)
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_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal) (μ ⊗ₘ κ)

Tactic:
·

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      (μ.trim hm) s_1 < ∞ →
        0 ≤
          ∫ (x : α) in s_1,
            AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ.trim hm

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      (μ.trim hm) s_1 < ∞ →
        0 ≤
          ∫ (x : α) in s_1,
            AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ.trim hm
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : ¬m ≤ m₀
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]

pp: case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]

Tactic:
·

Goal state after:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : ¬m ≤ m₀
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_2
α : 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 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
⊢ ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 (μ.trim hm)) (hg : MemLp g 1 (μ.trim hm)),
    Disjoint (Function.support f) (Function.support g) →
      (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) =
          ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) →
        (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) =
            ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) →
          (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg)) =
            ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg))

pp: case refine_3
α : 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 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
⊢ IsClosed
    {f | (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm f) = ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm f)}

Tactic:
·

Goal state after:
case refine_2
α : 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 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
⊢ ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 (μ.trim hm)) (hg : MemLp g 1 (μ.trim hm)),
    Disjoint (Function.support f) (Function.support g) →
      (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) =
          ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) →
        (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) =
            ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) →
          (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg)) =
            ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]

pp: case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]

Tactic:
·

Goal state after:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]
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_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal) (μ ⊗ₘ κ)

Tactic:
·

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal) (μ ⊗ₘ κ)
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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ (∀ᵐ (x : 𝓧) ∂μ, Integrable (fun y ↦ log ((∂μ/∂ν) (x, y).1).toReal) (κ x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖log ((∂μ/∂ν) (x, y).1).toReal‖ ∂κ x) μ

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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ AEStronglyMeasurable (fun p ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)

Tactic:
·

Goal state after:
𝓧 : 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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ (∀ᵐ (x : 𝓧) ∂μ, Integrable (fun y ↦ log ((∂μ/∂ν) (x, y).1).toReal) (κ x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖log ((∂μ/∂ν) (x, y).1).toReal‖ ∂κ x) μ
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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ AEStronglyMeasurable (fun p ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)

Tactic:
·

Goal state after:
𝓧 : 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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ AEStronglyMeasurable (fun p ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : ¬m ≤ m0
⊢ μ[f | m] =ᵐ[μ.restrict s] 0

pp: case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
⊢ μ[f | m] =ᵐ[μ.restrict s] 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : ¬m ≤ m0
⊢ μ[f | m] =ᵐ[μ.restrict s] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᵐ[μ.restrict s] 0

pp: case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᵐ[μ.restrict s] 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᵐ[μ.restrict s] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : ¬m ≤ m₀
⊢ μ[c • f | m] =ᵐ[μ] c • μ[f | m]

pp: case pos
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : m ≤ m₀
⊢ μ[c • f | m] =ᵐ[μ] c • μ[f | m]

Tactic:
·

Goal state after:
case neg
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : ¬m ≤ m₀
⊢ μ[c • f | m] =ᵐ[μ] c • μ[f | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

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

pp: case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ μ[f | m] =ᵐ[μ.restrict s] 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : ¬Integrable f μ
⊢ μ[f | m] =ᵐ[μ.restrict s] 0