awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ ∫⁻ (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)
have h : ∀
  (h₀ :
    Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      (0 : ENNReal)),
  ∫⁻ (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: rcases ((η ∘ₖ κ) a).zero_one s with (h₀ | h₁)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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 :
  ∀
    (h₀ :
      Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
        (0 : ENNReal)),
    ∫⁻ (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)
⊢ ∫⁻ (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)
have h₁ : ∀
  (h₁ :
    Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      (1 : ENNReal)),
  ∫⁻ (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: rcases ((η ∘ₖ κ) a).zero_one s with (h₀ | h₁)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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) (0 : ENNReal)
⊢ ∫⁻ (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)
have h : ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
  x ∈ t →
    Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: rw [h₀, zero_mul, setLIntegral_eq_zero_iff ht <| η.measurable_coe hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (hypothesis)
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) (0 : ENNReal)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    x ∈ t →
      Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)
have h₁ : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ENNReal)
  (fun (a : β) ↦ (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s) 0
Tactic: rw [comp_apply' _ _ _ hs, lintegral_eq_zero_iff <| η.measurable_coe hs] at h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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₀ :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ENNReal)
    (fun (a : β) ↦ (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s) 0
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    x ∈ t →
      Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)
have h : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Eq (α := ENNReal)
                  ((fun (a : β) ↦ ((((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)) x)
                  (0 x))
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                x ∈ t →
                  Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
                    (0 : ENNReal))
              x}
          x}
    a
Tactic: filter_upwards [h₀] with x hx _ using hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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₀ :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ENNReal)
    (fun (a : β) ↦ (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s) 0
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ENNReal)
                    ((fun (a : β) ↦ ((((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal))
                      x)
                    (0 x))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  x ∈ t →
                    Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
                      (0 : ENNReal))
                x}
            x}
      a
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    x ∈ t →
      Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)
have h₁ : ∀ (a : β),
  Eq (α := ENNReal) ((((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 a : ENNReal) →
    a ∈ t →
      Eq (α := ENNReal) ((((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: filter_upwards [h₀] with x hx _ using hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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)
⊢ ∫⁻ (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)
have h : ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
Tactic: rw [h₁, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
have refine : LE.le.{u_2} (α := β → ENNReal) (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s)
  fun (a : β) ↦ 1
Tactic: refine lintegral_mono ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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 : β) ↦ (1 : ENNReal)) b)
have 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)
Tactic: rw [← measure_univ (μ := η b)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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)
⊢ ∫⁻ (a : β) in t, 1 ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
have rw : Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
Tactic: rw [setLIntegral_one]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
have _ : ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
  ∫⁻ (a : β) in t, 1 ∂(κ : (a : α) → Measure β) a
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
have _₁ : ∫⁻ (a : β) in t, 1 ∂(κ : (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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (hypothesis)
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)
⊢ ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
have 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
Tactic: refine le_antisymm integral_le_kernel <| tsub_eq_zero_iff_le.mp ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ 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
have 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
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ 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
have 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)
Tactic: rw [setLIntegral_one]