mathlib-initiative/mathlib-tactics huggingface dataset:
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 δ
κ : Kernel (α × β) γ
inst✝ : ∀ (b : β), IsMarkovKernel (κ.sectL b)
⊢ IsMarkovKernel κ

Tactic:
refine ⟨fun _ ↦ ⟨?_⟩⟩

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 δ
κ : Kernel (α × β) γ
inst✝ : ∀ (b : β), IsMarkovKernel (κ.sectL b)
x✝ : α × β
⊢ (κ x✝) Set.univ = 1
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 δ
κ : Kernel (α × β) γ
inst✝ : ∀ (b : α), IsMarkovKernel (κ.sectR b)
⊢ IsMarkovKernel κ

Tactic:
refine ⟨fun _ ↦ ⟨?_⟩⟩

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 δ
κ : Kernel (α × β) γ
inst✝ : ∀ (b : α), IsMarkovKernel (κ.sectR b)
x✝ : α × β
⊢ (κ x✝) Set.univ = 1
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
by_cases hη : IsSFiniteKernel η

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
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 κ
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z

Tactic:
by_cases hη : IsSFiniteKernel η

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 η
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z

case neg
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 η
⊢ swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z
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 κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)

Tactic:
by_cases hη : IsSFiniteKernel η

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 η
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)

case neg
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 η
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂η x ∂κ x = ∫⁻ (b : γ × β), f b ∂(η ×ₖ κ) x

pp: case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a ↦ f a.swap

Tactic:
lintegral_prod _ _ _ hf

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂η x ∂κ x = ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂κ x ∂η x

case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a ↦ f a.swap
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc

Tactic:
by_cases hη : IsSFiniteKernel η

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : ¬IsSFiniteKernel κ
⊢ ⇑η ∘ₘ μ ⊗ₘ κ = (⇑(κ ⊗ₖ η) ∘ₘ μ).snd

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
⊢ ⇑η ∘ₘ μ ⊗ₘ κ = (⇑(κ ⊗ₖ η) ∘ₘ μ).snd

Tactic:
· simp [compProd_of_not_isSFiniteKernel _ _ hκ,
      Kernel.compProd_of_not_isSFiniteKernel_left _ _ hκ, FunLike.coe_zero]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
⊢ ⇑η ∘ₘ μ ⊗ₘ κ = (⇑(κ ⊗ₖ η) ∘ₘ μ).snd
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 γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ ∫⁻ (b : β), ((η.restrict ht) (a, b)) (Prod.mk b ⁻¹' u) ∂(κ.restrict hs) a =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' (u ∩ s ×ˢ t)) ∂κ a

Tactic:
simp only [restrict_apply, Set.preimage, Measure.restrict_apply' ht, Set.mem_inter_iff,
    Set.mem_prod]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ ∫⁻ (b : β) in s, (η (a, b)) ({x | (b, x) ∈ u} ∩ t) ∂κ a = ∫⁻ (b : β), (η (a, b)) {x | (b, x) ∈ u ∧ b ∈ s ∧ x ∈ t} ∂κ a
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 : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂η (a, x) < ∞
⊢ (fun b ↦ ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂η (a, b)) =ᵐ[κ a] fun a_1 ↦
    ENNReal.ofReal (∫⁻ (a : γ), ‖f (a_1, a)‖ₑ ∂η (a, a_1)).toReal

Tactic:
filter_upwards [h2f] with x hx

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 α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂η (a, x) < ∞
x : β
hx : ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂η (a, x) < ∞
⊢ ∫⁻ (c : γ), ‖f (x, c)‖ₑ ∂η (a, x) = ENNReal.ofReal (∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂η (a, x)).toReal
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
simp only [hf, not_false_eq_true, tilted_of_not_integrable, Measure.coe_zero,
      Pi.zero_apply, integral_undef hf, div_zero, integral_zero, ENNReal.ofReal_zero]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯)).map ⇑MeasurableEquiv.prodAssoc.symm = κ ⊗ₖ η ⊗ₖ ξ

