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

Goal state before:
pp: case h_basic
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ t ∈ ⋃ a, {Iic ↑a}, (κ x) t = (ρ.condKernel x) t

pp: case h_compl
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ (t : Set ℝ), MeasurableSet t → (κ x) t = (ρ.condKernel x) t → (κ x) tᶜ = (ρ.condKernel x) tᶜ

pp: case h_union
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (f : ℕ → Set ℝ),
      Pairwise (Function.onFun Disjoint f) →
        (∀ (i : ℕ), MeasurableSet (f i)) →
          (∀ (i : ℕ), (κ x) (f i) = (ρ.condKernel x) (f i)) → (κ x) (⋃ i, f i) = (ρ.condKernel x) (⋃ i, f i)

Tactic:
·

Goal state after:
case h_basic
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ t ∈ ⋃ a, {Iic ↑a}, (κ x) t = (ρ.condKernel x) t
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case neg.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x) ≠ ∞

pp: case neg.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m ↦ (κ a) (countablePartitionSet n x ×ˢ seq m) / (ν a) (countablePartitionSet n x)) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x)))

Tactic:
·

Goal state after:
case neg.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x) ≠ ∞
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: case h_compl
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ (t : Set ℝ), MeasurableSet t → (κ x) t = (ρ.condKernel x) t → (κ x) tᶜ = (ρ.condKernel x) tᶜ

pp: case h_union
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (f : ℕ → Set ℝ),
      Pairwise (Function.onFun Disjoint f) →
        (∀ (i : ℕ), MeasurableSet (f i)) →
          (∀ (i : ℕ), (κ x) (f i) = (ρ.condKernel x) (f i)) → (κ x) (⋃ i, f i) = (ρ.condKernel x) (⋃ i, f i)

Tactic:
·

