mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: case insert.mX
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s✝ : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
⊢ ∀ i ∈ s, AEMeasurable (X i) P

Tactic:
exact fun i hi ↦ (mX i (mem_insert_of_mem hi))

Goal state after:
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 X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (fun ω i ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : ↑I) → 𝓧 ↑i)
hI : I.Countable
hs : MeasurableSet (I.domRestrict ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P, (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u) * (κ a) (Y ⁻¹' t)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
x✝ : Countable ↑I
⊢ ∀ᵐ (a : α) ∂P, (fun ω i ↦ X (↑i) ω) =ᵐ[κ a] fun ω i ↦ X' (↑i) ω

Tactic:
filter_upwards [ae_all_iff.2 fun (i : I) ↦ h2 i] with
      a (ha : ∀ (i : I), ∀ᵐ ω ∂κ a, X i ω = X' i ω)

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 X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (fun ω i ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : ↑I) → 𝓧 ↑i)
hI : I.Countable
hs : MeasurableSet (I.domRestrict ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P, (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u) * (κ a) (Y ⁻¹' t)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
x✝ : Countable ↑I
a : α
ha : ∀ (i : ↑I), ∀ᵐ (ω : Ω) ∂κ a, X (↑i) ω = X' (↑i) ω
⊢ (fun ω i ↦ X (↑i) ω) =ᵐ[κ a] fun ω i ↦ X' (↑i) ω
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case hm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
⊢ ∫ (x : Ω), (PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm (I.restrict fun x_1 ↦ X x_1 x) ∂P =
    ∫ (x : ↥I → ℝ), (PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm x ∂projectiveFamily I

Tactic:
rw [ContinuousLinearEquiv.integral_comp_id_comm,
          ContinuousLinearEquiv.integral_comp_comm]

Goal state after:
case hm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
⊢ (PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm (∫ (x : Ω), I.restrict fun x_1 ↦ X x_1 x ∂P) =
    (PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm (∫ (x : ↥I → ℝ), x ∂projectiveFamily I)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case hm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
i : ↥I
⊢ (∫ (x : Ω), I.restrict fun x_1 ↦ X x_1 x ∂P) i = 0 i

Tactic:
eval_integral

Goal state after:
case hm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
i : ↥I
⊢ ∫ (x : Ω), I.restrict (fun x_1 ↦ X x_1 x) i ∂P = 0 i

case hm.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
i : ↥I
⊢ ∀ (i : ↥I), Integrable (fun x ↦ I.restrict (fun x_1 ↦ X x_1 x) i) P
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: t : ℚ
⊢ ⨅ r, defaultRatCDF ↑r = defaultRatCDF t

Tactic:
by
  simp only [defaultRatCDF]
  have h_bdd : BddBelow (range fun r : ↥(Ioi t) ↦ ite ((r : ℚ) < 0) (0 : ℝ) 1) := by
    refine ⟨0, fun x hx ↦ ?_⟩
    obtain ⟨y, rfl⟩ := mem_range.mpr hx
    dsimp only
    split_ifs
    exacts [le_rfl, zero_le_one]
  split_ifs with h
  · refine le_antisymm ?_ (le_ciInf fun x ↦ ?_)
    · obtain ⟨q, htq, hq_neg⟩ : ∃ q, t < q ∧ q < 0 := ⟨t / 2, by linarith, by linarith⟩
      refine (ciInf_le h_bdd ⟨q, htq⟩).trans ?_
      rw [if_pos]
      rwa [Subtype.coe_mk]
    · split_ifs
      exacts [le_rfl, zero_le_one]
  · refine le_antisymm ?_ ?_
    · refine (ciInf_le h_bdd ⟨t + 1, lt_add_one t⟩).trans ?_
      split_ifs
      exacts [zero_le_one, le_rfl]
    · refine le_ciInf fun x ↦ ?_
      rw [if_neg]
      rw [not_lt] at h ⊢
      exact h.trans (mem_Ioi.mp x.prop).le

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atBot atBot
x : ℝ
⊢ ↑(hf.stieltjesFunction a) x ≤ (f a ∘ qs) x

Tactic:
rw [Function.comp_apply, ← stieltjesFunction_eq hf]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atBot atBot
x : ℝ
⊢ ↑(hf.stieltjesFunction a) x ≤ ↑(hf.stieltjesFunction a) ↑(qs x)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ (f a ∘ qs) x ≤ ↑(hf.stieltjesFunction a) x

Tactic:
rw [Function.comp_apply, ← stieltjesFunction_eq hf]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ ↑(hf.stieltjesFunction a) ↑(qs x) ≤ ↑(hf.stieltjesFunction a) x
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case hbc
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ (L₁ (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F)) ⋯ ⋯ ⋯
    ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖x‖ * ‖inr ℝ E F‖ ≤ ‖x‖

Tactic:
norm_inr_le_one,

Goal state after:
case hbc
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ (L₁ (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F)) ⋯ ⋯ ⋯
    ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖x‖ * 1 ≤ ‖x‖
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ (hf.stieltjesFunction a).measure univ = ENNReal.ofReal 1

Tactic:
← sub_zero (1 : ℝ)

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ (hf.stieltjesFunction a).measure univ = ENNReal.ofReal (1 - 0)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case h₂
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ (L₁ (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F)) ⋯ ⋯ ⋯
    ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖y‖ * ‖inr ℝ E F‖ ≤ ‖y‖

Tactic:
norm_inr_le_one,

Goal state after:
case h₂
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ (L₁ (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F)) ⋯ ⋯ ⋯
    ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖y‖ * 1 ≤ ‖y‖
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
h : i < j
h1 : i.succ ≤ j.succ
h2 : i.castSucc ≤ j.succ
h3 : i.castSucc ≤ j.castSucc
⊢ ↑(t i.succ) - ↑(t i.succ) - ↑(min (t i.castSucc) (t j.succ)) + ↑(min (t i.castSucc) (t j.castSucc)) = 0

Tactic:
min_eq_left (ht h2),

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
h : i < j
h1 : i.succ ≤ j.succ
h2 : i.castSucc ≤ j.succ
h3 : i.castSucc ≤ j.castSucc
⊢ ↑(t i.succ) - ↑(t i.succ) - ↑(t i.castSucc) + ↑(min (t i.castSucc) (t j.castSucc)) = 0
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case e_a.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ ↑(∫ (ω : Ω), ∑ i, (L ∘SL single ℝ E i) (X i ω) ∂P) = ↑(∑ i, ∫ (ω : Ω), (L ∘SL single ℝ E i) (X i ω) ∂P)

Tactic:
integral_finsetSum _ fun i _ ↦ ((hX.eval i).map_fun _).integrable.ofReal

Goal state after:
case e_a.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ ↑(∑ i, ∫ (a : Ω), (L ∘SL single ℝ E i) (X i a) ∂P) = ↑(∑ i, ∫ (ω : Ω), (L ∘SL single ℝ E i) (X i ω) ∂P)
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 : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun n ↦ f (a, t) ↑n) atTop (𝓝 1)
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (f (a, t)) atTop (𝓝 1)

Tactic:
filter_upwards [this, hf.mono a] with t ht h_mono
    rw [tendsto_iff_tendsto_subseq_of_monotone h_mono tendsto_natCast_atTop_atTop]
    exact ht

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ (condCDF ρ a).measure univ = ENNReal.ofReal 1

Tactic:
← sub_zero (1 : ℝ)

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ (condCDF ρ a).measure univ = ENNReal.ofReal (1 - 0)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

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

Tactic:
· simpa using fun i ↦ ((hX.eval j).eval i).memLp_two.const_mul _

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case convert_7
Ω : 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]
⊢ ∫ (x : Ω), ((fun ω ↦ (X 0 ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) ^ 2) x ∂P = 1

Tactic:
simp only [Pi.pow_apply, div_pow]
    rw [integral_div, ← variance_eq_integral mX0, Real.sq_sqrt (variance_nonneg _ _), div_self hX]

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case convert_9
Ω : 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]
⊢ ∀ (i : ℕ),
    IdentDistrib (fun ω ↦ (X i ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P])
      (fun ω ↦ (X 0 ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) P P

Tactic:
convert! fun n ↦ (hident n).comp (u := fun x ↦ (x - P[X 0]) / √Var[X 0; P]) (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ ⇑(κ ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.swap β α) ∘ₘ ν.prod μ = ⇑(Kernel.swap β γ) ∘ₘ ⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ

Tactic:
rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]

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
s : Set β
hs : MeasurableSet s
| (κ.fst a) s

Tactic:
← h

Goal state after:
α : 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
s : Set β
hs : MeasurableSet s
| ((κ.fst ⊗ₖ κCond).fst a) s
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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
u v : ↥S
huv : u ≠ v
⊢ ¬↑u = ↑v

Tactic:
← Subtype.ext_iff

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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
u v : ↥S
huv : u ≠ v
⊢ ¬u = v
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) = ∞

Tactic:
ENNReal.div_eq_top

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 ×ˢ ∅) ≠ 0 ∧ (ν a) (countablePartitionSet n x) = 0 ∨
      (κ a) (countablePartitionSet n x ×ˢ ∅) = ∞ ∧ (ν a) (countablePartitionSet n x) ≠ ∞)
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:
· exact Eventually.of_forall (fun n ↦ densityProcess_mono_set hκν n a x h)

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

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'
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
⊢ Measurable fun x ↦ κ.density ν a x s

Tactic:
exact measurable_density_right κ ν hs a

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 α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : (κ.fst a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / 0).toReal = 0

Tactic:
by_cases h' : κ a (countablePartitionSet n x ×ˢ univ) = 0

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : (κ.fst a) (countablePartitionSet n x) = 0
h' : (κ a) (countablePartitionSet n x ×ˢ univ) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / 0).toReal = 0

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : (κ.fst a) (countablePartitionSet n x) = 0
h' : ¬(κ a) (countablePartitionSet n x ×ˢ univ) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / 0).toReal = 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 α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : (κ.fst a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)).toReal = 0

Tactic:
simp only [h]
    by_cases h' : κ a (countablePartitionSet n x ×ˢ univ) = 0
    · simp [h']
    · simp

Goal state after: