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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsZeroOrMarkovKernel κ
η : Kernel β γ
inst✝ : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)

Tactic:
obtain rfl | _ := eq_zero_or_isMarkovKernel κ

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsZeroOrMarkovKernel η
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (η ∘ₖ 0)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsZeroOrMarkovKernel κ
η : Kernel β γ
inst✝ : IsZeroOrMarkovKernel η
h✝ : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
⊢ κ ∥ₖ 0 = 0

Tactic:
by_cases h : IsSFiniteKernel κ
  · ext; simp [parallelComp_apply]
  · exact parallelComp_of_not_isSFiniteKernel_left _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsZeroOrMarkovKernel κ
inst✝ : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)

Tactic:
obtain rfl | _ := eq_zero_or_isMarkovKernel κ

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
x : α × γ
inst✝¹ : IsZeroOrMarkovKernel η
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (0 ∥ₖ η)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsZeroOrMarkovKernel κ
inst✝ : IsZeroOrMarkovKernel η
h✝ : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hg : Measurable g
a : γ
⊢ ((κ.comap g hg) a) Set.univ ≤ κ.bound

Tactic:
rw [comap_apply' κ hg a Set.univ]

Goal state after:
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hg : Measurable g
a : γ
⊢ (κ (g a)) Set.univ ≤ κ.bound
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
⊢ (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

Tactic:
by_cases hf : Measurable f
  · simp only [map, hf, ↓reduceDIte]
    rfl
  · simp [map_of_not_measurable _ hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
⊢ (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)

Tactic:
by_cases hf : Measurable f
  · simp only [map, hf, ↓reduceDIte]
    rfl
  · simp [map_of_not_measurable _ hf]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
· refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
    rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prodMk_left hs)]
      at hs_zero ⊢
    filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ ∫⁻ (a : Y × T), (Measure.dirac a.swap) s ∂(κ ac.1).prod (η ac.2) = ∫⁻ (b : T), (κ ac.1) (Prod.mk b ⁻¹' s) ∂η ac.2

Tactic:
MeasureTheory.lintegral_prod_symm

Goal state after:
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ ∫⁻ (y : T), ∫⁻ (x : Y), (Measure.dirac (x, y).swap) s ∂κ ac.1 ∂η ac.2 = ∫⁻ (b : T), (κ ac.1) (Prod.mk b ⁻¹' s) ∂η ac.2

case pos.hf
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ (Measure.dirac a.swap) s) ((κ ac.1).prod (η ac.2))
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ∞

Tactic:
have ht : MeasurableSet t := measurableSet_toMeasurable _ _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
⊢ ∀ᵐ (b : β) ∂κ a, (η (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
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
δ : Type u_5
inst✝ : TopologicalSpace δ
f : β × γ → δ
hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ ∀ᵐ (x : β) ∂κ a, AEStronglyMeasurable (fun y ↦ f (x, y)) (η (a, x))

Tactic:
by
  filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with x hx using
    ⟨fun y => hf.mk f (x, y), hf.stronglyMeasurable_mk.comp_measurable measurable_prodMk_left, hx⟩

Goal state after:
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f (x, y) ∂κ x

Tactic:
← uncurry_curry f

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : StronglyMeasurable (uncurry (Function.curry f))
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f (x, y) ∂κ x
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: case neg.refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) ≤ (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν) * (ν.real univ)⁻¹
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
← div_le_iff₀,

Goal state after:
case neg.refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) / (ν.real univ)⁻¹ ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

case neg.refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) ≤ (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν) * (ν.real univ)⁻¹
⊢ 0 < (ν.real univ)⁻¹
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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
⊢ (∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ∞) →
    (∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂η b ∂κ a < ∞ ↔
      ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂η a).toReal ∂κ a < ∞)

Tactic:
intro h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h : ∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ∞
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂η b ∂κ a < ∞ ↔ ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂η a).toReal ∂κ a < ∞
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case mp
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ klDiv μ ν = ∞ → μ ≪ ν → ¬Integrable (llr μ ν) μ

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : klDiv μ ν = ∞
⊢ μ ≪ ν → ¬Integrable (llr μ ν) μ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case mpr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ (μ ≪ ν → ¬Integrable (llr μ ν) μ) → klDiv μ ν = ∞

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν → ¬Integrable (llr μ ν) μ
⊢ klDiv μ ν = ∞
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
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 μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞) =
    if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞

Tactic:
simp [hμν, h_int, h_int_iff, integrable_klFun_rnDeriv_iff hμν]

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : c = 0
⊢ (klDiv μ (c • ν)).toReal = ↑c * (klDiv (c⁻¹ • μ) ν).toReal

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ (klDiv μ (c • ν)).toReal = ↑c * (klDiv (c⁻¹ • μ) ν).toReal

Tactic:
· simp only [hc, zero_smul, NNReal.coe_zero, inv_zero, klDiv_zero_left, zero_mul]
    rcases eq_zero_or_neZero μ with rfl | hμ <;> simp

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ (klDiv μ (c • ν)).toReal = ↑c * (klDiv (c⁻¹ • μ) ν).toReal
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
⊢ f ∈ (lpMeas F 𝕜 m p μ).carrier ↔ AEStronglyMeasurable (↑↑f) μ

Tactic:
lpMeas,

