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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
⊢ Tendsto (fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop

Tactic:
refine tendsto_atTop_atTop_of_monotone' ?_ ?_

Goal state after:
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
⊢ Monotone fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))

case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
⊢ ¬BddAbove (Set.range fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : 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
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ

Tactic:
refine Integrable.mono (ha.add hb) ?_ (ae_of_all _ fun ω ↦ ?_)
  · by_cases hab : a = b
    · have ha_eq_t : a = t := le_antisymm hat (hab ▸ htb)
      rw [← ha_eq_t]
      exact ha.1
    · refine AEMeasurable.aestronglyMeasurable ?_
      refine measurable_exp.comp_aemeasurable (AEMeasurable.const_mul ?_ _)
      by_cases ha_zero : a = 0
      · refine aemeasurable_of_aemeasurable_exp_mul ?_ hb.1.aemeasurable
        rw [ha_zero] at hab
        exact Ne.symm hab
      · exact aemeasurable_of_aemeasurable_exp_mul ha_zero ha.1.aemeasurable
  · simp only [norm_eq_abs, abs_exp, Pi.add_apply]
    conv_rhs => rw [abs_of_nonneg (by positivity)]
    rcases le_total 0 (X ω) with h | h
    · calc exp (t * X ω)
      _ ≤ exp (b * X ω) := exp_le_exp.mpr (mul_le_mul_of_nonneg_right htb h)
      _ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_left (exp_nonneg _)
    · calc exp (t * X ω)
      _ ≤ exp (a * X ω) := exp_le_exp.mpr (mul_le_mul_of_nonpos_right hat h)
      _ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_right (exp_nonneg _)

Goal state after:
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
ω : Ω
hω : BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)
⊢ ¬Tendsto (fun n ↦ f n ω) atTop atTop

Tactic:
htop

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
ω : Ω
hω : BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)
htop : Tendsto (fun n ↦ f n ω) atTop atTop
⊢ False
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
ω : Ω
hω : BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)
⊢ ¬Tendsto (fun n ↦ f n ω) atTop atBot

Tactic:
htop

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
ω : Ω
hω : BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)
htop : Tendsto (fun n ↦ f n ω) atTop atBot
⊢ False
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case mp
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
ω : Ω
hω₁ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n ↦ f n ω) atTop atTop
⊢ Tendsto (fun n ↦ predictablePart f ℱ μ n ω) atTop atTop

Tactic:
refine tendsto_atTop_atTop_of_monotone' ?_ ?_

Goal state after:
case mp.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
ω : Ω
hω₁ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n ↦ f n ω) atTop atTop
⊢ Monotone fun n ↦ predictablePart f ℱ μ n ω

case mp.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
ω : Ω
hω₁ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n ↦ f n ω) atTop atTop
⊢ ¬BddAbove (Set.range fun n ↦ predictablePart f ℱ μ n ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
s : Set Ω
inst✝¹ : DecidablePred fun x ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst✝ : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
⊢ stoppedValue f (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) ω = s.piecewise (f i) (f j) ω

Tactic:
stoppedValue

Goal state after:
Ω : Type u_1
s : Set Ω
inst✝¹ : DecidablePred fun x ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst✝ : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
⊢ f (s.piecewise (fun x ↦ ↑i) (fun x ↦ ↑j) ω).untopA ω = s.piecewise (f i) (f j) ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
s : Set Ω
inst✝² : DecidablePred fun x ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst✝¹ : AddCommGroup α
inst✝ : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
⊢ stoppedValue f (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) ω = (s.indicator (f i) + sᶜ.indicator (f j)) ω

Tactic:
stoppedValue

Goal state after:
Ω : Type u_1
s : Set Ω
inst✝² : DecidablePred fun x ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst✝¹ : AddCommGroup α
inst✝ : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
⊢ f (s.piecewise (fun x ↦ ↑i) (fun x ↦ ↑j) ω).untopA ω = (s.indicator (f i) + sᶜ.indicator (f j)) ω
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
x y : ℝ
⊢ gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x

Tactic:
rw [sub_eq_add_neg, ← gaussianPDFReal_sub, sub_eq_add_neg, neg_neg]

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 μ
i : ι
⊢ ((covarianceBilin (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)) ((basisFun ι ℝ) i)) ((basisFun ι ℝ) i) = Var[X i; μ]

Tactic:
by
  rw [covarianceBilin_apply_basisFun hX, covariance_self]
  have (i : ι) := (hX i).aemeasurable
  fun_prop

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

Goal state before:
pp: case e_6
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 : ℝ
⊢ {a_1 | ‖(√2 / 2) • a_1.1 + -((√2 / 2) • a_1.2)‖ ≤ a ∧ b < ‖(√2 / 2) • a_1.1 + (√2 / 2) • a_1.2‖} =
    {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}

Tactic:
have h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹ := by
      simp only [norm_mul, norm_inv, Real.norm_ofNat, Real.norm_eq_abs]
      rw [abs_of_nonneg (by positivity)]
      nth_rw 1 [← Real.sq_sqrt (by simp : (0 : ℝ) ≤ 2)]
      rw [pow_two, mul_inv, mul_assoc, inv_mul_cancel₀ (by positivity), mul_one]

Goal state after:
case e_6
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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
⊢ {a_1 | ‖(√2 / 2) • a_1.1 + -((√2 / 2) • a_1.2)‖ ≤ a ∧ b < ‖(√2 / 2) • a_1.1 + (√2 / 2) • a_1.2‖} =
    {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case zero
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}
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ μ {x | normThreshold a 0 < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ 0

Tactic:
simp only [pow_zero, pow_one, normThreshold_zero]

Goal state after:
case zero
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}
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ μ {x | a < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a})
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case succ
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}
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn : μ {x | normThreshold a n < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n
⊢ μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ (n + 1)

Tactic:
have h_mul_le : c * μ {x | normThreshold a (n + 1) < ‖x‖}
        ≤ μ {x | normThreshold a n < ‖x‖} ^ 2 :=
      measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self h_rot _ _

Goal state after:
case succ
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}
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn : μ {x | normThreshold a n < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n
h_mul_le : c * μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | normThreshold a n < ‖x‖} ^ 2
⊢ μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ (n + 1)
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).toNNReal * t ^ 2 / 2

