awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : IsFiniteMeasure μ
κ : Kernel α β
inst_1 : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s) μ

Tactic:
Integrable.mono' (integrable_const κ.bound.toReal)
    ((κ.measurable_coe hs).ennreal_toReal.aestronglyMeasurable)
    (ae_of_all μ fun x ↦ ?_)

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.Integrable.mono', ENNReal.toReal, MeasureTheory.ae_of_all, ProbabilityTheory.Kernel.measurable_coe, Measurable.ennreal_toReal, MeasureTheory.integrable_const, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : IsFiniteMeasure μ
κ : Kernel α β
inst_1 : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
refine : ∀ (x : α), ‖Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s‖ ≤ κ.bound.toReal
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s) μ

Tactic:
refine Integrable.mono' (integrable_const κ.bound.toReal)
    ((κ.measurable_coe hs).ennreal_toReal.aestronglyMeasurable)
    (ae_of_all μ fun x ↦ ?_)

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.Integrable.mono', ENNReal.toReal, MeasureTheory.ae_of_all, ProbabilityTheory.Kernel.measurable_coe, Measurable.ennreal_toReal, MeasureTheory.integrable_const, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : IsFiniteMeasure μ
κ : Kernel α β
inst_1 : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
rw : Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s ≤ κ.bound.toReal
⊢ ‖Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s‖ ≤ κ.bound.toReal

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]

Premises used: MeasureTheory.measureReal_nonneg, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : IsFiniteMeasure μ
κ : Kernel α β
inst_1 : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s ≤ κ.bound.toReal

Tactic:
ENNReal.toReal_mono (Kernel.bound_ne_top _) (Kernel.measure_le_bound _ _ _)

Premises used: ProbabilityTheory.Kernel.bound_ne_top, MeasureTheory.Measure.real, ProbabilityTheory.Kernel.measure_le_bound, ENNReal.toReal_mono
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : IsFiniteMeasure μ
κ : Kernel α β
inst_1 : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s ≤ κ.bound.toReal

Tactic:
exact ENNReal.toReal_mono (Kernel.bound_ne_top _) (Kernel.measure_le_bound _ _ _)

Premises used: ProbabilityTheory.Kernel.bound_ne_top, ProbabilityTheory.Kernel.measure_le_bound, ENNReal.toReal_mono
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : IsFiniteMeasure μ
κ : Kernel α β
inst_1 : IsMarkovKernel κ
s : Set β
hs : MeasurableSet s
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s) μ

Tactic:
IsFiniteKernel.integrable μ κ hs

Premises used: ProbabilityTheory.Kernel.IsFiniteKernel.integrable
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
h₁ :
  Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ)
    (fun (a : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f a b) fun (a : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b
⊢ Eq.{u_3 + 1} (α := E) (∫ (a : α), @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f a b ∂μ)
    (∫ (a : α), @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
h₁ :
  ∀ (a : α) (ha : f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a),
    Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f a b)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b)
⊢ Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ)
    (fun (a : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f a b) fun (a : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b

Tactic:
filter_upwards [h] with _ ha
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
a : α
ha h₁ : f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f a b)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
a : α
ha : f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
a_1 : β
hb : f a a_1 = g a a_1
⊢ f a a_1 = g a a_1

Tactic:
hb
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
a : α
ha : f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x}
      a_1
h₂ h₃ : ∀ (a_1 : β) (hb : f a a_1 = g a a_1), f a a_1 = g a a_1
⊢ f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a

Tactic:
filter_upwards [ha] with _ hb using hb
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
pos :
  ∀ (ha : a ∈ s),
    Eq.{u_3 + 1} (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (y : β) ↦ s.indicator (fun (x : α) ↦ f x y) a)
      (s.indicator (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y) a)
neg :
  ∀ (ha : a ∉ s),
    Eq.{u_3 + 1} (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (y : β) ↦ s.indicator (fun (x : α) ↦ f x y) a)
      (s.indicator (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y) a)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (y : β) ↦ s.indicator (fun (x : α) ↦ f x y) a)
    (s.indicator (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y) a)

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
ha : a ∈ s
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (y : β) ↦ s.indicator (fun (x : α) ↦ f x y) a)
    (s.indicator (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y) a)

Tactic:
simp [ha]
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
ha : a ∉ s
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (y : β) ↦ s.indicator (fun (x : α) ↦ f x y) a)
    (s.indicator (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y) a)

Tactic:
simp [ha]
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
rw : (@integral _ _ _ _ mβ (Measure.dirac (g a)) fun (x : β) ↦ f x) = f (g a)
rw₁ rw₂ : f (g a) = f (g a)
⊢ (@integral _ _ _ _ mβ ((deterministic g hg : (a : α) → Measure β) a) fun (x : β) ↦ f x) = f (g a)

Tactic:
rw [deterministic_apply, integral_dirac' _ _ hf]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, MeasureTheory.integral_dirac'
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
inst_3 : MeasurableSingletonClass β
hg : Measurable g
rw : (@integral _ _ _ _ mβ (Measure.dirac (g a)) fun (x : β) ↦ f x) = f (g a)
rw₁ rw₂ : f (g a) = f (g a)
⊢ (@integral _ _ _ _ mβ ((deterministic g hg : (a : α) → Measure β) a) fun (x : β) ↦ f x) = f (g a)

Tactic:
rw [deterministic_apply, integral_dirac _ (g a)]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, MeasureTheory.integral_dirac
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
s : Set β
hs : MeasurableSet s
inst_3 : Decidable (g a ∈ s)
rw :
  (@integral _ _ _ _ mβ (Measure.restrict (Measure.dirac (g a)) s) fun (x : β) ↦ f x) = if g a ∈ s then f (g a) else 0
rw₁ rw₂ : (if g a ∈ s then f (g a) else 0) = if g a ∈ s then f (g a) else 0
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((deterministic g hg : (a : α) → Measure β) a) s) fun (x : β) ↦ f x) =
    if g a ∈ s then f (g a) else 0

Tactic:
rw [deterministic_apply, setIntegral_dirac' hf _ hs]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, MeasureTheory.setIntegral_dirac'
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
inst_3 : MeasurableSingletonClass β
hg : Measurable g
s : Set β
inst_4 : Decidable (g a ∈ s)
rw :
  (@integral _ _ _ _ mβ (Measure.restrict (Measure.dirac (g a)) s) fun (x : β) ↦ f x) = if g a ∈ s then f (g a) else 0
rw₁ rw₂ : (if g a ∈ s then f (g a) else 0) = if g a ∈ s then f (g a) else 0
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((deterministic g hg : (a : α) → Measure β) a) s) fun (x : β) ↦ f x) =
    if g a ∈ s then f (g a) else 0

Tactic:
rw [deterministic_apply, setIntegral_dirac f _ s]

Premises used: MeasureTheory.setIntegral_dirac, ProbabilityTheory.Kernel.deterministic_apply
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
rw rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (((const α μ : Kernel α β) : (a : α) → Measure β) a) fun (x : β) ↦ f x)
    (∫ (x : β), f x ∂μ)

Tactic:
rw [const_apply]

Premises used: ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
s : Set β
rw rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) (∫ (x : β) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict (((const α μ : Kernel α β) : (a : α) → Measure β) a) s) fun (x : β) ↦ f x)
    (∫ (x : β) in s, f x ∂μ)

Tactic:
rw [const_apply]

Premises used: ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
rw rw₁ :
  Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦ f x)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦ f x)
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((κ.restrict (s := s) hs : (a : α) → Measure β) a) fun (x : β) ↦ f x)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦ f x)

Tactic:
rw [restrict_apply]

Premises used: ProbabilityTheory.Kernel.restrict_apply
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
t : Set β
rw :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict (Measure.restrict ((κ : (a : α) → Measure β) a) s) t) fun (x : β) ↦ f x)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) (t ∩ s)) fun (x : β) ↦ f x)
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) (t ∩ s)) fun (x : β) ↦ f x)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) (t ∩ s)) fun (x : β) ↦ f x)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.restrict (s := s) hs : (a : α) → Measure β) a) t) fun (x : β) ↦ f x)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) (t ∩ s)) fun (x : β) ↦ f x)

Tactic:
rw [restrict_apply, Measure.restrict_restrict' hs]

Premises used: ProbabilityTheory.Kernel.restrict_apply, MeasureTheory.Measure.restrict_restrict'
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
simp_rw :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) fun (b : β) ↦
      g b)
    (if a ∈ s then @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((piecewise (s := s) hs κ η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
    (if a ∈ s then @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)

Tactic:
simp_rw [piecewise_apply]

Premises used: ProbabilityTheory.Kernel.piecewise_apply
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
pos :
  a ∈ s →
    Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b)
neg :
  a ∉ s →
    Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
      (@integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) fun (b : β) ↦
      g b)
    (if a ∈ s then @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
h : a ∈ s
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
h : a ∉ s
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
    (@integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
t : Set β
simp_rw :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ
      (Measure.restrict (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) t) fun (b : β) ↦
      g b)
    (if a ∈ s then @integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((piecewise (s := s) hs κ η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
    (if a ∈ s then @integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)

Tactic:
simp_rw [piecewise_apply]

Premises used: ProbabilityTheory.Kernel.piecewise_apply
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
t : Set β
pos :
  a ∈ s →
    Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
      (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
neg :
  a ∉ s →
    Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
      (@integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ
      (Measure.restrict (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) t) fun (b : β) ↦
      g b)
    (if a ∈ s then @integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
t : Set β
h : a ∈ s
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Integral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
t : Set β
h : a ∉ s
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
    (@integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Invariance
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
⊢ (⇑κ : (a : α) → Measure α) ∘ₘ μ = μ

Tactic:
hκ

Premises used: ProbabilityTheory.Kernel.Invariant
-- Module: Mathlib.Probability.Kernel.Invariance
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
rw : Eq (α := Kernel α α) (const α ((⇑κ : (a : α) → Measure α) ∘ₘ μ)) (const α μ)
rw₁ rw₂ : Eq (α := Kernel α α) (const α μ) (const α μ)
⊢ Eq (α := Kernel α α) (κ ∘ₖ const α μ) (const α μ)

Tactic:
rw [comp_const κ μ, hκ.def]

Premises used: ProbabilityTheory.Kernel.Invariant.def
-- Module: Mathlib.Probability.Kernel.Invariance
Goal:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
inl : IsEmpty α → (κ ∘ₖ η).Invariant μ
inr : ∀ (hα : Nonempty α), (κ ∘ₖ η).Invariant μ
⊢ (κ ∘ₖ η).Invariant μ

Tactic:
rcases isEmpty_or_nonempty α with _ | hα

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Probability.Kernel.Invariance
Goal:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
h : IsEmpty α
⊢ (κ ∘ₖ η).Invariant μ

Tactic:
Subsingleton.elim _ _

Premises used: ProbabilityTheory.Kernel.Invariant, Subsingleton.elim
-- Module: Mathlib.Probability.Kernel.Invariance
Goal:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
h : IsEmpty α
⊢ (κ ∘ₖ η).Invariant μ

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Probability.Kernel.Invariance
Goal:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
inr : (⇑(κ ∘ₖ η) : (a : α) → Measure α) ∘ₘ μ = μ
inr₁ : Measure.bind (α := α) (mα := mα) ((⇑η : (a : α) → Measure α) ∘ₘ μ) (⇑κ : (a : α) → Measure α) = μ
inr₂ : (⇑κ : (a : α) → Measure α) ∘ₘ μ = μ
inr₃ inr₄ : μ = μ
⊢ (κ ∘ₖ η).Invariant μ

Tactic:
rw [Invariant, ← Measure.comp_assoc, hη, hκ]

Premises used: ProbabilityTheory.Kernel.Invariant, MeasureTheory.Measure.comp_assoc
-- Module: Mathlib.Probability.Kernel.Invariance
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((π : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.Invariant π

Tactic:
ext s hs