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

Goal state before:
pp: case e_a.e_f
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
ω : Ω
⊢ (X ω ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * rexp (v * X ω) =
    (X ω - deriv (cgf X μ) v) ^ 2 * rexp (v * X ω)

Tactic:
ring

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

Goal state before:
pp: case convert_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)
⊢ ContDiffOn ℝ (↑1 + 1) (cgf X μ) (Set.Icc 0 t)

Tactic:
exact (analyticOn_cgf.mono hs).contDiffOn hu

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
t : ℝ
⊢ rexp (↑v * t ^ 2 / 2) * (↑v * (2 * t) / 2) = ↑v * t * rexp (↑v * t ^ 2 / 2)

Tactic:
ring

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

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
i : ι
x✝¹ : i ∈ Finset.univ
j : ι
x✝ : j ∈ Finset.univ
⊢ x.ofLp i * (y.ofLp j * cov[X i, X j; μ]) = x.ofLp i * y.ofLp j * cov[X i, X j; μ]

Tactic:
ring

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

Goal state before:
pp: case neg
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
⊢ ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹

Tactic:
StrongDual.toLpₗ_apply h_Lp,

Goal state after:
case neg
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
⊢ ‖MemLp.toLp ⇑L ⋯‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
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
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ ↑(∫ (x : E), L x ∂μ) * I - ↑Var[⇑L; μ] / 2 + ↑(L c) * I = (↑(∫ (x : E), L x ∂μ) + ↑(L c)) * I - ↑Var[⇑L; μ] / 2

Tactic:
ring

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
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
this : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) * 2 = 2 * (‖p.1 + p.2‖ - ‖p.1 - p.2‖)

Tactic:
ring

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (fun x ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) μ

Tactic:
simp_rw [mul_assoc]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc, mul_comm _ (‖L₂‖), mul_assoc, ← pow_two]
      refine Integrable.const_mul ?_ _
      exact h.integrable_norm_pow (by simp)

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

Goal state before:
pp: case e_f
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
⊢ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ = ‖L₁‖ * ‖L₂‖ * ‖x‖ ^ 2

Tactic:
ring

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

Goal state before:
pp: a : ℝ
n : ℕ
⊢ a * (√2 ^ (n + 1) - 1) * (√2 + 1) = a * (1 + √2) * (√2 ^ (n + 1) - 1)

Tactic:
ring

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝¹ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this✝ : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖y‖ ≤ ‖c‖ / 2
this : ‖c‖ ≤ ‖y‖ + ‖y - c‖
⊢ 2 ^ ↑p * ‖y - c‖ ^ ↑p = 0 + 2 ^ ↑p * ‖y - c‖ ^ ↑p

Tactic:
ring

Goal state after:
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 μ
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[ℝ] ℝ
t : ℝ
⊢ t * (t * (f L) L) / 2 = (f L) L * t ^ 2 / 2

Tactic:
ring

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ^ (↑p - 1) * (2 * ‖y‖) = 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 0

Tactic:
ring

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_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 0 < c.toReal / (1 - c).toReal

Tactic:
div_pos_iff_of_pos_right

Goal state after:
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_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 0 < c.toReal

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_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 0 < (1 - c).toReal
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)
L : StrongDual ℝ E
⊢ ↑(n L) * I * 2 ^ 2 * ↑π = ↑(L m) * I * 2 - ↑((f L) L) + ↑(n L) * I * 2 ^ 2 * ↑π - ↑(L m) * I * 2 + ↑((f L) L)

Tactic:
ring

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

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
h' : MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)
⊢ ∫ (x : E), L₁ x * L₂ x ∂Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ =
    ∫ (x : E), L₂ x * L₁ x ∂Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ

Tactic:
mul_comm (L₁ _)

Goal state after:
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'
hε : 0 < ε
x : E
⊢ (‖x - y‖ + ‖y‖) ^ 2 = ‖x - y‖ ^ 2 + ‖y‖ ^ 2 + 2 * ‖x - y‖ * ‖y‖

Tactic:
ring

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ cexp (-(↑(∑ i, ⟪(stdOrthonormalBasis ℝ E) i, t⟫ ^ 2) / 2)) = cexp (-↑(‖t‖ ^ 2) / 2)

Tactic:
(stdOrthonormalBasis ℝ E).sum_sq_inner_right,

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ cexp (-(↑(‖t‖ ^ 2) / 2)) = cexp (-↑(‖t‖ ^ 2) / 2)
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'
hε : 0 < ε
x : E
⊢ ‖x - y‖ ^ 2 + ‖y‖ ^ 2 + ε * ‖x - y‖ ^ 2 + ε⁻¹ * ‖y‖ ^ 2 = (1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2

Tactic:
ring

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

Goal state before:
pp: case e'_3
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_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
⊢ C * t (n + 1) ^ 2 = logRatio (μ {x | ‖x‖ ≤ a}) * normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2

Tactic:
ring

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

Goal state before:
pp: case e_a
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_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
⊢ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n + -Real.log (c.toReal / (1 - c).toReal) * 2 ^ n =
    -2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n

Tactic:
ring

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

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
h : ∀ (s : S), ∃ I L, ∀ (ω : Ω), Y s ω = L (I.restrict fun x ↦ X x ω)
I : Finset S
⊢ HasGaussianLaw (fun ω ↦ I.restrict fun x ↦ Y x ω) P

Tactic:
choose J L hL using h
    classical
    let K : (I.biUnion J → E) →L[ℝ] I → F :=
      { toFun x s := L s (fun t ↦ x ⟨t.1, mem_biUnion.2 ⟨s.1, s.2, t.2⟩⟩)
        map_add' x y := by ext; simp [← Pi.add_def]
        map_smul' c x := by ext; simp [← Pi.smul_def] }
    have : (fun ω ↦ I.restrict (Y · ω)) = K ∘ (fun ω ↦ (I.biUnion J).restrict (X · ω)) := by
      ext; simp [K, hL, Finset.restrict_def]
    rw [this]
    exact (hX.hasGaussianLaw _).map _

Goal state after:
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)) := ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖x ∘SL inl ℝ E F‖ ≤ ‖x‖

Tactic:
grw [opNorm_comp_le, norm_inl_le_one, mul_one]

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

Goal state before:
pp: case e_f.e_6
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
y : ℝ
⊢ y ∈ Iic x ↔ y ∈ ⋂ i, Iic ↑↑i

Tactic:
simp only [mem_Iic, mem_iInter, Subtype.forall]

Goal state after:
case e_f.e_6
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
y : ℝ
⊢ y ≤ x ↔ ∀ (a : ℚ), x < ↑a → y ≤ ↑a
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case hv.hX
Ω : 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 : WithLp 2 (↥I → ℝ)
⊢ ∀ (i : ↥I), MemLp (fun ω ↦ ω i) 2 (projectiveFamily I)

Tactic:
exact fun i ↦ (IsGaussian.hasGaussianLaw_id.eval i).memLp_two

Goal state after:
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)) := ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖y ∘SL inl ℝ E F‖ ≤ ‖y‖

Tactic:
grw [opNorm_comp_le, norm_inl_le_one, mul_one]

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

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

Tactic:
rw [← setIntegral_univ, setIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
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:
rw [measureReal_def, ← Measure.iInf_rat_gt_prod_Iic hA q]
        exact (ENNReal.toReal_iInf (fun r ↦ measure_ne_top _ _)).symm

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
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
c : ℝ
x : ↥{t₀, t₀ + t} → ℝ
⊢ c * x ⟨t₀ + t, ⋯⟩ - c * x ⟨t₀, ⋯⟩ = c * (x ⟨t₀ + t, ⋯⟩ - x ⟨t₀, ⋯⟩)

Tactic:
ring

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case e'_7
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this : Tendsto (fun n ↦ (√↑n)⁻¹ * t) atTop (𝓝 0)
x✝ : ℕ
⊢ 1 + -(((↑√↑x✝)⁻¹ * ↑t) ^ 2 / 2) = 1 - ((↑√↑x✝)⁻¹ * ↑t) ^ 2 / 2

Tactic:
ring

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝ : SFinite μ
⊢ μ ⊗ₘ κ = ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(Kernel.copy α) ∘ₘ μ

Tactic:
by_cases hκ : IsSFiniteKernel κ

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝ : SFinite μ
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(Kernel.copy α) ∘ₘ μ

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝ : SFinite μ
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(Kernel.copy α) ∘ₘ μ
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

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

Tactic:
← exp_add,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (fun ω ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[⇑L₁ ∘ X, ⇑L₂ ∘ Y; P] = 0
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this : (⇑L ∘ fun ω ↦ (X ω, Y ω)) = ⇑(L ∘SL inl ℝ E F) ∘ X + ⇑(L ∘SL inr ℝ E F) ∘ Y
⊢ cexp (↑(∫ (x : Ω), (⇑L ∘ fun ω ↦ (X ω, Y ω)) x ∂P) * I - ↑Var[⇑L ∘ fun ω ↦ (X ω, Y ω); P] / 2) =
    cexp
      (↑(∫ (x : Ω), (⇑(L ∘SL inl ℝ E F) ∘ X) x ∂P) * I - ↑Var[⇑(L ∘SL inl ℝ E F) ∘ X; P] / 2 +
        (↑(∫ (x : Ω), (⇑(L ∘SL inr ℝ E F) ∘ Y) x ∂P) * I - ↑Var[⇑(L ∘SL inr ℝ E F) ∘ Y; P] / 2))
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hfm
α : 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
⊢ Measurable fun x ↦ (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)

Tactic:
change Measurable ((fun (p : α × _) ↦ κ p.1 (countablePartitionSet n p.2 ×ˢ s)
      / ν p.1 (countablePartitionSet n p.2)) ∘ (fun x ↦ (a, x)))

Goal state after:
case hfm
α : 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
⊢ Measurable
    ((fun p ↦ (κ p.1) (countablePartitionSet n p.2 ×ˢ s) / (ν p.1) (countablePartitionSet n p.2)) ∘ fun x ↦ (a, x))