awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (p : α × γ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n p.2 ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n p.2) : ℝ≥0∞)
have change : Measurable (α := α × γ) (β := ℝ≥0∞)
  ((fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ) : ℝ≥0∞)) ∘
    fun (p : α × γ) ↦
    (p.1, Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) (countablePartitionSet n p.2) sorry))
Tactic: change Measurable[mα.prod (countableFiltration γ n)]
      ((fun (p : α × countablePartition γ n) ↦ κ p.1 (↑p.2 ×ˢ s) / ν p.1 p.2)
        ∘ (fun (p : α × γ) ↦ (p.1, ⟨countablePartitionSet n p.2, countablePartitionSet_mem n p.2⟩)))
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ) : ℝ≥0∞)
have refine_1 : Measurable (β := ℝ≥0∞) fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
  (((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s)
Tactic: refine Measurable.div ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
refine_1 :
  Measurable (β := ℝ≥0∞) fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
    (((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s)
⊢ Measurable (β := ℝ≥0∞) fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ) : ℝ≥0∞)
have refine_2 : Measurable (β := ℝ≥0∞) fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
  (((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ)
Tactic: refine Measurable.div ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
    (((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s)
have refine_1 : ∀ (t : (↑(countablePartition γ n) : Type u_3)),
  Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (((κ : (a : α) → Measure (γ × β)) (x, t).1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑(x, t).2 : Set γ) ×ˢ s)
Tactic: refine measurable_from_prod_countable_left (fun t ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
    (((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ)
have refine_2 : ∀ (y : (↑(countablePartition γ n) : Type u_3)),
  Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (((ν : (a : α) → Measure γ) (x, y).1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑(x, y).2 : Set γ)
Tactic: refine measurable_from_prod_countable_left ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ Measurable (α := α × γ) (β := ℝ≥0∞)
    ((fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ) : ℝ≥0∞)) ∘
      fun (p : α × γ) ↦
      (p.1, Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) (countablePartitionSet n p.2) ⋯))
have h1 : Measurable (β := ℝ≥0∞) fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s) : ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ) : ℝ≥0∞)
Tactic: have h1 : @Measurable _ _ (mα.prod ⊤) _
      (fun p : α × countablePartition γ n ↦ κ p.1 (↑p.2 ×ˢ s) / ν p.1 p.2) := by
    refine Measurable.div ?_ ?_
    · refine measurable_from_prod_countable_left (fun t ↦ ?_)
      exact Kernel.measurable_coe _ ((measurableSet_countablePartition _ t.prop).prod hs)
    · refine measurable_from_prod_countable_left ?_
      rintro ⟨t, ht⟩
      exact Kernel.measurable_coe _ (measurableSet_countablePartition _ ht)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
h1 :
  Measurable (β := ℝ≥0∞) fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ) : ℝ≥0∞)
⊢ Measurable (α := α × γ) (β := ℝ≥0∞)
    ((fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ) : ℝ≥0∞)) ∘
      fun (p : α × γ) ↦
      (p.1, Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) (countablePartitionSet n p.2) ⋯))
have refine : Measurable (β := (↑(countablePartition γ n) : Type u_3)) fun (p : α × γ) ↦
  Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) (countablePartitionSet n p.2) sorry
Tactic: refine h1.comp (measurable_fst.prodMk ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (p : α × γ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n p.2 ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n p.2) : ℝ≥0∞)
have refine : mα.prod ((↑(countableFiltration γ) : ℕ → MeasurableSpace γ) n) ≤ Prod.instMeasurableSpace
Tactic: refine Measurable.mono (measurable_densityProcess_countableFiltration_aux κ ν n hs) ?_ le_rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ) fun (x : γ) ↦ κ.densityProcess ν n a x s
have refine : Measurable (β := ℝ≥0∞) fun (x : γ) ↦
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
Tactic: refine @Measurable.ennreal_toReal _ (countableFiltration γ n) _ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (countablePartitionSet n x ×ˢ s) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
      {p : γ × β | p.1 ∈ countablePartitionSet n x} :
    ℝ≥0∞)
Tactic: rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
have refine : ∀ x_1 ∈ countablePartitionSet n x ×ˢ s,
  Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ countablePartitionSet n x} x_1
Tactic: refine measure_mono (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x_1 : γ
s : Set β
x : γ × β
⊢ x ∈ countablePartitionSet n x_1 ×ˢ s →
    Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ countablePartitionSet n x_1} x
have simp : x.1 ∈ countablePartitionSet n x_1 → x.2 ∈ s → x.1 ∈ countablePartitionSet n x_1
Tactic: simp only [mem_prod, mem_setOf_eq, and_imp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
have calc : LE.le (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (countablePartitionSet n x ×ˢ s) :
    ℝ≥0∞)
  ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
Tactic: calc κ a (countablePartitionSet n x ×ˢ s)
    ≤ fst κ a (countablePartitionSet n x) := by
        rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]
        refine measure_mono (fun x ↦ ?_)
        simp only [mem_prod, mem_setOf_eq, and_imp]
        exact fun h _ ↦ h
  _ ≤ ν a (countablePartitionSet n x) := hκν a _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ κ.densityProcess ν n a x s ≤ 1
have refine : (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (countablePartitionSet n x ×ˢ s) ≤
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal 1)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
Tactic: refine ENNReal.toReal_le_of_le_ofReal zero_le_one (ENNReal.div_le_of_le_mul ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (countablePartitionSet n x ×ˢ s) ≤
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal 1)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (countablePartitionSet n x ×ˢ s) :
    ℝ≥0∞)
  ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
Tactic: rw [ENNReal.ofReal_one, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
have refine_1 : ∀ (x : γ), ‖κ.densityProcess ν n a x s‖ ≤ 1
Tactic: refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun x ↦ ?_))).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
refine_1 : ∀ (x : γ), ‖κ.densityProcess ν n a x s‖ ≤ 1
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
have refine_2 : HPow.hPow (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      (ENNReal.toReal 1)⁻¹ *
    ENNReal.ofReal 1 ≤
  (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
Tactic: refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun x ↦ ?_))).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) ((ν : (a : α) → Measure γ) a)
have rw : MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a)
Tactic: rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a)
have refine_1 : Measurable (β := ℝ) fun (x : γ) ↦ κ.densityProcess ν n a x s
Tactic: refine ⟨Measurable.aestronglyMeasurable ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
refine_1 : Measurable (β := ℝ) fun (x : γ) ↦ κ.densityProcess ν n a x s
⊢ MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a)
have refine_2 : @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) < ∞
Tactic: refine ⟨Measurable.aestronglyMeasurable ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) u) fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (u ×ˢ s)
have this : IsFiniteKernel κ
Tactic: have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) u) fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (u ×ˢ s)
have hu_meas : MeasurableSet u
Tactic: have hu_meas : MeasurableSet u := measurableSet_countablePartition n hu
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) u) fun (x : γ) ↦
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n x ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) :
            ℝ≥0∞)).toReal) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (u ×ˢ s)
have rw : (∫⁻ (a_1 : γ) in u,
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n a_1 ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n a_1) :
          ℝ≥0∞) ∂(ν : (a : α) → Measure γ) a).toReal =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (u ×ˢ s)
Tactic: rw [integral_toReal]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
rw :
  (∫⁻ (a_1 : γ) in u,
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n a_1 ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n a_1) :
            ℝ≥0∞) ∂(ν : (a : α) → Measure γ) a).toReal =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (u ×ˢ s)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) u) fun (x : γ) ↦
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n x ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) :
            ℝ≥0∞)).toReal) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (u ×ˢ s)
have hfm : AEMeasurable (β := ℝ≥0∞) (_m := mγ)
  (fun (x : γ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
  (Measure.restrict ((ν : (a : α) → Measure γ) a) u)
Tactic: rw [integral_toReal]