mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)

Tactic:
have hdown := hf.neg.submartingale.bddAbove_iff_exists_tendsto hbdd'

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), rexp (t * (α * X x)) ∂μ = ∫ (x : Ω), rexp (t * α * X x) ∂μ

Tactic:
mul_assoc

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case mpr
Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
ω : ι
h : ω = (τ y).untopA
⊢ ω ∈ s ∧ τ y = ↑ω

Tactic:
· simp only [h]
    specialize hbdd y
    have : τ y ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
    lift τ y to ι using this with i hi
    simpa using hbdd

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

Goal state before:
pp: case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_int : ∀ i ∈ ∅, AEStronglyMeasurable (fun ω ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ

Tactic:
| empty =>

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

Goal state before:
pp: case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), Measurable (X i)
h_int : ∀ i ∈ ∅, Integrable (fun ω ↦ rexp (t * X i ω)) μ
⊢ Integrable (fun ω ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ

Tactic:
| empty =>

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

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
⊢ AEMeasurable X μ

Tactic:
refine aemeasurable_of_aemeasurable_exp_mul ?_ hb.1.aemeasurable

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
⊢ b ≠ 0
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
⊢ mgf (∑ i ∈ ∅, X i) μ t = ∏ i ∈ ∅, mgf (X i) μ t

Tactic:
| empty =>

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | X ω ≤ ε} ≤ rexp (- - -t * ε) * mgf X μ (- -t)

Tactic:
← mgf_neg,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | X ω ≤ ε} ≤ rexp (- - -t * ε) * mgf (-X) μ (-t)
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : CompleteSpace E
inst✝⁴ : CompleteSpace F
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
L : E ≃L[𝕜] F
⊢ ∫ (x : F), x ∂Measure.map (⇑L) μ = L (∫ (x : E), x ∂μ)

Tactic:
show ⇑L = ⇑L.toHomeomorph.toMeasurableEquiv from rfl,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : CompleteSpace E
inst✝⁴ : CompleteSpace F
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
L : E ≃L[𝕜] F
⊢ ∫ (x : F), x ∂Measure.map (⇑L.toHomeomorph.toMeasurableEquiv) μ = L.toHomeomorph.toMeasurableEquiv (∫ (x : E), x ∂μ)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
⊢ Integrable (fun a ↦ ||X a| ^ p| * rexp (v * X a + x * |X a|)) μ

Tactic:
refine Integrable.mono (g := fun a ↦ (p / (|t| - x)) ^ p * exp (v * X a + |t| * |X a|))
    ?_ ?_ <| ae_of_all _ fun ω ↦ ?_

Goal state after:
case refine_2.refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
⊢ Integrable (fun a ↦ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)) μ

case refine_2.refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
⊢ AEStronglyMeasurable (fun a ↦ ||X a| ^ p| * rexp (v * X a + x * |X a|)) μ

case refine_2.refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
ω : Ω
⊢ ‖||X ω| ^ p| * rexp (v * X ω + x * |X ω|)‖ ≤ ‖(p / (|t| - x)) ^ p * rexp (v * X ω + |t| * |X ω|)‖
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω ↦ |X ω| ^ p * rexp (v * X ω)) μ

Tactic:
convert!
    integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul ht_int_pos ht_int_neg le_rfl _ hp using 4
  · simp
  · simp [ht]

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

Goal state before:
pp: case refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ HasDerivAt (fun x ↦ ↑(X ω) ^ n * cexp (x * ↑(X ω))) (↑(X ω) ^ n * ↑(X ω) * cexp (ε * ↑(X ω))) ε

Tactic:
mul_assoc

Goal state after:
case refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ HasDerivAt (fun x ↦ ↑(X ω) ^ n * cexp (x * ↑(X ω))) (↑(X ω) ^ n * (↑(X ω) * cexp (ε * ↑(X ω)))) ε
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (fun ω ↦ rexp ((v + min (v - l) (u - v) / 2) * X ω)) μ

pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (fun ω ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ

Tactic:
· exact h_subset (add_half_inf_sub_mem_Ioo hvlu)

Goal state after:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (fun ω ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
h : ∃ n, x ≤ t n
h' : ∀ m < Nat.find h, t m < x
⊢ Nat.find h - 1 < Nat.find h

Tactic:
by simp [hx]

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:
mul_assoc

Goal state after:
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‖))) μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case refine_3
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₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖

Tactic:
mul_assoc

Goal state after:
case refine_3
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₁‖ * ‖x‖ * (‖L₂‖ * ‖x‖)
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✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

Tactic:
calc ‖uncenteredCovarianceBilinDual μ L₁ L₂‖
  _ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredCovarianceBilinDual_apply h]
  _ ≤ ∫ x, ‖L₁ x‖ * ‖L₂ x‖ ∂μ := (norm_integral_le_integral_norm _).trans (by simp)
  _ ≤ ∫ x, ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ := by
    refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
    · simp_rw [← norm_mul]
      exact (MemLp.integrable_mul (h.continuousLinearMap_comp L₁)
        (h.continuousLinearMap_comp L₂)).norm
    · 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)
    · simp only
      rw [mul_assoc]
      gcongr
      · exact ContinuousLinearMap.le_opNorm L₁ x
      · exact ContinuousLinearMap.le_opNorm L₂ x
  _ = ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
    rw [← integral_const_mul]
    congr with x
    ring

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

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

Tactic:
mul_assoc

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

Tactic:
mul_assoc

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 : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
| ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * (c * ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n)))
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ Var[fun x ↦ x s; projectiveFamily I] = ↑↑s

Tactic:
rw [← covariance_self, covariance_eval_projectiveFamily, min_self]

Goal state after:
I : Finset ℝ≥0
s : ↥I
⊢ AEMeasurable (fun x ↦ x s) (projectiveFamily I)
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
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
x : E
hx : ‖x‖ ≤ a
⊢ x ∈ closedBall 0 a

Tactic:
by simp [hx]

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

Goal state before:
pp: case empty
Ω : 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
mX : ∀ i ∈ ∅, AEMeasurable (X i) P
hX : iIndepFun (∅.restrict X) P
⊢ charFunDual (Measure.map (∑ i ∈ ∅, X i) P) = ∏ i ∈ ∅, charFunDual (Measure.map (X i) P)

Tactic:
| empty =>

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 : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen : MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
hs : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : Set 𝓨
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂P,
    (κ a) ((fun ω i ↦ X i ω) ⁻¹' (↑I).pi s ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X i ω) ⁻¹' (↑I).pi s) * (κ a) (Y ⁻¹' t)

Tactic:
simp only [Set.mem_pi, Set.mem_univ, Set.mem_ofPred_eq, forall_const] at hs

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

Goal state before:
pp: x y : ℚ
hxy : x ≤ y
⊢ (if x < 0 then 0 else 1) ≤ if y < 0 then 0 else 1

Tactic:
split_ifs with h_1 h_2 h_2

Goal state after:
case pos
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : y < 0
⊢ 0 ≤ 0

case neg
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : ¬y < 0
⊢ 0 ≤ 1

case pos
x y : ℚ
hxy : x ≤ y
h_1 : ¬x < 0
h_2 : y < 0
⊢ 1 ≤ 0

case neg
x y : ℚ
hxy : x ≤ y
h_1 : ¬x < 0
h_2 : ¬y < 0
⊢ 1 ≤ 1
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ toRatCDF (fun p ↦ f p.2) ((), a) = toRatCDF f a

Tactic:
unfold toRatCDF
  rw [isRatStieltjesPoint_unit_prod_iff]

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

Goal state before:
pp: 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[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x y : StrongDual ℝ (E × F)
⊢ (L₁.toBilinForm (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂.toBilinForm (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F) =
    (L₁.toBilinForm (y ∘SL inl ℝ E F)) (x ∘SL inl ℝ E F) + (L₂.toBilinForm (y ∘SL inr ℝ E F)) (x ∘SL inr ℝ E F)

Tactic:
h₁.eq,

Goal state after:
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[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x y : StrongDual ℝ (E × F)
⊢ (L₁.toBilinForm (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂.toBilinForm (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F) =
    (L₁.toBilinForm (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂.toBilinForm (y ∘SL inr ℝ E F)) (x ∘SL inr ℝ E F)
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
⊢ IsGaussian (Measure.map (fun ω x ↦ X x ω) P)

Tactic:
by
    have := hX2.isProbabilityMeasure
    let := Fintype.ofFinite ι
    rw [isGaussian_iff_gaussian_charFunDual]
    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.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (i : ℝ), Measurable fun a ↦ ENNReal.ofReal (↑(condCDF ρ a) i)

Tactic:
exact fun u ↦ (measurable_condCDF ρ u).ennreal_ofReal

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
⊢ ∀ (s : Set β), MeasurableSet s → (ν a) s < ∞ → IntegrableOn (fun a_3 ↦ f (a, a_3) q) s (ν a)

Tactic:
exact fun _ _ _ ↦ (hf.integrable a _).integrableOn

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) ∅ ∂ν a = (κ a) (s ×ˢ ∅)

Tactic:
simp only [measure_empty, lintegral_const, zero_mul, prod_empty]

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) ∅ ∂ν a = (κ a) (s ×ˢ ∅)

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' ∅) ∂ν a = (κ a) ∅

Tactic:
| empty =>

Goal state after: