mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (Measure.map f (Kernel.id a✝¹)) s✝ = ((deterministic f hf) a✝¹) s✝

Tactic:
Kernel.deterministic_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (Measure.map f (Kernel.id a✝¹)) s✝ = (Measure.dirac (f a✝¹)) s✝
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (Kernel.id (f a✝¹)) s✝ = ((deterministic f hf) a✝¹) s✝

Tactic:
Kernel.deterministic_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (Kernel.id (f a✝¹)) s✝ = (Measure.dirac (f a✝¹)) s✝
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set (γ × β)
hs : MeasurableSet s
⊢ (κ.swapRight a) s = (κ a) {p | p.swap ∈ s}

Tactic:
by
  rw [swapRight_apply, Measure.map_apply measurable_swap hs]; rfl

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel κ.snd

Tactic:
Kernel.snd_eq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.snd)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel κ.snd

Tactic:
Kernel.snd_eq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.snd)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel κ.snd

Tactic:
Kernel.snd_eq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.snd)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel κ.snd

Tactic:
Kernel.snd_eq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.snd)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
⊢ ∫⁻ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac ((a, b), b).2 ∂η ((a, b), b).1 =
    (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
have h_int x : ∫⁻ y, swap γ β (x, y) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x := by
    rw [lintegral_dirac']
    · simp [swap_apply' _ hs, Set.indicator_apply]
    · simpa [swap_apply' _ hs, Prod.swap_prod_mk] using!
        measurable_const.indicator (measurable_prodMk_right hs)

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
h_int : ∀ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x
⊢ ∫⁻ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac ((a, b), b).2 ∂η ((a, b), b).1 =
    (η (a, b)) (Prod.mk b ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y ↦ f (x, y)) (η (a, x))) ∧
      HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)

Tactic:
by
  rw [hasFiniteIntegral_congr h1f.ae_eq_mk,
    hasFiniteIntegral_compProd_iff h1f.stronglyMeasurable_mk]
  apply and_congr
  · apply eventually_congr
    filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with x hx using
      hasFiniteIntegral_congr hx
  · apply hasFiniteIntegral_congr
    filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with _ hx using
      integral_congr_ae (EventuallyEq.fun_comp hx _)

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ ↥(Lp E 1 ((κ ⊗ₖ η) a)) → ℝ≥0∞

Tactic:
exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖ₑ ∂η (a, x) ∂κ a

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Integrable (fun x ↦ (∫ (a : α), rexp (f a) ∂μ)⁻¹ • rexp (f x) • g x) μ ↔ Integrable (fun x ↦ rexp (f x) • g x) μ

Tactic:
rw [integrable_fun_smul_iff]

Goal state after:
case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ (∫ (a : α), rexp (f a) ∂μ)⁻¹ ≠ 0
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ AEMeasurable g ν

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, g x ≠ ∞

Tactic:
· exact ((measurable_exp.comp_aemeasurable hfν).div_const _).ennreal_ofReal

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, g x ≠ ∞
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : ¬Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

Tactic:
· simp only [hμν, h_int, and_self, ↓reduceIte]
    rw [ofReal_integral_eq_lintegral_ofReal]
    · rwa [integrable_klFun_rnDeriv_iff hμν]
    · exact ae_of_all _ fun _ ↦ klFun_nonneg ENNReal.toReal_nonneg

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : ¬Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: case pos
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
C : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∈ s n → ∑' (n : ι), ‖f n x‖ₑ < ∞
D : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∉ s n → f n x = 0
x : X
hx : ∀ (n : ι), x ∈ s n → ∑' (n : ι), ‖f n x‖ₑ < ∞
h'x : ∀ (n : ι), x ∉ s n → f n x = 0
h : ∃ n, x ∈ s n
⊢ ∑' (n : ι), ‖f n x‖ₑ < ∞

pp: case neg
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
C : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∈ s n → ∑' (n : ι), ‖f n x‖ₑ < ∞
D : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∉ s n → f n x = 0
x : X
hx : ∀ (n : ι), x ∈ s n → ∑' (n : ι), ‖f n x‖ₑ < ∞
h'x : ∀ (n : ι), x ∉ s n → f n x = 0
h : ∀ (n : ι), x ∉ s n
⊢ ∑' (n : ι), ‖f n x‖ₑ < ∞

Tactic:
· rcases h with ⟨n, hn⟩
    exact hx n hn

Goal state after:
case neg
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
C : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∈ s n → ∑' (n : ι), ‖f n x‖ₑ < ∞
D : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∉ s n → f n x = 0
x : X
hx : ∀ (n : ι), x ∈ s n → ∑' (n : ι), ‖f n x‖ₑ < ∞
h'x : ∀ (n : ι), x ∉ s n → f n x = 0
h : ∀ (n : ι), x ∉ s n
⊢ ∑' (n : ι), ‖f n x‖ₑ < ∞
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)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf) x ∂μ →
        ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg) x ∂μ →
          ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf + MemLp.toLp g hg)) x ∂μ =
            ∫ (x : α) in s, ↑↑(MemLp.toLp f hf + MemLp.toLp g hg) x ∂μ