Tactic:
rw [Real.coe_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[ℝ] ℝ
t : ℝ
⊢ t * (t * (f L) L) / 2 = (f L) L * t ^ 2 / 2

case hr
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 : ℝ
⊢ 0 ≤ (f L) 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)) μ
⊢ Integrable (fun x ↦ rexp (C' * ‖x‖ ^ 2)) μ

Tactic:
let ε := (C - C') / C'

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'
⊢ Integrable (fun x ↦ rexp (C' * ‖x‖ ^ 2)) μ
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < (1 - c).toReal ∧ (1 - c).toReal < c.toReal ∨ (1 - c).toReal < 0 ∧ c.toReal < (1 - c).toReal

Tactic:
refine Or.inl ⟨?_, ?_⟩

Goal state after:
case refine_1
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < (1 - c).toReal

case refine_2
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ (1 - c).toReal < c.toReal
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
inst✝¹ : CompleteSpace E
μ : Measure E
inst✝ : IsGaussian μ
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
⊢ C / 2 < C

Tactic:
by simp [hC_pos]

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✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
hC_neg : Integrable (fun x ↦ rexp (-C * ‖x‖ ^ 2)) μ
⊢ Set.Ioo (-C) C ⊆ interior (integrableExpSet (fun x ↦ ‖x‖ ^ 2) μ)

Tactic:
rw [IsOpen.subset_interior_iff isOpen_Ioo]

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
hC_neg : Integrable (fun x ↦ rexp (-C * ‖x‖ ^ 2)) μ
⊢ Set.Ioo (-C) C ⊆ integrableExpSet (fun x ↦ ‖x‖ ^ 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✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
hC_neg : Integrable (fun x ↦ rexp (-C * ‖x‖ ^ 2)) μ
h_subset : Set.Ioo (-C) C ⊆ interior (integrableExpSet (fun x ↦ ‖x‖ ^ 2) μ)
⊢ -C < 0

Tactic:
by simp [hC_pos]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S = μ

Tactic:
rw [multivariateGaussian, integral_map (by fun_prop) (by fun_prop),
    integral_add (integrable_const _), integral_const]
  · simp [ContinuousLinearMap.integral_comp_comm _ IsGaussian.integrable_fun_id]
  · exact IsGaussian.integrable_id.comp_measurable (by fun_prop)

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

Goal state before:
pp: case inl
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
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
x : E
ha' : ‖x‖ ≤ a
⊢ ‖x‖ ≤ a ∨ ∃ i, t i < ‖x‖ ∧ ‖x‖ ≤ t (i + 1)

Tactic:
exact Or.inl ha'

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
s : Set ((i : S) → 𝓧 i)
hs : MeasurableSet s
t : Set 𝓨
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂P, (κ a) ((fun ω i ↦ X' i ω) ⁻¹' s ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X' i ω) ⁻¹' s) * (κ a) (Y ⁻¹' t)

Tactic:
have : ∀ᵐ a ∂P, κ a (((fun ω i ↦ X i ω) ⁻¹' s) ∩ (Y ⁻¹' t)) =
      κ a ((fun ω i ↦ X i ω) ⁻¹' s) * κ a (Y ⁻¹' t) :=
    h1 ((fun ω i ↦ X i ω) ⁻¹' s) (Y ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩

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
s : Set ((i : S) → 𝓧 i)
hs : MeasurableSet s
t : Set 𝓨
ht : MeasurableSet t
this : ∀ᵐ (a : α) ∂P, (κ a) ((fun ω i ↦ X i ω) ⁻¹' s ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X i ω) ⁻¹' s) * (κ a) (Y ⁻¹' t)
⊢ ∀ᵐ (a : α) ∂P, (κ a) ((fun ω i ↦ X' i ω) ⁻¹' s ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X' i ω) ⁻¹' s) * (κ a) (Y ⁻¹' t)
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: case refine_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ (↥(J i) → E)
L₂ : StrongDual ℝ (↥(J j) → E)
h1 : (⇑L₁ ∘ fun ω k ↦ X (↑i) (↑k) ω) = ∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k
h2 : (⇑L₂ ∘ fun ω k ↦ X (↑j) (↑k) ω) = ∑ k, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑j ↑k
⊢ cov[∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k, ⇑L₂ ∘ fun ω j_1 ↦ X (↑j) (↑j_1) ω; P] = 0

Tactic:
h2,

Goal state after:
case refine_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ (↥(J i) → E)
L₂ : StrongDual ℝ (↥(J j) → E)
h1 : (⇑L₁ ∘ fun ω k ↦ X (↑i) (↑k) ω) = ∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k
h2 : (⇑L₂ ∘ fun ω k ↦ X (↑j) (↑k) ω) = ∑ k, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑j ↑k
⊢ cov[∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k,
      ∑ k, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑j ↑k; P] =
    0