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

Goal state before:
pp: α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ Integrable (AEStronglyMeasurable.mk g hgm) ((μ.trim hm).restrict s)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ lpMeasSubgroupToLpTrim F p μ hm (f + g) = lpMeasSubgroupToLpTrim F p μ hm f + lpMeasSubgroupToLpTrim F p μ hm g

Tactic:
by
  ext1
  grw [Lp.coeFn_add]
  refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm ?_ ?_
  · exact (Lp.stronglyMeasurable _).add (Lp.stronglyMeasurable _)
  grw [lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq,
    ← Lp.coeFn_add]
  rfl

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν

Tactic:
rwa [integrable_klFun_rnDeriv_iff hμν]

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

Goal state before:
pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aestronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᵐ[μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᵐ[μ.restrict s] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_nnnorm_eq : (fun x ↦ ↑‖g x‖₊) =ᵐ[μ.restrict s] fun x ↦ ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊
⊢ IntegrableOn g s μ

Tactic:
IntegrableOn,

Goal state after:
case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aestronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᵐ[μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᵐ[μ.restrict s] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_nnnorm_eq : (fun x ↦ ↑‖g x‖₊) =ᵐ[μ.restrict s] fun x ↦ ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊
⊢ Integrable g (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
s : Set α
a✝ : MeasurableSet s
hμs : μ s < ∞
⊢ IntegrableOn (↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp)) s μ

Tactic:
IntegrableOn,

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
s : Set α
a✝ : MeasurableSet s
hμs : μ s < ∞
⊢ Integrable (↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp)) (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᵐ[μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᵐ[μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᵐ[μ] ∅
f' : α → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)

Tactic:
have hff' : f =ᵐ[μ] f' := by
    have : s_f \ s_g =ᵐ[μ] s_f := by
      rw [← Set.sdiff_inter_self_eq_sdiff, Set.inter_comm]
      refine ((ae_eq_refl s_f).diff h_inter_empty).trans ?_
      rw [Set.sdiff_empty]
    refine ((indicator_ae_eq_of_ae_eq_set this).trans ?_).symm
    rw [Set.indicator_support]
    exact hfm.ae_eq_mk.symm

Goal state after:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᵐ[μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᵐ[μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᵐ[μ] ∅
f' : α → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
hff' : f =ᵐ[μ] f'
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)

Tactic:
rcases finite_or_infinite ι with hι | hι

Goal state after:
case inl
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Finite ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)

case inr
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Infinite ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: case inr
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Infinite ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)

Tactic:
obtain ⟨e⟩ := nonempty_equiv_of_countable (α := ℕ) (β := ι)

Goal state after:
case inr
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Infinite ι
e : ℕ ≃ ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)
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)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ∞
i j : ℕ
hij : i ≤ j
⊢ (fun i ↦ S i ∩ s) i ⊆ (fun i ↦ S i ∩ s) j

Tactic:
x

Goal state after:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ∞
i j : ℕ
hij : i ≤ j
x : α
⊢ x ∈ (fun i ↦ S i ∩ s) i → x ∈ (fun i ↦ S i ∩ s) j
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 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
⊢ (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g) = ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)

Tactic:
refine @Lp.induction α F' m _ 1 (μ.trim hm) _ ENNReal.coe_ne_top (fun g : α →₁[μ.trim hm] F' =>
    condExpL1CLM F' hm μ ((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g : α →₁[μ] F') =
    ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)) ?_ ?_ ?_ g

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))

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))

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)}
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
⊢ μ.real (t ∩ s) • 1 = μ.real (t ∩ s)

Tactic:
rw [smul_eq_mul, mul_one]

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 κ
h_ac : μ ≪ ν
⊢ ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν

Tactic:
by
    rw [Measure.lintegral_compProd (by fun_prop)]
    simp

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

Goal state before:
pp: case pos
α : 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
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
⊢ ⇑T ∘ μ[f | m] =ᵐ[μ] μ[⇑T ∘ f | m]

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq hm ?_ (fun s ms hs => ?_) (fun s ms hs => ?_) ?_
      · exact T.integrable_comp hf_int
      · exact (T.integrable_comp integrable_condExp).integrableOn
      · calc
          ∫ x in s, (T ∘ μ[f | m]) x ∂μ = T (∫ x in s, μ[f | m] x ∂μ) :=
            T.integral_comp_comm integrable_condExp.restrict
          _ = T (∫ x in s, f x ∂μ) := congrArg T (setIntegral_condExp hm hf_int ms)
          _ = ∫ x in s, (T ∘ f) x ∂μ := (T.integral_comp_comm hf_int.restrict).symm
      · exact T.cont.comp_aestronglyMeasurable stronglyMeasurable_condExp.aestronglyMeasurable

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 μ)
hf : ¬Integrable f μ
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Tactic:
condExpL1_undef hf

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 μ)
hf : ¬Integrable f μ
⊢ AEStronglyMeasurable (↑↑0) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : 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)
⊢ μ[fun a ↦ ∑' (i : ι), f i a | m] =ᵐ[μ] fun a ↦ ∑' (i : ι), μ[f i | m] a

Tactic:
grw [condExp_ae_eq_condExpL1 hm]

Goal state after:
case pos
α : 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)
⊢ ↑↑(condExpL1 hm μ fun a ↦ ∑' (i : ι), f i a) =ᵐ[μ] fun a ↦ ∑' (i : ι), μ[f i | m] a
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
hm : ¬mΩ ≤ mΩ₀
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f | mΩ] x < ∞

Tactic:
simp [condLExp_of_not_le hm]

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X =ᵐ[P] Y
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X | mΩ] =ᵐ[P] P⁻[Y | mΩ]

Tactic:
simp [condLExp_of_not_le hm]

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[0 | mΩ] = 0

Tactic:
simp [condLExp_of_not_le hm]

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X | mΩ] ≤ᵐ[P] P⁻[Y | mΩ]

Tactic:
simp_rw [condLExp_of_not_le hm, Filter.EventuallyLE.rfl]

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[c • X | mΩ] =ᵐ[P] c • P⁻[X | mΩ]

Tactic:
simp [condLExp_of_not_le hm]

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

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst✝ : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (Measure.map id ν)
h :
  (fun a ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) (id a)).toReal) =ᵐ[ν.trim ⋯]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap id m]
⊢ (fun x ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) x).toReal) =ᵐ[Measure.map id ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]

Tactic:
simp_rw [MeasurableSpace.comap_id, id_def, trim_eq_map] at h

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst✝ : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (Measure.map id ν)
h :
  (fun a ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) a).toReal) =ᵐ[Measure.map id ν]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | m]
⊢ (fun x ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) x).toReal) =ᵐ[Measure.map id ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[c • X | mΩ] =ᵐ[P] c • P⁻[X | mΩ]

Tactic:
simp [condLExp_of_not_le hm]

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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
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
φY : ↥Y → ℝ := φ ∘ ⇑Y.subtypeL
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
hfY_int : Integrable fY μ
lem2 : μ[f | m] =ᵐ[μ] ⇑Y.subtypeL ∘ μ[fY | m]
lem3 : φ ∘ f =ᵐ[μ] φY ∘ fY
⊢ φY ∘ μ[fY | m] ≤ᵐ[μ] μ[φY ∘ fY | m]

Tactic:
refine (hφ_cvx.comp_linearMap Y.subtype).map_condExp_le_of_hereditarilyLindelofSpace
        (s := Y.subtypeL ⁻¹' s) hm ?_ ?_ ?_ hfY_int (Integrable.congr hφ_int lem3)
      · exact hφ_cont.comp (by fun_prop) fun x => by
          #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
          (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
          goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem
          in the new canonicalizer; a minimization would help. The original proof was: `grind` -/
          simp
      · filter_upwards [lem0, hf] with a ha hb
        simp_all [fY]
      · exact hs.preimage Y.subtypeL.continuous

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x ↦ klFun ((∂μ/∂ν) x).toReal) ν

Tactic:
rwa [integrable_klFun_rnDeriv_iff hμν]

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hf : StronglyMeasurable klFun
hf_cont : ContinuousWithinAt klFun (Ici 0) 0
⊢ Integrable (fun x ↦ klFun ((∂μ/∂ν) x).toReal) ν

Tactic:
rwa [integrable_klFun_rnDeriv_iff hμν]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : ¬SigmaFinite (μ.trim hm)
⊢ (fun x ↦ ‖μ[f | m] x‖) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ | m]

Tactic:
simp [condExp_of_not_sigmaFinite hm hμm]

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : ¬SigmaFinite (μ.trim hm)
⊢ (fun x ↦ 0) ≤ᵐ[μ] 0
Module: Mathlib.Lean.Thunk

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
x : a = b
⊢ a.get = b.get

Tactic:
x

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
x : a = b
⊢ b.get = b.get