Tactic:
by_cases hη : IsSFiniteKernel η

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯)).map ⇑MeasurableEquiv.prodAssoc.symm = κ ⊗ₖ η ⊗ₖ ξ

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯)).map ⇑MeasurableEquiv.prodAssoc.symm = κ ⊗ₖ η ⊗ₖ ξ
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 γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η

Tactic:
by_cases hη : IsSFiniteKernel η

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η
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 γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun i ↦ κ i ⊗ₖ η

Tactic:
by_cases hη : IsSFiniteKernel η

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun i ↦ κ i ⊗ₖ η

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : ¬IsSFiniteKernel η
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun i ↦ κ i ⊗ₖ η
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ llr (c⁻¹ • μ) ν =ᵐ[μ] llr μ (c • ν)

Tactic:
by
  have hc' : c⁻¹ ≠ 0 := by simp [hc_ne_top]
  have hc_ne_top' : c⁻¹ ≠ ∞ := by simp [hc]
  filter_upwards [llr_smul_left hμν c⁻¹ hc' hc_ne_top', llr_smul_right hμν c hc hc_ne_top] with
    x hx_left hx_right
  rw [hx_left, hx_right]
  simp [sub_eq_add_neg]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
E : Type u_8
inst✝ : NormedAddCommGroup E
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
⊢ Integrable f (μ ⊗ₘ κ) ↔
    (∀ᵐ (x : α) ∂μ, Integrable (fun y ↦ f (x, y)) (κ x)) ∧ Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ

Tactic:
Measure.compProd,

Goal state after:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
E : Type u_8
inst✝ : NormedAddCommGroup E
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
⊢ Integrable f ((Kernel.const Unit μ ⊗ₖ prodMkLeft Unit κ) ()) ↔
    (∀ᵐ (x : α) ∂μ, Integrable (fun y ↦ f (x, y)) (κ x)) ∧ Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
E : Type u_8
inst✝ : NormedAddCommGroup E
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
⊢ Integrable f (μ ⊗ₘ κ) ↔
    (∀ᵐ (x : α) ∂μ, Integrable (fun y ↦ f (x, y)) (κ x)) ∧ Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ

Tactic:
simp_rw [Measure.compProd, ProbabilityTheory.integrable_compProd_iff hf, Kernel.prodMkLeft_apply,
    Kernel.const_apply]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ ⊗ₘ κ)
⊢ ∫ (x : α × β), f x ∂μ ⊗ₘ κ = ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ

Tactic:
Measure.compProd,

Goal state after:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ ⊗ₘ κ)
⊢ ∫ (x : α × β), f x ∂(Kernel.const Unit μ ⊗ₖ prodMkLeft Unit κ) () = ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
Measure.compProd,

Goal state after:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α × β) in s ×ˢ t, f x ∂(Kernel.const Unit μ ⊗ₖ prodMkLeft Unit κ) () =
    ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f : ∀ (s : Set α), MeasurableSet s → 0 < μ s → ∞ ≤ μ s
fn : ℕ → SimpleFunc α E
hfn : ∀ (n : ℕ), μ (Function.support ⇑(fn n)) < ∞
hfn_lim : ∀ (x : α), Tendsto (fun n ↦ (fn n) x) atTop (𝓝 (f x))
A : ∀ (n : ℕ), μ (Function.support ⇑(fn n)) = 0
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), (fn n) x = 0
x : α
hx : ∀ (n : ℕ), (fn n) x = 0
⊢ f x = 0 x

Tactic:
apply tendsto_nhds_unique (hfn_lim x)

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f : ∀ (s : Set α), MeasurableSet s → 0 < μ s → ∞ ≤ μ s
fn : ℕ → SimpleFunc α E
hfn : ∀ (n : ℕ), μ (Function.support ⇑(fn n)) < ∞
hfn_lim : ∀ (x : α), Tendsto (fun n ↦ (fn n) x) atTop (𝓝 (f x))
A : ∀ (n : ℕ), μ (Function.support ⇑(fn n)) = 0
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), (fn n) x = 0
x : α
hx : ∀ (n : ℕ), (fn n) x = 0
⊢ Tendsto (fun n ↦ (fn n) x) atTop (𝓝 (0 x))
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
⊢ klDiv μ (c • ν) = ↑c * klDiv (c⁻¹ • μ) ν

Tactic:
have hc' : (c : ℝ≥0∞) ≠ 0 := by simpa

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
⊢ klDiv μ (c • ν) = ↑c * klDiv (c⁻¹ • μ) ν
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))
hf_mem_ℒp : MemLp (↑↑f) p μ := memLp_of_memLp_trim hm (Lp.memLp f)
⊢ MemLp.toLp ↑↑f ⋯ ∈ lpMeasSubgroup F m p μ

Tactic:
mem_lpMeasSubgroup_iff_aestronglyMeasurable

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))
hf_mem_ℒp : MemLp (↑↑f) p μ := memLp_of_memLp_trim hm (Lp.memLp f)
⊢ AEStronglyMeasurable (↑↑(MemLp.toLp ↑↑f ⋯)) μ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
⊢ klDiv (c • μ) (c • ν) = ↑c * klDiv μ ν

Tactic:
have hc' : (c : ℝ≥0∞) ≠ 0 := by simpa

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
hc' : ↑c ≠ 0
⊢ klDiv (c • μ) (c • ν) = ↑c * klDiv μ ν
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
ι : 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 < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ 0 ≤ 1 - p.toReal⁻¹

Tactic:
simp only [sub_nonneg]

Goal state after:
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 < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ p.toReal⁻¹ ≤ 1
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)
inst✝ : CompleteSpace E
f : ℕ → ↥(Lp E p μ)
hf : ∑' (n : ℕ), ‖f n‖ₑ ≠ ∞
A : ∀ᵐ (a : X) ∂μ, Summable fun n ↦ ‖↑↑(f n) a‖
B : ∀ᵐ (x : X) ∂μ, ∀ (n : ℕ), ↑↑(∑ i ∈ range n, f i) x = ∑ i ∈ range n, ↑↑(f i) x
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ℕ), f n) a)

Tactic:
obtain ⟨ns, hns, nslim⟩ : ∃ ns : ℕ → ℕ, StrictMono ns ∧ ∀ᵐ x ∂μ,
      Tendsto (fun i ↦ (∑ j ∈ range (ns i), f j : Lp E p μ) x) atTop (𝓝 ((∑' n, f n) x)) := by
    have : Tendsto (fun i ↦ (∑ j ∈ range i, f j)) atTop (𝓝 (∑' n, f n)) :=
      Summable.tendsto_sum_tsum_nat (Summable.of_enorm hf)
    exact (tendstoInMeasure_of_tendsto_Lp this).exists_seq_tendsto_ae

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace E
f : ℕ → ↥(Lp E p μ)
hf : ∑' (n : ℕ), ‖f n‖ₑ ≠ ∞
A : ∀ᵐ (a : X) ∂μ, Summable fun n ↦ ‖↑↑(f n) a‖
B : ∀ᵐ (x : X) ∂μ, ∀ (n : ℕ), ↑↑(∑ i ∈ range n, f i) x = ∑ i ∈ range n, ↑↑(f i) x
ns : ℕ → ℕ
hns : StrictMono ns
nslim : ∀ᵐ (x : X) ∂μ, Tendsto (fun i ↦ ↑↑(∑ j ∈ range (ns i), f j) x) atTop (𝓝 (↑↑(∑' (n : ℕ), f n) x))
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ℕ), f n) a)
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: 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)

Tactic:
let : Fintype ι := Fintype.ofFinite ι
    filter_upwards [coeFn_fun_finsetSum univ f] with x hx
    rw [tsum_fintype, hx]
    exact hasSum_fintype _

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

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

Tactic:
by
  rw [setIntegral_congr_ae (hm s hs) ((condExp_ae_eq_condExpL1 hm f).mono fun x hx _ => hx)]
  exact setIntegral_condExpL1 hf hs

Goal state after: