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

Goal state before:
pp: case hp
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ 0 ≤ ∫ (b : β) in s, ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a

Tactic:
exact setIntegral_nonneg hs (fun _ _ ↦ stieltjesOfMeasurableRat_nonneg _ _ _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ENNReal.ofReal (∫ (b : β) in s, ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a) = (κ a) (s ×ˢ Iic x)

Tactic:
rw [ofReal_integral_eq_lintegral_ofReal, setLIntegral_stieltjesOfMeasurableRat hf _ _ hs]

Goal state after:
case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ((ν a).restrict s)

case f_nn
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ 0 ≤ᵐ[(ν a).restrict s] fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ Tendsto (fun i ↦ ∫ (a_1 : β), f (a, a_1) (seq i) ∂ν a) atTop (𝓝 (∫ (a : β), 0 ∂ν a))

pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ᵐ (a_1 : β) ∂ν a, Antitone fun i ↦ f (a, a_1) (seq i)

pp: case refine_4
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ᵐ (a_1 : β) ∂ν a, ∀ (i : ℕ), 0 ≤ f (a, a_1) (seq i)

Tactic:
· rw [integral_zero]
    exact hf.tendsto_integral_of_antitone a seq hseq hseq_tendsto

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ᵐ (a_1 : β) ∂ν a, Antitone fun i ↦ f (a, a_1) (seq i)

case refine_4
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ᵐ (a_1 : β) ∂ν a, ∀ (i : ℕ), 0 ≤ f (a, a_1) (seq i)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
⊢ ∀ᵐ (x : β) ∂ν a, ‖⨅ r, f (a, x) ↑r‖ ≤ 1

Tactic:
filter_upwards [hf.bddBelow_range a, hf.nonneg a, hf.le_one a]
    with t hbdd_below h_nonneg h_le_one

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ ‖⨅ r, f (a, t) ↑r‖ ≤ 1
Module: Mathlib.Probability.CDF

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ENNReal.ofReal (↑(cdf μ) x) = μ (Iic x)

Tactic:
by
  have h := lintegral_condCDF ((dirac Unit.unit).prod μ) x
  simpa only [fst_prod, prod_prod, measure_univ, one_mul, lintegral_dirac] using! h

Goal state after:
Module: Mathlib.Probability.CDF

Goal state before:
pp: μ : Measure ℝ
⊢ IsProbabilityMeasure (cdf μ).measure

Tactic:
constructor
  simp only [StieltjesFunction.measure_univ _ (tendsto_cdf_atBot μ) (tendsto_cdf_atTop μ), sub_zero,
    ENNReal.ofReal_one]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
⊢ ∃ m f,
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ (E × F)),
        charFunDual (Measure.map (fun ω ↦ (X ω, Y ω)) P) L = cexp (↑(L m) * I - ↑((f L) L) / 2)

Tactic:
refine ⟨(∫ x, x ∂P.map X, ∫ y, y ∂P.map Y),
      .diagonalStrongDualProd (covarianceBilinDual (P.map X)) (covarianceBilinDual (P.map Y)),
      isPosSemidef_diagonalStrongDualProd isPosSemidef_covarianceBilinDual
        isPosSemidef_covarianceBilinDual, fun L ↦ ?_⟩

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
⊢ charFunDual (Measure.map (fun ω ↦ (X ω, Y ω)) P) L =
    cexp
      (↑(L (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P)) * I -
        ↑((((covarianceBilinDual (Measure.map X P)).diagonalStrongDualProd (covarianceBilinDual (Measure.map Y P))) L)
              L) /
          2)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
⊢ ∀ (s : Set β), MeasurableSet s → (ν a) s < ∞ → ∫ (x : β) in s, ⨅ r, f (a, x) ↑r ∂ν a = ∫ (x : β) in s, f (a, x) q ∂ν a

Tactic:
intro s hs _

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
a✝ : (ν a) s < ∞
⊢ ∫ (x : β) in s, ⨅ r, f (a, x) ↑r ∂ν a = ∫ (x : β) in s, f (a, x) q ∂ν 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 ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫ (b : β), ↑(f (a, b)) x ∂ν a = ∫ (b : β) in univ, ↑(f (a, b)) x ∂ν a

Tactic:
Measure.restrict_univ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫ (b : β), ↑(f (a, b)) x ∂ν a = ∫ (b : β), ↑(f (a, b)) x ∂ν a
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
inst✝ : IsFiniteKernel κ
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫⁻ (b : β), ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = ∫⁻ (b : β) in univ, ENNReal.ofReal (↑(f (a, b)) x) ∂ν a

Tactic:
Measure.restrict_univ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
inst✝ : IsFiniteKernel κ
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫⁻ (b : β), ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = ∫⁻ (b : β), ENNReal.ofReal (↑(f (a, b)) x) ∂ν a
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : 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
b : β
⊢ s.indicator (fun x ↦ r) b ≤ s.indicator (fun b ↦ (κCond (a, b)) univ) b