Tactic:
intro f g hf_Lp hg_Lp _ hf hg
    simp_rw [(condExpL1CLM F' hm μ).map_add]
    rw [setIntegral_congr_ae (hm s hs) ((Lp.coeFn_add (condExpL1CLM F' hm μ (hf_Lp.toLp f))
      (condExpL1CLM F' hm μ (hg_Lp.toLp g))).mono fun x hx _ => hx)]
    rw [setIntegral_congr_ae (hm s hs)
      ((Lp.coeFn_add (hf_Lp.toLp f) (hg_Lp.toLp g)).mono fun x hx _ => hx)]
    simp_rw [Pi.add_apply]
    rw [integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn,
      integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn, hf,
      hg]

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

Goal state before:
pp: case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E'
h_ae_eq_f : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯) =ᵐ[μ] fun a ↦ ⟪c, ↑↑f a⟫
⊢ ∫ (a : α) in s, ⟪c, ↑↑↑((condExpL2 E' 𝕜 hm) f) a⟫ ∂μ - ∫ (a : α) in s, ⟪c, ↑↑f a⟫ ∂μ = 0

Tactic:
sub_eq_zero,

Goal state after:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E'
h_ae_eq_f : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯) =ᵐ[μ] fun a ↦ ⟪c, ↑↑f a⟫
⊢ ∫ (a : α) in s, ⟪c, ↑↑↑((condExpL2 E' 𝕜 hm) f) a⟫ ∂μ = ∫ (a : α) in s, ⟪c, ↑↑f a⟫ ∂μ
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:
· rw [ae_zero]; exact eventually_bot

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_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))) μ
t : Set α
ht : MeasurableSet t
hμt : (μ.trim hm) t < ∞
⊢ 0 ≤ ∫ (x : α) in t, AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ.trim hm

Tactic:
rw [← setIntegral_trim hm h.stronglyMeasurable_mk ht]

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))) μ
t : Set α
ht : MeasurableSet t
hμt : (μ.trim hm) t < ∞
⊢ 0 ≤ ∫ (x : α) in t, AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case pos.refine_3
α : 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 μ
t : Set α
ht : MeasurableSet t
a✝ : (μ.restrict s) t < ∞
⊢ ∫ (x : α) in t ∩ s, μ[f | m] x ∂μ = ∫ (x : α) in t ∩ s, 0 x ∂μ

Tactic:
setIntegral_condExp hm hf_int (ht.inter hs),

Goal state after:
case pos.refine_3
α : 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 μ
t : Set α
ht : MeasurableSet t
a✝ : (μ.restrict s) t < ∞
⊢ ∫ (x : α) in t ∩ s, f x ∂μ = ∫ (x : α) in t ∩ s, 0 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 (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    ∫ (a : 𝓧), llr μ ν a ∂μ + ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ

Tactic:
by
  have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
  have ⟨h_int_μν, h_int_κη⟩ := (integrable_llr_compProd_iff h_ac).mp h_int
  have h_int1 : Integrable (fun p ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ) := by
    rw [Measure.integrable_compProd_iff]
    · simp only [ne_eq, enorm_ne_top, not_false_eq_true, integrable_const_enorm,
      Filter.eventually_true, integral_const, probReal_univ, smul_eq_mul, one_mul, true_and]
      rwa [← integrable_norm_iff (by fun_prop)] at h_int_μν
    · exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)
  calc ∫ p, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ
  _ = ∫ p, ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂(ν ⊗ₘ η) := by
    rw [integral_rnDeriv_mul_log h_ac]
  _ = ∫ p, ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal *
      (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) ∂(ν ⊗ₘ η) :=
    integral_congr_ae (rnDeriv_compProd_mul_log_eq_mul_add h_ac_κη)
  _ = ∫ p, (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) ∂(μ ⊗ₘ κ) :=
    integral_rnDeriv_smul h_ac
  _ = ∫ p, log ((∂μ/∂ν) p.1).toReal ∂(μ ⊗ₘ κ) +
      ∫ p, log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂(μ ⊗ₘ κ) := by
    rw [integral_add h_int1]
    exact h_int_κη.ofReal
  _ = ∫ a, llr μ ν a ∂μ + ∫ p, llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂(μ ⊗ₘ κ) := by
    congr
    rw [Measure.integral_compProd h_int1]
    simp [llr]

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 μ
inst✝ : HereditarilyLindelofSpace E
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) μ
L : ℕ → E →L[ℝ] ℝ
c : ℕ → ℝ
hLc1 : ∀ (i : ℕ), s.domRestrict ⇑(L i) + const (↑s) (c i) ≤ s.domRestrict φ
hLc2 : ⨆ i, s.domRestrict ⇑(L i) + const (↑s) (c i) = s.domRestrict φ
⊢ ∀ᵐ (a : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a

Tactic:
have hp := ae_all_iff.2 fun i => (L i).comp_condExp_add_const_comm hm hf_int (c i)

Goal state after:
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 μ
inst✝ : HereditarilyLindelofSpace E
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) μ
L : ℕ → E →L[ℝ] ℝ
c : ℕ → ℝ
hLc1 : ∀ (i : ℕ), s.domRestrict ⇑(L i) + const (↑s) (c i) ≤ s.domRestrict φ
hLc2 : ⨆ i, s.domRestrict ⇑(L i) + const (↑s) (c i) = s.domRestrict φ
hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (fun x ↦ (L i) (μ[f | m] x) + c i) a = μ[fun y ↦ (L i) (f y) + c i | m] a
⊢ ∀ᵐ (a : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: case refine_2
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this✝ : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
⊢ ∀ (s : Set 𝓧),
    MeasurableSet s →
      ν s < ∞ →
        ∫ (x : 𝓧) in s, ((Measure.map g μ).rnDeriv (Measure.map g ν) (g x)).toReal ∂ν =
          ∫ (x : 𝓧) in s, (μ.rnDeriv ν x).toReal ∂ν

pp: case refine_3
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this✝ : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
⊢ AEStronglyMeasurable (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) ν

Tactic:
· rintro _ ⟨t, ht, rfl⟩ _
    calc ∫ x in g ⁻¹' t, ((μ.map g).rnDeriv (ν.map g) (g x)).toReal ∂ν
    _ = ∫ y in t, ((μ.map g).rnDeriv (ν.map g) y).toReal ∂(ν.map g) := by
      rw [setIntegral_map ht _ hg.aemeasurable]
      exact Measurable.aestronglyMeasurable (by fun_prop)
    _ = ∫ x in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν := by
      rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]

Goal state after:
case refine_3
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this✝ : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
⊢ AEStronglyMeasurable (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) ν
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
hAi : ∑ j, A i j = 1
j : ι
⊢ (if j = i then 1 else 0) = (Finset.affineCombination k Finset.univ (⇑(b.coord j) ∘ p)) fun j ↦ A i j

Tactic:
Finset.univ.affineCombination_eq_linear_combination _ _ hAi

Goal state after:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
hAi : ∑ j, A i j = 1
j : ι
⊢ (if j = i then 1 else 0) = ∑ i_1, A i i_1 • (⇑(b.coord j) ∘ p) i_1