Goal state after:
case h_compl
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ (t : Set ℝ), MeasurableSet t → (κ x) t = (ρ.condKernel x) t → (κ x) tᶜ = (ρ.condKernel x) tᶜ
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd : ((κ'.fst ⊗ₖ η) a) (univ ×ˢ range e)ᶜ = 0
⊢ MeasurableSet (univ ×ˢ range e)ᶜ

pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd : (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' (univ ×ˢ range e)ᶜ)) =ᵐ[κ'.fst a] 0
⊢ ∀ᵐ (t : β) ∂κ'.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}

Tactic:
·

Goal state after:
case hs
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd : ((κ'.fst ⊗ₖ η) a) (univ ×ˢ range e)ᶜ = 0
⊢ MeasurableSet (univ ×ˢ range e)ᶜ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ∀ (i : ℕ), NullMeasurableSet (countablePartitionSet n x ×ˢ seq i) (κ a)

pp: case hm
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ Antitone fun m ↦ countablePartitionSet n x ×ˢ seq m

pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ∃ i, (κ a) (countablePartitionSet n x ×ˢ seq i) ≠ ∞

Tactic:
·

Goal state after:
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ∀ (i : ℕ), NullMeasurableSet (countablePartitionSet n x ×ˢ seq i) (κ a)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hm
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ Antitone fun m ↦ countablePartitionSet n x ×ˢ seq m

pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ∃ i, (κ a) (countablePartitionSet n x ×ˢ seq i) ≠ ∞

Tactic:
·

Goal state after:
case hm
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ Antitone fun m ↦ countablePartitionSet n x ×ˢ seq m
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ∃ i, (κ a) (countablePartitionSet n x ×ˢ seq i) ≠ ∞

Tactic:
·

Goal state after:
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ∃ i, (κ a) (countablePartitionSet n x ×ˢ seq i) ≠ ∞
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: case h_union
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (f : ℕ → Set ℝ),
      Pairwise (Function.onFun Disjoint f) →
        (∀ (i : ℕ), MeasurableSet (f i)) →
          (∀ (i : ℕ), (κ x) (f i) = (ρ.condKernel x) (f i)) → (κ x) (⋃ i, f i) = (ρ.condKernel x) (⋃ i, f i)

Tactic:
·

Goal state after:
case h_union
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (f : ℕ → Set ℝ),
      Pairwise (Function.onFun Disjoint f) →
        (∀ (i : ℕ), MeasurableSet (f i)) →
          (∀ (i : ℕ), (κ x) (f i) = (ρ.condKernel x) (f i)) → (κ x) (⋃ i, f i) = (ρ.condKernel x) (⋃ i, f i)
Module: Mathlib.Probability.Kernel.Disintegration.Density

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

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

Tactic:
·

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

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

Tactic:
·

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

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

pp: case refine_2.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (ε : ℝ),
    0 < ε →
      ∃ C,
        ∀ (i : ℕ),
          eLpNorm ({x | C ≤ ‖κ.densityProcess ν i a x s‖₊}.indicator fun x ↦ κ.densityProcess ν i a x s) 1 (ν a) ≤
            ENNReal.ofReal ε

Tactic:
·

Goal state after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (i : ℕ), AEStronglyMeasurable (fun x ↦ κ.densityProcess ν i a x s) (ν a)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (ε : ℝ),
    0 < ε →
      ∃ C,
        ∀ (i : ℕ),
          eLpNorm ({x | C ≤ ‖κ.densityProcess ν i a x s‖₊}.indicator fun x ↦ κ.densityProcess ν i a x s) 1 (ν a) ≤
            ENNReal.ofReal ε

Tactic:
·

Goal state after:
case refine_2.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (ε : ℝ),
    0 < ε →
      ∃ C,
        ∀ (i : ℕ),
          eLpNorm ({x | C ≤ ‖κ.densityProcess ν i a x s‖₊}.indicator fun x ↦ κ.densityProcess ν i a x s) 1 (ν a) ≤
            ENNReal.ofReal ε
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2.refine_2.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
⊢ eLpNorm ({x | 2 ≤ ‖κ.densityProcess ν n a x s‖₊}.indicator fun x ↦ κ.densityProcess ν n a x s) 1 (ν a) = 0

pp: case refine_2.refine_2.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
⊢ 0 ≤ ENNReal.ofReal ε

Tactic:
·

Goal state after:
case refine_2.refine_2.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
⊢ eLpNorm ({x | 2 ≤ ‖κ.densityProcess ν n a x s‖₊}.indicator fun x ↦ κ.densityProcess ν n a x s) 1 (ν a) = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2.refine_2.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
⊢ 0 ≤ ENNReal.ofReal ε

Tactic:
·

Goal state after:
case refine_2.refine_2.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
⊢ 0 ≤ ENNReal.ofReal ε
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ ((Measure.map (fun a ↦ (X a, Y a)) μ).fst {x})⁻¹ * (Measure.map (fun a ↦ (X a, Y a)) μ) ({x} ×ˢ s) =
    ((Measure.map X μ) {x})⁻¹ * (Measure.map (fun a ↦ (X a, Y a)) μ) ({x} ×ˢ s)

pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ (Measure.map (fun a ↦ (X a, Y a)) μ).fst {x} ≠ 0

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ ((Measure.map (fun a ↦ (X a, Y a)) μ).fst {x})⁻¹ * (Measure.map (fun a ↦ (X a, Y a)) μ) ({x} ×ˢ s) =
    ((Measure.map X μ) {x})⁻¹ * (Measure.map (fun a ↦ (X a, Y a)) μ) ({x} ×ˢ s)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ (Measure.map (fun a ↦ (X a, Y a)) μ).fst {x} ≠ 0

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ (Measure.map (fun a ↦ (X a, Y a)) μ).fst {x} ≠ 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ (fun n ↦ κ.densityProcess ν n a x s) ≤ᶠ[atTop] fun n ↦ κ.densityProcess ν n a x s'

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s'

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ (fun n ↦ κ.densityProcess ν n a x s) ≤ᶠ[atTop] fun n ↦ κ.densityProcess ν n a x s'
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s'

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s'

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s'