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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun u ↦ (∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) / mgf X μ u) v =
    (deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      mgf X μ v ^ 2

Tactic:
deriv_fun_div

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ (deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      mgf X μ v ^ 2 =
    (deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      mgf X μ v ^ 2

case hc
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ DifferentiableAt ℝ (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v

case hd
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ DifferentiableAt ℝ (mgf X μ) v

case hx
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ mgf X μ v ≠ 0
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (fun ω ↦ |X ω| ^ n) μ

Tactic:
by
  convert! integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet h n
  simp

Goal state after:
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω ↦ ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz
  rw [← integrable_norm_iff]
  swap; · fun_prop
  simpa [abs_rpow_of_nonneg (abs_nonneg _), Complex.norm_exp]
    using integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hz hp

Goal state after:
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case e'_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x✝ : ℝ
⊢ 0 = deriv (cgf X μ) 0

Tactic:
simpa [hc] using (deriv_cgf_zero (hs ⟨le_refl 0, le_of_lt ht⟩)).symm

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case h
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ MemLp id 2 (Measure.map (⇑L) μ)

Tactic:
exact memLp_map_measure_iff (by fun_prop) (by fun_prop) |>.2 (L.comp_memLp' h)

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ c - x) μ)

Tactic:
simp_rw [sub_eq_add_neg]
  suffices IsGaussian ((μ.map (fun x ↦ -x)).map (fun x ↦ c + x)) by
    rwa [Measure.map_map (by fun_prop) (by fun_prop), Function.comp_def] at this
  infer_instance

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ ‖L x‖ₑ ^ p.toReal ≤ ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal

Tactic:
rw [← ENNReal.mul_rpow_of_nonneg]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ ‖L x‖ₑ ^ p.toReal ≤ (‖L‖ₑ * ‖x‖ₑ) ^ p.toReal

case hz
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ 0 ≤ p.toReal
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✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ (√2 ^ 2)⁻¹ * √2 = (√2)⁻¹

Tactic:
rw [pow_two, mul_inv, mul_assoc, inv_mul_cancel₀ (by positivity), mul_one]

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
s : Set (StrongDual 𝕜 E)
hs : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ r, ∀ x ∈ s, ‖(toLpₗ μ p) x‖ ≤ r

Tactic:
simp_rw [isVonNBounded_iff'] at hs

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
s : Set (StrongDual 𝕜 E)
hs : ∃ r, ∀ x ∈ s, ‖x‖ ≤ r
⊢ ∃ r, ∀ x ∈ s, ‖(toLpₗ μ p) x‖ ≤ r
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 μ
⊢ IsGaussian μ ↔
    ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)

Tactic:
refine ⟨fun h ↦ ⟨μ[id], covarianceBilinDual μ, isPosSemidef_covarianceBilinDual,
    h.charFunDual_eq'⟩,
    fun ⟨m, f, hf, h⟩ ↦ isGaussian_of_map_eq_gaussianReal fun L ↦ ⟨L m, (f L L).toNNReal, ?_⟩⟩

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 μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
L : E →L[ℝ] ℝ
⊢ Measure.map (⇑L) μ = gaussianReal (L m) ((f L) L).toNNReal
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L : StrongDual ℝ E
⊢ 0 ≤ ((covarianceBilinDual μ) L) L

Tactic:
by_cases h : MemLp id 2 μ
  · simp only [covarianceBilinDual, uncenteredCovarianceBilinDual,
      ContinuousLinearMap.bilinearComp_apply, IsBoundedBilinearMap.toContinuousLinearMap_apply]
    exact real_inner_self_nonneg
  · simp [h]

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

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

Tactic:
· simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt]
      exact ⟨h.trans_lt hd, by finiteness⟩

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

Goal state before:
pp: I : Finset ℝ≥0
i✝ j✝ : ↥I
⊢ covMatrix I i✝ j✝ = Matrix.of (fun s t ↦ ℙ.real (Icc 0 ↑↑s ∩ Icc 0 ↑↑t)) i✝ j✝

Tactic:
simp [Icc_inter_Icc]

Goal state after:
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
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * a ^ 2)) ∂μ =
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))

Tactic:
by
      simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter]
      rw [mul_comm]
      simp only [inv_pow, C]
      field_simp
      congr with x
      simp

Goal state after:
Module: Mathlib.Probability.CDF

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
a : ℝ
⊢ (cdf μ).measure (Iic a) = μ (Iic a)

Tactic:
rw [StieltjesFunction.measure_Iic _ (tendsto_cdf_atBot μ), sub_zero, ofReal_cdf]

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ charFun (Measure.map (fun ω ↦ ∑ k ∈ Finset.range n, X k ω) P) ((√↑n)⁻¹ * t) =
    charFun (Measure.map (X 0) P) ((√↑n)⁻¹ * t) ^ n

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ AEMeasurable (fun ω ↦ ∑ k ∈ Finset.range n, X k ω) P