Goal state after:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
⊢ f ∈ { carrier := {f | AEStronglyMeasurable (↑↑f) μ}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }.carrier ↔
    AEStronglyMeasurable (↑↑f) μ
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 : ↥(Lp F p (μ.trim hm))
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) =ᵐ[μ.trim hm] ↑↑f

Tactic:
refine
    (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _) ?_

Goal state after:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) =ᵐ[μ] ↑↑f
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∫ (x : α) in s, ‖g x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

Tactic:
exact integral_norm_le_of_forall_fin_meas_integral_eq hm hf hfi hg hgi hgf hs hμs

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

Goal state before:
pp: α : 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)
⊢ (fun x ↦ ↑‖g x‖₊) =ᵐ[μ.restrict s] fun x ↦ ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊

Tactic:
refine hg_eq_restrict.mono fun x hx => ?_

Goal state after:
α : 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)
x : α
hx : g x = ↑↑↑((condExpL2 ℝ ℝ hm) f) x
⊢ (fun x ↦ ↑‖g x‖₊) x = (fun x ↦ ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) x
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᵐ[ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
⊢ μ.rnDeriv ν x = 1 x

Tactic:
have hx' : klFun (μ.rnDeriv ν x).toReal = 0 := le_antisymm hx (klFun_nonneg ENNReal.toReal_nonneg)

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᵐ[ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
hx' : klFun (μ.rnDeriv ν x).toReal = 0
⊢ μ.rnDeriv ν x = 1 x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x y : G
⊢ (compLpL 2 μ (toSpanSingleton ℝ x) + compLpL 2 μ (toSpanSingleton ℝ y))
      ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) =
    (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) +
      (compLpL 2 μ (toSpanSingleton ℝ y)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))

Tactic:
add_apply

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x y : G
⊢ (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) +
      (compLpL 2 μ (toSpanSingleton ℝ y)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) =
    (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) +
      (compLpL 2 μ (toSpanSingleton ℝ y)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case insert
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
i : ι
s : Finset ι
his : i ∉ s
heq : (∀ i ∈ s, Integrable (f i) μ) → μ[∑ i ∈ s, f i | m] =ᵐ[μ] ∑ i ∈ s, μ[f i | m]
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ μ[f i + ∑ x ∈ s, f x | m] =ᵐ[μ] ∑ i ∈ insert i s, μ[f i | m]

Tactic:
Finset.sum_insert his

Goal state after:
case insert
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
i : ι
s : Finset ι
his : i ∉ s
heq : (∀ i ∈ s, Integrable (f i) μ) → μ[∑ i ∈ s, f i | m] =ᵐ[μ] ∑ i ∈ s, μ[f i | m]
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ μ[f i + ∑ x ∈ s, f x | m] =ᵐ[μ] μ[f i | m] + ∑ x ∈ s, μ[f x | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos.refine_1
α : 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)
⊢ Integrable (⇑T ∘ f) μ

Tactic:
exact T.integrable_comp hf_int

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst✝ : NeZero P
X : Ω → ℝ≥0∞
hP : ¬IsFiniteMeasure P
hσ : ¬SigmaFinite (P.trim ⋯)
⊢ P⁻[X | ⊥] = fun x ↦ (P Set.univ)⁻¹ • ∫⁻ (ω : Ω), X ω ∂P

Tactic:
rw [not_isFiniteMeasure_iff] at hP

Goal state after:
case neg
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst✝ : NeZero P
X : Ω → ℝ≥0∞
hP : P Set.univ = ∞
hσ : ¬SigmaFinite (P.trim ⋯)
⊢ P⁻[X | ⊥] = fun x ↦ (P Set.univ)⁻¹ • ∫⁻ (ω : Ω), X ω ∂P
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
a : 𝓧
ha1 : ((∂Measure.map g μ/∂Measure.map g ν) (g a)).toReal = ν[fun a ↦ ((∂μ/∂ν) a).toReal | MeasurableSpace.comap g m𝓨] a
⊢ f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] a) ≤
      ν[fun x ↦ f ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] a →
    f ((∂Measure.map g μ/∂Measure.map g ν) (g a)).toReal ≤
      ν[fun x ↦ f ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] a

Tactic:
ha2

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
a : 𝓧
ha1 : ((∂Measure.map g μ/∂Measure.map g ν) (g a)).toReal = ν[fun a ↦ ((∂μ/∂ν) a).toReal | MeasurableSpace.comap g m𝓨] a
ha2 :
  f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] a) ≤
    ν[fun x ↦ f ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] a
⊢ f ((∂Measure.map g μ/∂Measure.map g ν) (g a)).toReal ≤ ν[fun x ↦ f ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] a
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
a : 𝓧
ha1 : ((∂μ.trim hm/∂ν.trim hm) a).toReal = ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] a
⊢ f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] a) ≤ ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] a →
    f ((∂μ.trim hm/∂ν.trim hm) a).toReal ≤ ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] a

Tactic:
ha2

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
a : 𝓧
ha1 : ((∂μ.trim hm/∂ν.trim hm) a).toReal = ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] a
ha2 : f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] a) ≤ ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] a
⊢ f ((∂μ.trim hm/∂ν.trim hm) a).toReal ≤ ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] a
Module: Mathlib.Lean.Thunk

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

Tactic:
intro; ext; assumption

Goal state after: