mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ ∫ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

Tactic:
← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht),

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 η
inst✝ : NormedSpace ℝ E
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ ∫ (z : β × γ), f z ∂((κ ⊗ₖ η).restrict ⋯) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
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
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
a : α
s : Set ((β × γ) × δ)
hs : MeasurableSet s
⊢ Measurable ⇑MeasurableEquiv.prodAssoc.symm

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : μ s < ∞
⊢ ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a ∂μ =
    ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : μ s < ∞
⊢ Measurable ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : μ s < ∞
⊢ ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a ∂μ = ∫⁻ (a : 𝓧) in s, (κ a) univ ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ ∀ᵐ (a : 𝓧) ∂μ, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = (κ a) univ

Tactic:
by

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
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ ∫ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

Tactic:
by

Goal state after:
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
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
a : α
s : Set ((β × γ) × δ)
hs : MeasurableSet s
b : β
⊢ Measurable fun x ↦ MeasurableEquiv.prodAssoc.symm (b, x)

Tactic:
by

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
f : β × γ → E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ univ) ((κ ⊗ₖ η) a)
⊢ ∫ (z : β × γ) in s ×ˢ univ, f z ∂(κ ⊗ₖ η) a = ∫ (x : β) in s, ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a

Tactic:
by

Goal state after:
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
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯)).map ⇑MeasurableEquiv.prodAssoc.symm = κ ⊗ₖ η ⊗ₖ ξ

Tactic:
by

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
f : β × γ → E
t : Set γ
ht : MeasurableSet t
hf : IntegrableOn f (univ ×ˢ t) ((κ ⊗ₖ η) a)
⊢ ∫ (z : β × γ) in univ ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

Tactic:
by

Goal state after:
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

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 α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ (fun x ↦ ∫ (y : γ), f y ∂η x) =ᵐ[κ a] fun x ↦ ∫ (y : γ), AEStronglyMeasurable.mk f hf y ∂η x

Tactic:
by

Goal state after:
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 α β
η : Kernel β γ
δ : Type u_5
inst✝ : TopologicalSpace δ
f : γ → δ
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ ∀ᵐ (x : β) ∂κ a, AEStronglyMeasurable f (η x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (fun x ↦ rexp (f x)) μ

Tactic:
by

Goal state after:
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

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun p ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
⊢ StronglyMeasurable fun p ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
by

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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
p✝ q✝ r✝ : Prop
h : r✝ → p✝
⊢ (r✝ ↔ p✝ ∧ q✝) ↔ p✝ → (r✝ ↔ q✝)

Tactic:
by

Goal state after:
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

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun p ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable : Integrable (fun x ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)
⊢ StronglyMeasurable fun x ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
⊢ ∫⁻ (x : α), g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
by

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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
⊢ HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f y‖ ∂η x) (κ a)

Tactic:
by

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 : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
this : AEMeasurable (fun x ↦ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (fun x ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict s)

Tactic:
by

Goal state after:
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

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 : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (fun x ↦ rexp (f x)) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
⊢ ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a

Tactic:
by

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 : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
by

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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f y‖ ∂η x) (κ a)

Tactic:
by

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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ Integrable f ((η ∘ₖ κ) a) ↔ (∀ᵐ (y : β) ∂κ a, Integrable f (η y)) ∧ Integrable (fun y ↦ ∫ (z : γ), ‖f z‖ ∂η y) (κ a)

Tactic:
by

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

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
⊢ MeasurableSet (Prod.map id f '' t)

Tactic:
· exact (MeasurableEmbedding.id.prodMap hf).measurableSet_image.mpr ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ Integrable f (⇑κ ∘ₘ μ) ↔ (∀ᵐ (x : α) ∂μ, Integrable f (κ x)) ∧ Integrable (fun x ↦ ∫ (y : β), ‖f y‖ ∂κ x) μ

Tactic:
by

Goal state after:
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
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
⊢ (κ ⊗ₖ η).comapRight ⋯ = κ ⊗ₖ η.comapRight hf

Tactic:
by

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 α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ ∫ (x : β), F (∫ (y : γ), f y + g y ∂η x) ∂κ a = ∫ (x : β), F (∫ (y : γ), f y ∂η x + ∫ (y : γ), g y ∂η x) ∂κ a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
h_ae1 : ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
⊢ ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)

Tactic:
by

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
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
this : AEMeasurable (fun x ↦ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (fun x ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict s)

Tactic:
by

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 α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ ∫ (x : β), F (∫ (y : γ), f y - g y ∂η x) ∂κ a = ∫ (x : β), F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x) ∂κ a

Tactic:
by

Goal state after:
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 η
x : α
s : Set β
hs : MeasurableSet s
b : β
⊢ (η (x, b)) {c | b ∈ s} = s.indicator (fun b ↦ (η (x, b)) Set.univ) b

Tactic:
by

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
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (fun x ↦ rexp (f x)) μ

Tactic:
by

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 α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ ∫⁻ (x : β), F (∫ (y : γ), f y - g y ∂η x) ∂κ a = ∫⁻ (x : β), F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x) ∂κ a

Tactic:
by

Goal state after:
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 η
x : α
s : Set β
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η).fst x) s = ∫⁻ (b : β), s.indicator (fun b ↦ (η (x, b)) Set.univ) b ∂κ x

Tactic:
by

Goal state after:
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✝ : IsMarkovKernel η
⊢ (κ ⊗ₖ η).fst = κ

Tactic:
by

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
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
a : α
ha : μ.rnDeriv μ a = 1
⊢ llr μ μ a = 0 a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ llr μ μ =ᵐ[μ] 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ (fun x ↦ rexp (llr μ ν x)) =ᵐ[ν] fun x ↦ if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ (fun x ↦ rexp (llr μ ν x)) =ᵐ[μ] fun x ↦ (μ.rnDeriv ν x).toReal

Tactic:
by

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 : α → ℝ
g : α → E
⊢ ∫ (x : α), g x ∂μ.tilted f = ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
⊢ (fun x ↦ rexp (llr μ ν x)) =ᵐ[ν] fun x ↦ (μ.rnDeriv ν x).toReal

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ -llr μ ν =ᵐ[μ] llr ν μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ (fun x ↦ rexp (-llr μ ν x)) =ᵐ[μ] fun x ↦ (ν.rnDeriv μ x).toReal

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
⊢ ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
by

Goal state after: