awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
h :
  ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
⊢ ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)

Tactic:
rw [h₁, one_mul]

Premises used: one_mul
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    ∫⁻ (a : β) in t, 1 ∂(κ : (a : α) → Measure β) a

Tactic:
lintegral_mono ?_

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
refine :
  LE.le.{u_2} (α := β → ENNReal) (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s)
    fun (a : β) ↦ 1
⊢ ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    ∫⁻ (a : β) in t, 1 ∂(κ : (a : α) → Measure β) a

Tactic:
refine lintegral_mono ?_

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
b : β
rw :
  LE.le (α := (fun (a : β) ↦ ENNReal) b)
    ((fun (b : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)) b)
    ((fun (a : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) univ : ENNReal)) b)
⊢ LE.le (α := (fun (a : β) ↦ ENNReal) b)
    ((fun (b : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)) b)
    ((fun (a : β) ↦ (1 : ENNReal)) b)

Tactic:
rw [← measure_univ (μ := η b)]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
b : β
⊢ s ⊆ univ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
b : β
⊢ LE.le (α := (fun (a : β) ↦ ENNReal) b)
    ((fun (b : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)) b)
    ((fun (a : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) univ : ENNReal)) b)

Tactic:
exact measure_mono (by simp)

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
rw rw₁ :
  Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
⊢ ∫⁻ (a : β) in t, 1 ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t

Tactic:
rw [setLIntegral_one]

Premises used: MeasureTheory.setLIntegral_one
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
_ :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    ∫⁻ (a : β) in t, 1 ∂(κ : (a : α) → Measure β) a
_₁ :
  ∫⁻ (a : β) in t, 1 ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
⊢ ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t

Tactic:
calc
      _ ≤ ∫⁻ a in t, 1 ∂κ a := by
        refine lintegral_mono ?_
        intro b
        rw [← measure_univ (μ := η b)]
        exact measure_mono (by simp)
      _ = κ a t := by rw [setLIntegral_one]

Premises used: DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t

Tactic:
have integral_le_kernel : ∫⁻ b in t, (η b) s ∂κ a ≤ κ a t := by
      calc
      _ ≤ ∫⁻ a in t, 1 ∂κ a := by
        refine lintegral_mono ?_
        intro b
        rw [← measure_univ (μ := η b)]
        exact measure_mono (by simp)
      _ = κ a t := by rw [setLIntegral_one]
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
⊢ ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t

Tactic:
le_antisymm integral_le_kernel <| tsub_eq_zero_iff_le.mp ?_

Premises used: tsub_eq_zero_iff_le, le_antisymm, Iff.mp
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
h :
  HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) =
    0
⊢ ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t

Tactic:
refine le_antisymm integral_le_kernel <| tsub_eq_zero_iff_le.mp ?_

Premises used: tsub_eq_zero_iff_le, le_antisymm, Iff.mp
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
h :
  HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) ≤
    0
⊢ HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) =
    0

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
rw rw₁ :
  HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) =
    HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a)
⊢ HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) =
    ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
      ∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a

Tactic:
rw [setLIntegral_one]

Premises used: MeasureTheory.setLIntegral_one
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
hg : Measurable (β := ENNReal) fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s
hg_fin :
  ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≠
    ⊤
h_le :
  (ae (F := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) t)).EventuallyLE (β := ENNReal)
    (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) fun (b : β) ↦ 1
⊢ ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
      ∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in t,
      HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [lintegral_sub]

Premises used: MeasureTheory.lintegral_sub
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
⊢ Measurable (β := ENNReal) fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s

Tactic:
η.measurable_coe hs

Premises used: ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
⊢ Measurable (β := ENNReal) fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s

Tactic:
exact η.measurable_coe hs

Premises used: ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
⊢ Ne (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal) (⊤ : ENNReal)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
⊢ ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≠
    ⊤

Tactic:
exact ne_top_of_le_ne_top (by simp) integral_le_kernel

Premises used: ne_top_of_le_ne_top