mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
⊢ iIndepFun (fun t ω s ↦ X t s ω) P

Tactic:
refine iIndepFun.iIndepFun_process₀ mX fun I J ↦
    HasGaussianLaw.iIndepFun_of_covariance_strongDual ?_ fun i j hij L₁ L₂ ↦ ?_

Goal state after:
case refine_1
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
⊢ HasGaussianLaw (fun ω i j ↦ X (↑i) (↑j) ω) P

case refine_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ (↥(J i) → E)
L₂ : StrongDual ℝ (↥(J j) → E)
⊢ cov[⇑L₁ ∘ fun ω j ↦ X (↑i) (↑j) ω, ⇑L₂ ∘ fun ω j_1 ↦ X (↑j) (↑j_1) ω; P] = 0
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen : MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX
⊢ IndepSets πX {s | MeasurableSet s} κ P

Tactic:
rintro - - ⟨-, ⟨I, s, hs, rfl⟩, rfl⟩ ⟨t, ht, rfl⟩

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen : MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
hs : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : Set 𝓨
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂P,
    (κ a) ((fun ω i ↦ X i ω) ⁻¹' (↑I).pi s ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X i ω) ⁻¹' (↑I).pi s) * (κ a) (Y ⁻¹' t)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' // y < ↑r' }
r : { q' // y < ↑q' }
u : { q' // x < ↑q' }
⊢ 0 ≤ (fun q ↦ f a ↑q) u

Tactic:
exact hf.nonneg a _

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

Goal state before:
pp: case refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
u : { r' // x < ↑r' }
⊢ 0 ≤ (fun r ↦ f a ↑r) u

Tactic:
exact hf.nonneg a _

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ↑(hf.stieltjesFunction a) x ≤ 1

Tactic:
obtain ⟨r, hrx⟩ := exists_rat_gt x
  rw [← StieltjesFunction.iInf_rat_gt_eq]
  simp_rw [IsMeasurableRatCDF.stieltjesFunction_eq]
  refine ciInf_le_of_le ?_ ?_ (hf.le_one _ _)
  · refine ⟨0, fun z ↦ ?_⟩; rintro ⟨u, rfl⟩; exact hf.nonneg a _
  · exact ⟨r, hrx⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑(-i)
i : ℚ
⊢ x.2 ≤ ↑i

Tactic:
have h' := h (-i)

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑(-i)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑(- -i)
⊢ x.2 ≤ ↑i
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑i
i : ℚ
⊢ x.2 ≤ ↑(-i)

Tactic:
have h' := h (-i)

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑i
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑(-i)
⊢ x.2 ≤ ↑(-i)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
this : ∀ (t : ℝ≥0) (ω : Ω), (√↑c)⁻¹ * B (c * t) ω = (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω
⊢ IsGaussianProcess (fun t ω ↦ (√↑c)⁻¹ * B (c * t) ω) P

Tactic:
simp_rw [this]

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
this : ∀ (t : ℝ≥0) (ω : Ω), (√↑c)⁻¹ * B (c * t) ω = (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω
⊢ IsGaussianProcess (fun t ω ↦ (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω) P
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
⊢ (ρ.IicSnd ↑q).real s = ρ.real (s ×ˢ Iic ↑q)

Tactic:
measureReal_def,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
⊢ ((ρ.IicSnd ↑q) s).toReal = ρ.real (s ×ˢ Iic ↑q)
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
⊢ ((ρ.IicSnd ↑q) s).toReal = ρ.real (s ×ˢ Iic ↑q)

Tactic:
measureReal_def,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
⊢ ((ρ.IicSnd ↑q) s).toReal = (ρ (s ×ˢ Iic ↑q)).toReal
Module: Mathlib.Probability.CDF

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

Tactic:
measureReal_def,

Goal state after:
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ↑(cdf μ) x = (μ (Iic x)).toReal
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 κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h : ∀ (r : ↑(Ioi q)), ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ (κ a).real (A ×ˢ Iic ↑↑r)
⊢ ⨅ r, (κ a).real (A ×ˢ Iic ↑↑r) = (κ a).real (A ×ˢ Iic ↑q)

Tactic:
measureReal_def,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h : ∀ (r : ↑(Ioi q)), ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ (κ a).real (A ×ˢ Iic ↑↑r)
⊢ ⨅ r, (κ a).real (A ×ˢ Iic ↑↑r) = ((κ a) (A ×ˢ Iic ↑q)).toReal
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P) =
      (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ TendstoInDistribution (fun n ω ↦ (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P))
    atTop Y (fun x ↦ P) P'

Tactic:
simp_rw [this]

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P) =
      (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ TendstoInDistribution (fun n ω ↦ (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) atTop Y
    (fun x ↦ P) P'
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:

Tactic:
(κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
    _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
    _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * (ρ.fst ⊗ₘ ρCond) ({x} ×ˢ s)

Tactic:
rw [Measure.compProd_apply (measurableSet_prod.mpr (Or.inl ⟨measurableSet_singleton x, hs⟩))]

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ∫⁻ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) ∂ρ.fst
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this✝ : IsSFiniteKernel ρCond
this : ∀ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) = {x}.indicator (fun x ↦ (ρCond x) s) a
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ∫⁻ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) ∂ρ.fst

Tactic:
simp_rw [this]

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this✝ : IsSFiniteKernel ρCond
this : ∀ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) = {x}.indicator (fun x ↦ (ρCond x) s) a
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ∫⁻ (a : α), {x}.indicator (fun x ↦ (ρCond x) s) a ∂ρ.fst
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: 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
⊢ ∀ᵐ (b : β) ∂κ.fst a, IsProbabilityMeasure (κCond (a, b))

pp: 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
⊢ ∀ᵐ (b : β) ∂κ.fst a, IsProbabilityMeasure (κCond (a, b))

Tactic:
· rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h_sfin] at h; simp [h.symm]

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
⊢ ∀ᵐ (b : β) ∂κ.fst a, IsProbabilityMeasure (κCond (a, b))
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
⊢ (κ a) (countablePartitionSet n x ×ˢ s) = 0

Tactic:
have h0' : fst κ a (countablePartitionSet n x) = 0 := by simpa using (hκν a _).trans h0.le

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' : (κ.fst a) (countablePartitionSet n x) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ s) = 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 : ℝ
q : ℚ
hq : ↑q < x
⊢ ∃ x_1, ↑(s x_1) < x

Tactic:
obtain ⟨i, hi⟩ := hs_tendsto q

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 : ℝ
q : ℚ
hq : ↑q < x
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → s a ≤ q
⊢ ∃ x_1, ↑(s x_1) < x
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 : ℝ
q : ℚ
hq : x < ↑q
⊢ ∃ i, x ∈ s' i

Tactic:
obtain ⟨i, hi⟩ := hs_tendsto q

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 : ℝ
q : ℚ
hq : x < ↑q
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → q ≤ s a
⊢ ∃ i, x ∈ s' i
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ρ.fst, (κ x) s = (ρ.condKernel x) s

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
    (Kernel.measurable_coe κ hs) (Kernel.measurable_coe ρ.condKernel hs) (fun t ht _ ↦ ?_)
  conv_rhs => rw [Measure.setLIntegral_condKernel_eq_measure_prod ht hs, hκ]
  exact (Measure.compProd_apply_prod ht hs).symm

Goal state after:
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ Measure.map (fun x ↦ (X x, (f ∘ Y) x)) μ = Measure.map X μ ⊗ₘ (condDistrib Y X μ).map f

Tactic:
calc μ.map (fun x ↦ (X x, (f ∘ Y) x))
  _ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    simp [Function.comp_def]
  _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by rw [compProd_map_condDistrib hY]
  _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := by rw [Measure.compProd_map hf]

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

Goal state before:
pp: case compl
α : 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
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s \ A ×ˢ s)

Tactic:
measureReal_def,

Goal state after:
case compl
α : 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
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s \ A ×ˢ s)).toReal
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ Measure.map (fun x ↦ (X x, (f ∘ X) x)) μ = Measure.map (fun a ↦ (a, f a)) (Measure.map X μ)

Tactic:
AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX

Goal state after:
case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ Measure.map (fun x ↦ (X x, (f ∘ X) x)) μ = Measure.map ((fun a ↦ (a, f a)) ∘ X) μ
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
this : Measure.map (Prod.map id f) ρ = ρ.fst ⊗ₘ ρ.condKernel.map f
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ (s : Set ℝ), MeasurableSet s → (ρ'.condKernel x) s = (ρ.condKernel x) (f ⁻¹' s)

Tactic:
by
    rw [← hρ'] at this
    have heq := eq_condKernel_of_measure_eq_compProd_real _ this
    rw [hρ'] at heq
    filter_upwards [heq] with x hx s hs
    rw [← hx, Kernel.map_apply _ hf.measurable, Measure.map_apply hf.measurable hs]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ ⇑(μ ⊗ₘ κ).condKernel =ᵐ[μ] ⇑κ

Tactic:
suffices κ =ᵐ[(μ ⊗ₘ κ).fst] (μ ⊗ₘ κ).condKernel by symm; rwa [Measure.fst_compProd] at this
  refine eq_condKernel_of_measure_eq_compProd _ ?_
  rw [Measure.fst_compProd]

Goal state after:
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ ∀ᵐ (b : β) ∂Measure.map X μ, Integrable (fun ω ↦ f (b, ω)) ((condDistrib Y X μ) b)

Tactic:
rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]; exact hf_int.condKernel_ae

Goal state after: