mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
⊢ ∀ (b : ℝ≥0∞), 1 < b → (κ.fst a) {x | b ≤ (κCond (a, x)) univ} = 0

Tactic:
]

Goal state after:
case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
⊢ ∀ (b : ℝ≥0∞), 1 < b → (κ.fst a) {x | b ≤ (κCond (a, x)) univ} = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : 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) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)

Tactic:
]

Goal state after:
α : 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) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
h_le :
  (fun x ↦ ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t)) ≤ᵐ[ν a] fun x ↦
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ
⊢ ∫⁻ (a_1 : β), ((IsCondKernelCDF.toKernel f hf) (a, a_1)) univ ∂ν a -
      ∫⁻ (a_1 : β), ((IsCondKernelCDF.toKernel f hf) (a, a_1)) (Prod.mk a_1 ⁻¹' t) ∂ν a =
    ∫⁻ (x : β), ((IsCondKernelCDF.toKernel f hf) (a, x)) univ ∂ν a -
      ∫⁻ (x : β), ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t) ∂ν a

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
h_le :
  (fun x ↦ ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t)) ≤ᵐ[ν a] fun x ↦
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ
⊢ Measurable fun x ↦ ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t)

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
h_le :
  (fun x ↦ ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t)) ≤ᵐ[ν a] fun x ↦
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ
⊢ ∫⁻ (a_1 : β), ((IsCondKernelCDF.toKernel f hf) (a, a_1)) (Prod.mk a_1 ⁻¹' t) ∂ν a ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
h_le :
  (fun x ↦ ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t)) ≤ᵐ[ν a] fun x ↦
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ
⊢ Measurable fun x ↦ ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t)

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
h_le :
  (fun x ↦ ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t)) ≤ᵐ[ν a] fun x ↦
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ
⊢ ∫⁻ (a_1 : β), ((IsCondKernelCDF.toKernel f hf) (a, a_1)) (Prod.mk a_1 ⁻¹' t) ∂ν a ≠ ∞
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (fun x ↦ κ.densityProcess ν n a x s) 1 (ν a)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (fun x ↦ κ.densityProcess ν n a x s) 1 (ν a)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
h_le :
  (fun x ↦ ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t)) ≤ᵐ[ν a] fun x ↦
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ
⊢ (κ a) univ < ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
h_le :
  (fun x ↦ ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t)) ≤ᵐ[ν a] fun x ↦
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ
⊢ (κ a) univ < ∞
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : 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
⊢ (∫⁻ (a_1 : γ) in u, (κ a) (countablePartitionSet n a_1 ×ˢ s) / (ν a) (countablePartitionSet n a_1) ∂ν a).toReal =
    (κ a).real (u ×ˢ s)

pp: case hfm
α : 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
⊢ AEMeasurable (fun x ↦ (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)) ((ν a).restrict u)

pp: case hf
α : 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
⊢ ∀ᵐ (x : γ) ∂(ν a).restrict u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) < ∞

Tactic:
]

Goal state after:
α : 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
⊢ (∫⁻ (a_1 : γ) in u, (κ a) (countablePartitionSet n a_1 ×ˢ s) / (ν a) (countablePartitionSet n a_1) ∂ν a).toReal =
    (κ a).real (u ×ˢ s)

case hfm
α : 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
⊢ AEMeasurable (fun x ↦ (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)) ((ν a).restrict u)

case hf
α : 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
⊢ ∀ᵐ (x : γ) ∂(ν a).restrict u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) < ∞
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
⊢ (κ a) univ - (κ a) t = (κ a) univ - (κ a) t

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
h_2_le : (s.indicator fun x ↦ r) ≤ s.indicator fun b ↦ (κCond (a, b)) univ
this : r * (κ.fst a) s ≤ (κ.fst a) s
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0

Tactic:
]

Goal state after:
case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
h_2_le : (s.indicator fun x ↦ r) ≤ s.indicator fun b ↦ (κCond (a, b)) univ
this : r * (κ.fst a) s ≤ (κ.fst a) s
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : 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
x : γ
h0 : (ν a) (countablePartitionSet n x) = 0
h0' : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ s) = 0

Tactic:
]

Goal state after:
case pos
α : 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
x : γ
h0 : (ν a) (countablePartitionSet n x) = 0
h0' : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ s) = 0
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' f' i) ∂ν a = (κ a) (f' i)
h_eq : ∀ (a : β), Prod.mk a ⁻¹' ⋃ i, f' i = ⋃ i, Prod.mk a ⁻¹' f' i
h_disj : ∀ (a : β), Pairwise (Disjoint on fun i ↦ Prod.mk a ⁻¹' f' i)
x : β
⊢ ∑' (i : ℕ), ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' f' i) =
    ∑' (i : ℕ), ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' f' i)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : 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
t : γ
ht : t ∈ u
⊢ (κ a) (u ×ˢ s) / (ν a) u = (κ a) (u ×ˢ s) / (ν a) u

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
⊢ (ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω) ⟂ᵢ[P] ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
⊢ (ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω) ⟂ᵢ[P] ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : 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
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
⊢ ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a = (κ a) (u ×ˢ s)

Tactic:
]

Goal state after:
α : 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
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
⊢ ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a = (κ a) (u ×ˢ s)
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos.right
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
⊢ ∀ b < 1, (κ.fst a) {x | (κCond (a, x)) univ ≤ b} = 0

Tactic:
]

Goal state after:
case pos.right
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
⊢ ∀ b < 1, (κ.fst a) {x | (κCond (a, x)) univ ≤ b} = 0
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
hs : MeasurableSet s
⊢ (κ a) s = (κ a) s

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : 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
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
h0 : (ν a) u = 0
h0' : (κ a) {p | p.1 ∈ u} = 0
⊢ 0 = (κ a) (u ×ˢ s)

Tactic:
]

Goal state after:
case pos
α : 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
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
h0 : (ν a) u = 0
h0' : (κ a) {p | p.1 ∈ u} = 0
⊢ 0 = (κ a) (u ×ˢ s)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ cov[fun ω ↦
      ⟪∑ i, ((EuclideanSpace.basisFun ι ℝ).repr x).ofLp i • (EuclideanSpace.basisFun ι ℝ) i,
        (toLp 2 ∘ fun ω i ↦ X i ω) ω⟫,
      fun ω ↦
      ⟪∑ i, ((EuclideanSpace.basisFun κ ℝ).repr y).ofLp i • (EuclideanSpace.basisFun κ ℝ) i,
        (toLp 2 ∘ fun ω j ↦ Y j ω) ω⟫;
      P] =
    0

Tactic:
]

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ cov[fun ω ↦
      ⟪∑ i, ((EuclideanSpace.basisFun ι ℝ).repr x).ofLp i • (EuclideanSpace.basisFun ι ℝ) i,
        (toLp 2 ∘ fun ω i ↦ X i ω) ω⟫,
      fun ω ↦
      ⟪∑ i, ((EuclideanSpace.basisFun κ ℝ).repr y).ofLp i • (EuclideanSpace.basisFun κ ℝ) i,
        (toLp 2 ∘ fun ω j ↦ Y j ω) ω⟫;
      P] =
    0
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: case refine_2
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
x : ℝ
⊢ ∃ x_1, ↑(s x_1) < x

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
x : ℝ
⊢ ∃ x_1, ↑(s x_1) < x
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop
    (𝓝 ((κ a).real {p | p.1 ∈ univ}))

Tactic:
]

Goal state after:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop
    (𝓝 ((κ a).real {p | p.1 ∈ univ}))
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: case refine_2
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
x : ℝ
⊢ ∃ i, x ∈ s' i

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
x : ℝ
⊢ ∃ i, x ∈ s' i