mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case neg.refine_1.left
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, xs n ∈ {t}ᶜ
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ Tendsto (fun n ↦ ↑(xs n)) atTop (𝓝 ↑t)

Tactic:
tendsto_ofReal_iff

Goal state after:
case neg.refine_1.left
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, xs n ∈ {t}ᶜ
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ Tendsto xs atTop (𝓝 t)
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
μ : Measure E
x y : E
⊢ ((covarianceBilinDual μ) ((toDualMap ℝ E) x)) ((toDualMap ℝ E) y) = ((covarianceBilin μ) y) x

Tactic:
covarianceBilinDual_comm,

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
μ : Measure E
x y : E
⊢ ((covarianceBilinDual μ) ((toDualMap ℝ E) y)) ((toDualMap ℝ E) x) = ((covarianceBilin μ) y) x
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : StrongDual ℝ E → ℤ
hn :
  ∀ (L : StrongDual ℝ E),
    ↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 =
      ↑(L m) * I - ↑((f L) L) / 2 + ↑(n L) * (2 * ↑π * I)
h :
  ∀ (L : StrongDual ℝ E),
    ↑(n L) =
      (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 - ↑(L m) * I + ↑((f L) L) / 2) /
        (2 * ↑π * I)
⊢ Continuous (Int.cast ∘ n)

Tactic:
change Continuous (fun L ↦ (n L : ℂ))

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : StrongDual ℝ E → ℤ
hn :
  ∀ (L : StrongDual ℝ E),
    ↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 =
      ↑(L m) * I - ↑((f L) L) / 2 + ↑(n L) * (2 * ↑π * I)
h :
  ∀ (L : StrongDual ℝ E),
    ↑(n L) =
      (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 - ↑(L m) * I + ↑((f L) L) / 2) /
        (2 * ↑π * I)
⊢ Continuous fun L ↦ ↑(n L)
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
⊢ Integrable (fun x ↦ rexp (C' * ‖x‖ ^ 2)) μ

Tactic:
have hε : 0 < ε := div_pos (by rwa [sub_pos]) (by positivity)

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
⊢ Integrable (fun x ↦ rexp (C' * ‖x‖ ^ 2)) μ
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hd
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < (1 - d).toReal

Tactic:
simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hd, true_and]
    finiteness

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

Goal state before:
pp: E : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : IsGaussian μ
⊢ IsGaussian (Measure.map id μ)

Tactic:
by rwa [Measure.map_id]

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
hst : ↑s ≤ ↑t
⊢ ↑s - ↑t ≤ ↑t - ↑s

Tactic:
grw [hst]

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝ : (i : ι) → InnerProductSpace ℝ (E i)
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun X P ↔
    ∀ (t : WithLp 2 ((x : ι) → E x)),
      charFun (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) P) t = ∏ i, charFun (Measure.map (X i) P) (t.ofLp i)

Tactic:
by
  rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFun_eq_pi_iff,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]

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
h : ∀ᵐ (a : α) ∂P, (fun ω i ↦ X (↑i) ω) =ᵐ[κ a] fun ω i ↦ X' (↑i) ω
a : α
ha1 : (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u) * (κ a) (Y ⁻¹' t)
ha2 : (fun ω i ↦ X (↑i) ω) =ᵐ[κ a] fun ω i ↦ X' (↑i) ω
⊢ (κ a) ((fun ω i ↦ X' (↑i) ω) ⁻¹' u ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X' (↑i) ω) ⁻¹' u) * (κ a) (Y ⁻¹' t)

Tactic:
refine .trans (measure_congr (ae_eq_set_inter (ha2.symm.preimage _) .rfl)) (ha1.trans ?_)

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
h : ∀ᵐ (a : α) ∂P, (fun ω i ↦ X (↑i) ω) =ᵐ[κ a] fun ω i ↦ X' (↑i) ω
a : α
ha1 : (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u) * (κ a) (Y ⁻¹' t)
ha2 : (fun ω i ↦ X (↑i) ω) =ᵐ[κ a] fun ω i ↦ X' (↑i) ω
⊢ (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u) * (κ a) (Y ⁻¹' t) = (κ a) ((fun ω i ↦ X' (↑i) ω) ⁻¹' u) * (κ a) (Y ⁻¹' t)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ

Tactic:
by_cases hμ_zero : μ = 0

Goal state after:
case pos
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : μ = 0
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ

case neg
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
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 α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) (⇑κ ∘ₘ P)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
⊢ iIndepFun (fun i ω j ↦ X i j ω) κ P

Tactic:
by
  refine process_congr ?_ (fun i j ↦ Measure.ae_ae_of_ae_comp (hX i j).ae_eq_mk.symm)
  refine iIndepFun_process (fun i j ↦ (hX i j).measurable_mk) fun I J ↦ ?_
  exact (h I J).process_congr (fun i j ↦ Measure.ae_ae_of_ae_comp (hX i j).ae_eq_mk)

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' : ⨅ r, stieltjesFunctionAux f a ↑r = ⨅ r, stieltjesFunctionAux f a ↑↑r
⊢ ⨅ r, stieltjesFunctionAux f a ↑↑r = ⨅ r, f a ↑r

Tactic:
congr with r

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' : ⨅ r, stieltjesFunctionAux f a ↑r = ⨅ r, stieltjesFunctionAux f a ↑↑r
r : { r' // x < ↑r' }
⊢ stieltjesFunctionAux f a ↑↑r = f a ↑r
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : 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
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
⊢ ∃ m f,
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ ((x : ι) → E x)),
        charFunDual (Measure.map (fun ω x ↦ X x ω) P) L = cexp (↑(L m) * I - ↑((f L) L) / 2)

Tactic:
classical
    refine ⟨fun i ↦ ∫ x, x ∂P.map (X i),
      .diagonalStrongDualPi (fun i ↦ covarianceBilinDual (P.map (X i))),
      isPosSemidef_diagonalStrongDualPi (fun _ ↦ isPosSemidef_covarianceBilinDual), fun L ↦ ?_⟩
    rw [(iIndepFun_iff_charFunDual_pi (by fun_prop)).1 hX2]
    simp only [← LinearMap.sum_single_apply E (fun i ↦ ∫ x, x ∂P.map (X i)), map_sum, ofReal_sum,
      sum_mul, diagonalStrongDualPi_apply, sum_div, ← sum_sub_distrib, exp_sum]
    congr with i
    rw [(hX1 i).isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
      covarianceBilinDual_self_eq_variance]
    · simp
    · exact (hX1 i).isGaussian_map.memLp_two_id
    · exact (hX1 i).isGaussian_map.integrable_id

Goal state after:
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) - ↑(t i.castSucc) + ↑(min (t i.castSucc) (t j.castSucc)) = 0

Tactic:
min_eq_left (ht h3)

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) + ↑(t i.castSucc) = 0
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) = (⨅ r, (κ a) (A ×ˢ Iic ↑↑r)).toReal

