awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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)
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 γ)
⊢ 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:
refine Measurable.div ?_ ?_

Premises used: Measurable.div
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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)

Tactic:
measurable_from_prod_countable_left (fun t ↦ ?_)

Premises used: measurable_from_prod_countable_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 :
  ∀ (t : (↑(countablePartition γ n) : Type u_3)),
    Measurable (β := ℝ≥0∞) fun (x : α) ↦
      (((κ : (a : α) → Measure (γ × β)) (x, t).1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        ((↑(x, t).2 : Set γ) ×ˢ 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)

Tactic:
refine measurable_from_prod_countable_left (fun t ↦ ?_)

Premises used: measurable_from_prod_countable_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
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:
Kernel.measurable_coe _ ((measurableSet_countablePartition _ t.prop).prod hs)

Premises used: MeasurableSet.prod, Subtype.prop, ProbabilityTheory.Kernel.measurable_coe, MeasurableSpace.measurableSet_countablePartition
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
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:
exact Kernel.measurable_coe _ ((measurableSet_countablePartition _ t.prop).prod hs)

Premises used: MeasurableSet.prod, Subtype.prop, ProbabilityTheory.Kernel.measurable_coe, MeasurableSpace.measurableSet_countablePartition
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 γ)

Tactic:
measurable_from_prod_countable_left ?_

Premises used: measurable_from_prod_countable_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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_2 :
  ∀ (y : (↑(countablePartition γ n) : Type u_3)),
    Measurable (β := ℝ≥0∞) fun (x : α) ↦
      (((ν : (a : α) → Measure γ) (x, y).1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑(x, y).2 : Set γ)
⊢ 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_from_prod_countable_left ?_

Premises used: measurable_from_prod_countable_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
t : Set γ
ht : t ∈ countablePartition γ n
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (((ν : (a : α) → Measure γ) (x, Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) t ht).1 :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      (↑(x, Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) t ht).2 : Set γ)

Tactic:
Kernel.measurable_coe _ (measurableSet_countablePartition _ ht)

Premises used: ProbabilityTheory.Kernel.measurable_coe, MeasurableSpace.measurableSet_countablePartition
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
t : Set γ
ht : t ∈ countablePartition γ n
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (((ν : (a : α) → Measure γ) (x, Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) t ht).1 :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      (↑(x, Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) t ht).2 : Set γ)

Tactic:
exact Kernel.measurable_coe _ (measurableSet_countablePartition _ ht)

Premises used: ProbabilityTheory.Kernel.measurable_coe, MeasurableSpace.measurableSet_countablePartition
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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∞)

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)
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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) ⋯))

Tactic:
h1.comp (measurable_fst.prodMk ?_)

Premises used: Measurable.comp, Measurable.prodMk, measurable_fst
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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∞)
refine :
  Measurable (β := (↑(countablePartition γ n) : Type u_3)) fun (p : α × γ) ↦
    Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) (countablePartitionSet n p.2) ⋯
⊢ 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) ⋯))

Tactic:
refine h1.comp (measurable_fst.prodMk ?_)

Premises used: Measurable.comp, Measurable.prodMk, measurable_fst
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 (α := α × γ) (β := (↑(countablePartition γ n) : Type u_3))
    ((fun (c : γ) ↦ Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) (countablePartitionSet n c) ⋯) ∘
      fun (p : α × γ) ↦ p.2)

Tactic:
(measurable_countablePartitionSet_subtype n ⊤).comp measurable_snd

Premises used: Measurable.comp, ProbabilityTheory.measurable_countablePartitionSet_subtype, measurable_snd, Top.top
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 (α := α × γ) (β := (↑(countablePartition γ n) : Type u_3))
    ((fun (c : γ) ↦ Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) (countablePartitionSet n c) ⋯) ∘
      fun (p : α × γ) ↦ p.2)

Tactic:
exact (measurable_countablePartitionSet_subtype n ⊤).comp measurable_snd

Premises used: Measurable.comp, ProbabilityTheory.measurable_countablePartitionSet_subtype, measurable_snd, Top.top
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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∞)

Tactic:
Measurable.mono (measurable_densityProcess_countableFiltration_aux κ ν n hs) ?_ le_rfl

Premises used: le_rfl, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, Measurable.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : mα.prod ((↑(countableFiltration γ) : ℕ → MeasurableSpace γ) n) ≤ Prod.instMeasurableSpace
⊢ 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∞)

Tactic:
refine Measurable.mono (measurable_densityProcess_countableFiltration_aux κ ν n hs) ?_ le_rfl

Premises used: le_rfl, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, Measurable.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
⊢ mα.prod ((↑(countableFiltration γ) : ℕ → MeasurableSpace γ) n) ≤ Prod.instMeasurableSpace

Tactic:
sup_le_sup le_rfl (comap_mono ((countableFiltration γ).le _))

Premises used: MeasurableSpace.comap_mono, sup_le_sup, le_rfl, ProbabilityTheory.countableFiltration, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
⊢ mα.prod ((↑(countableFiltration γ) : ℕ → MeasurableSpace γ) n) ≤ Prod.instMeasurableSpace

Tactic:
exact sup_le_sup le_rfl (comap_mono ((countableFiltration γ).le _))

Premises used: MeasurableSpace.comap_mono, sup_le_sup, le_rfl, ProbabilityTheory.countableFiltration, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 (β := ℝ) fun (p : α × γ) ↦ κ.densityProcess ν n p.1 p.2 s

Tactic:
(measurable_densityProcess_aux κ ν n hs).ennreal_toReal

Premises used: ProbabilityTheory.Kernel.densityProcess, ProbabilityTheory.Kernel.measurable_densityProcess_aux, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
x : γ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ) fun (a : α) ↦ κ.densityProcess ν n a x s

Tactic:
((measurable_densityProcess κ ν n hs).comp (measurable_id.prodMk measurable_const) :)

Premises used: Measurable.comp, measurable_id, ProbabilityTheory.Kernel.measurable_densityProcess, Measurable.prodMk, ProbabilityTheory.Kernel.densityProcess, ENNReal.toReal, measurable_const, NNReal.toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
a : α
hs : MeasurableSet s
⊢ Measurable (β := ℝ) fun (x : γ) ↦ κ.densityProcess ν n a x s

Tactic:
((measurable_densityProcess κ ν n hs).comp (measurable_const.prodMk measurable_id) :)

Premises used: Measurable.comp, measurable_id, ProbabilityTheory.Kernel.measurable_densityProcess, Measurable.prodMk, ProbabilityTheory.Kernel.densityProcess, ENNReal.toReal, measurable_const, NNReal.toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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

Tactic:
@Measurable.ennreal_toReal _ (countableFiltration γ n) _ ?_

Premises used: ProbabilityTheory.Kernel.densityProcess, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
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∞)
⊢ Measurable (β := ℝ) fun (x : γ) ↦ κ.densityProcess ν n a x s

Tactic:
refine @Measurable.ennreal_toReal _ (countableFiltration γ n) _ ?_

Premises used: Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 (β := ℝ≥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:
((measurable_densityProcess_countableFiltration_aux κ ν n hs).comp measurable_prodMk_left :)

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 (β := ℝ≥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:
exact ((measurable_densityProcess_countableFiltration_aux κ ν n hs).comp measurable_prodMk_left :)

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
⊢ StronglyMeasurable (β := ℝ) fun (x : γ) ↦ κ.densityProcess ν n a x s

Tactic:
(measurable_countableFiltration_densityProcess κ ν n a hs).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, ProbabilityTheory.Kernel.measurable_countableFiltration_densityProcess
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
a : α
s : Set β
hs : MeasurableSet s
⊢ StronglyAdapted (m := mγ) (β := fun (n : ℕ) ↦ ℝ) (countableFiltration γ) fun (n : ℕ) (x : γ) ↦
    κ.densityProcess ν n a x s

Tactic:
fun n ↦ stronglyMeasurable_countableFiltration_densityProcess κ ν n a hs

Premises used: MeasureTheory.StronglyAdapted, ProbabilityTheory.Kernel.stronglyMeasurable_countableFiltration_densityProcess
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
a : α
x : γ
s : Set β
⊢ 0 ≤ κ.densityProcess ν n a x s

Tactic:
ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, ProbabilityTheory.Kernel.densityProcess
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 β
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∞)
⊢ 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:
rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]

Premises used: MeasurableSpace.measurableSet_countablePartitionSet, ProbabilityTheory.Kernel.fst_apply'
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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∞)

Tactic:
measure_mono (fun x ↦ ?_)

Premises used: MeasureTheory.measure_mono