Tactic:
(hindep.restrict _).charFun_map_fun_finsetSum_eq_prod (fun _ _ ↦ mX _)

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ (∏ i ∈ Finset.range n, charFun (Measure.map (X i) P)) ((√↑n)⁻¹ * t) = charFun (Measure.map (X 0) P) ((√↑n)⁻¹ * t) ^ n

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ AEMeasurable (fun ω ↦ ∑ k ∈ Finset.range n, X k ω) 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 κ
inst✝ : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q

Tactic:
rw [ae_all_iff]
  refine fun q ↦ ae_eq_of_forall_setIntegral_eq_of_sigmaFinite (μ := ν a) ?_ ?_ ?_
  · exact fun _ _ _ ↦ (hf.integrable_iInf_rat_gt _ _).integrableOn
  · exact fun _ _ _ ↦ (hf.integrable a _).integrableOn
  · intro s hs _
    rw [hf.setIntegral _ hs, hf.setIntegral_iInf_rat_gt _ _ hs]

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

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ ((Kernel.id ∥ₖ κ) a) s) (μ.prod ν)

pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (κ a) (Prod.mk x ⁻¹' s) ∂ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((Kernel.id ∥ₖ κ) (x, y)) s ∂ν ∂μ

Tactic:
· exact (Kernel.measurable_coe _ hs).aemeasurable

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (κ a) (Prod.mk x ⁻¹' s) ∂ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((Kernel.id ∥ₖ κ) (x, y)) s ∂ν ∂μ
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case inl.refine_1
Ω : 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
n : ℕ
⊢ (fun ω ↦ (√↑0)⁻¹ * (∑ k ∈ Finset.range 0, X k ω - ↑0 * ∫ (x : Ω), X 0 x ∂P)) =ᵐ[P] fun ω ↦
    (√↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P)

Tactic:
filter_upwards [this] with ω hω

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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
n : ℕ
ω : Ω
hω : ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
⊢ (√↑0)⁻¹ * (∑ k ∈ Finset.range 0, X k ω - ↑0 * ∫ (x : Ω), X 0 x ∂P) =
    (√↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P)
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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ Measure.map (fun ω ↦ (√↑0)⁻¹ * (∑ k ∈ Finset.range 0, X k ω - ↑0 * ∫ (x : Ω), X 0 x ∂P)) P = Measure.map Y P'

Tactic:
simp [hY.map_eq, 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 μ
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 (Prod.map id f) (Measure.map (fun x ↦ (X x, Y x)) μ) =
    Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ)

Tactic:
by rw [compProd_map_condDistrib hY]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : β → E
a : α
inst✝¹ : CompleteSpace E
g : α → β
inst✝ : MeasurableSingletonClass β
hg : Measurable g
⊢ ∫ (x : β), f x ∂Measure.dirac (g a) = f (g a)

Tactic:
integral_dirac _ (g a)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : β → E
a : α
inst✝¹ : CompleteSpace E
g : α → β
inst✝ : MeasurableSingletonClass β
hg : Measurable g
⊢ f (g a) = f (g a)
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
x✝ : ι → Prop
⊢ x✝ ∈ (fun p ↦ {i | p i}) ⁻¹' {s | i ∈ s} ↔ x✝ ∈ cylinder {i} {fun x ↦ True}

Tactic:
simp [funext_iff]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ 0 = 0 + 0

Tactic:
rw [zero_add]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ (Measure.pi fun i ↦ μ (e ↑i)) (⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I)) ⁻¹' S) =
    (piContent μ) (cylinder I S)

pp: case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable (I.preimage ⇑e ⋯).restrict

pp: case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ MeasurableSet (⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I)) ⁻¹' S)

pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(piCongrLeft X e)

Tactic:
piContent_cylinder μ hS,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ (Measure.pi fun i ↦ μ (e ↑i)) (⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I)) ⁻¹' S) =
    (Measure.pi fun i ↦ μ ↑i) S

case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable (I.preimage ⇑e ⋯).restrict

case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ MeasurableSet (⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I)) ⁻¹' S)

ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(piCongrLeft X e)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : ((η.withDensity (κ.rnDeriv η)) a) univ + ((κ.singularPart η) a) univ = (κ a) univ
⊢ ((κ.singularPart η) a) univ ≤ κ.bound

Tactic:
exact (self_le_add_left _ _).trans (h.le.trans (measure_le_bound _ _ _))

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
⊢ s.pi t = ⋂ s', (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ

Tactic:
rw [← Set.pi_iUnion_eq_iInter_pi, Set.iUnion_finset_eq_set]

Goal state after:
ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
⊢ s.pi t = s.pi fun i ↦ if i ∈ s then t i else Set.univ
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hb
ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
⊢ Tendsto (fun s' ↦ ∏ i ∈ s', (μ ↑i) (t ↑i)) atTop (𝓝 (⨅ s_1, ∏ i ∈ s_1, (μ ↑i) (t ↑i)))

Tactic:
exact tendsto_atTop_iInf (prod_anti_set_of_le_one' (by simp [prob_le_one]))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ ((η ∘ₖ κ) a) univ - ((η ∘ₖ κ) a) s = 0

Tactic:
measure_univ h₁,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ 1 - ((η ∘ₖ κ) a) s = 0