Tactic:
by_cases hbs : b ∈ s

Goal state after:
case pos
α : 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
b : β
hbs : b ∈ s
⊢ s.indicator (fun x ↦ r) b ≤ s.indicator (fun b ↦ (κCond (a, b)) univ) b

case neg
α : 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
b : β
hbs : b ∉ s
⊢ s.indicator (fun x ↦ r) b ≤ s.indicator (fun b ↦ (κCond (a, b)) univ) b
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (fun ω ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[⇑L₁ ∘ X, ⇑L₂ ∘ Y; P] = 0
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this : (⇑L ∘ fun ω ↦ (X ω, Y ω)) = ⇑(L ∘SL inl ℝ E F) ∘ X + ⇑(L ∘SL inr ℝ E F) ∘ Y
⊢ Integrable (⇑(L ∘SL inr ℝ E F) ∘ Y) P

Tactic:
exact (hXY.snd.map _).integrable

Goal state after:
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 : α
q r : ℚ
hqr : q ≤ r
c : γ
⊢ ↑q ≤ ↑r

Tactic:
exact_mod_cast hqr

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

Goal state before:
pp: α : 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 : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
b : β
⊢ s.indicator (fun b ↦ (κCond (a, b)) univ) b ≤ s.indicator (fun x ↦ r) b

Tactic:
by_cases hbs : b ∈ s

Goal state after:
case pos
α : 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 : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
b : β
hbs : b ∈ s
⊢ s.indicator (fun b ↦ (κCond (a, b)) univ) b ≤ s.indicator (fun x ↦ r) b

case neg
α : 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 : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
b : β
hbs : b ∉ s
⊢ s.indicator (fun b ↦ (κCond (a, b)) univ) b ≤ s.indicator (fun x ↦ r) b
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 : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
⊢ ⋃ i, s' i = univ

Tactic:
· ext x
      simp only [mem_iUnion, mem_univ, iff_true]
      rw [tendsto_atTop_atTop] at hs_tendsto
      have ⟨q, hq⟩ := exists_rat_gt x
      obtain ⟨i, hi⟩ := hs_tendsto q
      refine ⟨i, hq.le.trans ?_⟩
      exact mod_cast hi i le_rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Tactic:
Measure.restrict_univ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Tactic:
Measure.restrict_univ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) (κ a)
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫ (b : β) in s, ∫ (ω : Ω) in Set.univ, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Tactic:
Measure.restrict_univ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) (κ a)
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a

Tactic:
rw [← setIntegral_condKernel a hs MeasurableSet.univ hf]; simp_rw [Measure.restrict_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫ (b : β) in Set.univ, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Tactic:
Measure.restrict_univ

Goal state after:
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

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, forall_exists_index, forall_apply_eq_imp_iff]
    exact ae_all_iff.2 fun q ↦ eq_condKernel_of_measure_eq_compProd' κ hκ measurableSet_Iic

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

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Tactic:
Measure.restrict_univ

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

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Tactic:
Measure.restrict_univ

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

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫ (b : β) in s, ∫ (ω : Ω) in Set.univ, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Tactic:
Measure.restrict_univ

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 ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ eLpNorm (fun x ↦ κ.densityProcess ν n a x s) 1 (ν a) ≤ ↑((ν a) univ).toNNReal

Tactic:
refine (eLpNorm_densityProcess_le hκν n a s).trans_eq ?_

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 ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ (ν a) univ = ↑((ν a) univ).toNNReal
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) ρ
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫ (b : β) in Set.univ, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Tactic:
Measure.restrict_univ

Goal state after:
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 β
X' : α → β
hX : X =ᵐ[μ] X'
⊢ Y =ᵐ[μ] Y

Tactic:
by rfl

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 ≤ ν
a : α
x : γ
s : Set β
⊢ 0 ≤ κ.density ν a x s

Tactic:
by
  refine le_limsup_of_frequently_le ?_ ?_
  · exact Frequently.of_forall (fun n ↦ densityProcess_nonneg _ _ _ _ _ _)
  · exact isBoundedUnder_of ⟨1, fun n ↦ densityProcess_le_one hκν _ _ _ _⟩

Goal state after:
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 β
Y' : α → Ω
hY : Y =ᵐ[μ] Y'
⊢ X =ᵐ[μ] X

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[ρ.fst] ⇑ρ.condKernel

Tactic:
have h := Kernel.condKernel_apply_eq_condKernel (Kernel.const α ρ) a

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
h : (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[(Kernel.const α ρ).fst a] ⇑((Kernel.const α ρ) a).condKernel
⊢ (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[ρ.fst] ⇑ρ.condKernel