Tactic:
exact (ENNReal.toReal_iInf (fun r ↦ measure_ne_top _ _)).symm

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

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

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:
· exact hindep.comp (fun _ x ↦ (x - P[X 0]) / √Var[X 0; P]) (by fun_prop)

Goal state after:
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
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
x : γ
h0 : (ν a) (countablePartitionSet n x) = 0
h0' : (κ.fst a) (countablePartitionSet n x) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ s) = 0

Tactic:
rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)] at h0'

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
x : γ
h0 : (ν a) (countablePartitionSet n x) = 0
h0' : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ s) = 0
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
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)
⊢ κ'.fst = κ.fst

Tactic:
ext a u

Goal state after:
α : 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)
a : α
u : Set β
a✝ : MeasurableSet u
⊢ (κ'.fst a) u = (κ.fst a) u
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
⊢ MeasurableSet (univ ×ˢ range e)ᶜ

Tactic:
exact (MeasurableSet.univ.prod he.measurableSet_range).compl

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✝ : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
x✝ : ρ.fst t < ∞
| ∫⁻ (x : α) in t, (ρ.condKernel x) s ∂ρ.fst

Tactic:
rw [Measure.setLIntegral_condKernel_eq_measure_prod ht hs, hκ]

Goal state after:
α : 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
t : Set α
ht : MeasurableSet t
x✝ : ρ.fst t < ∞
| (ρ.fst ⊗ₘ κ) (t ×ˢ s)
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)ᶜ

Tactic:
exact (MeasurableSet.univ.prod he.measurableSet_range).compl

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 α γ
x : γ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a ↦ κ.density ν a x s

Tactic:
change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun a ↦ (a, x)))

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
x : γ
s : Set β
hs : MeasurableSet s
⊢ Measurable ((fun p ↦ κ.density ν p.1 p.2 s) ∘ fun a ↦ (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
heq : ∀ᵐ (x : α) ∂ρ.fst, (ρ.condKernel.map f) x = (Measure.map (Prod.map id f) ρ).condKernel x
x : α
hx : (ρ.condKernel.map f) x = (Measure.map (Prod.map id f) ρ).condKernel x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.map (embeddingReal Ω) (ρ.condKernel x)) s = (ρ.condKernel x) (f ⁻¹' s)

Tactic:
Measure.map_apply hf.measurable hs

Goal state after:
α : 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
heq : ∀ᵐ (x : α) ∂ρ.fst, (ρ.condKernel.map f) x = (Measure.map (Prod.map id f) ρ).condKernel x
x : α
hx : (ρ.condKernel.map f) x = (Measure.map (Prod.map id f) ρ).condKernel x
s : Set ℝ
hs : MeasurableSet s
⊢ (ρ.condKernel x) (embeddingReal Ω ⁻¹' s) = (ρ.condKernel x) (f ⁻¹' s)