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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
h' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ hittingBtwn u s n m₁ ω = hittingBtwn u s n m₂ ω

Tactic:
by
  simp only [hittingBtwn, if_pos h']
  obtain ⟨j, hj₁, hj₂⟩ := h'
  rw [if_pos]
  · refine le_antisymm ?_ (by gcongr; exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩])
    refine le_csInf ⟨j, Set.Icc_subset_Icc_right h hj₁, hj₂⟩ fun i hi => ?_
    by_cases hi' : i ≤ m₁
    · exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hi.1.1, hi'⟩, hi.2⟩
    · change j ∈ {i | u i ω ∈ s} at hj₂
      exact ((csInf_le bddBelow_Icc.inter_of_left ⟨hj₁, hj₂⟩).trans hj₁.2).trans (le_of_not_ge hi')
  exact ⟨j, ⟨hj₁.1, hj₁.2.trans h⟩, hj₂⟩

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

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
this : ∀ (i : WithTop ι), {ω | min (τ ω) (π ω) ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}
⊢ ((MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})) ∧
      MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | π ω ≤ ↑i})) →
    MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | min (τ ω) (π ω) ≤ ↑i})

Tactic:
this,

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
this : ∀ (i : WithTop ι), {ω | min (τ ω) (π ω) ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i}
⊢ ((MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})) ∧
      MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | π ω ≤ ↑i})) →
    MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ ({ω | τ ω ≤ ↑i} ∪ {ω | π ω ≤ ↑i}))
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ upcrossings a b f ω < ∞ ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
this,

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ (∃ k, upcrossings a b f ω ≤ ↑k) ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ⨆ n, ∫⁻ (a_1 : Ω), ↑(upcrossingsBefore a b f n a_1) ∂μ ≤
    ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
this,

Goal state after:
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ⨆ n, ∫⁻ (a_1 : Ω), ↑(upcrossingsBefore a b f n a_1) ∂μ ≤
    ⨆ N, ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ MeasurableSet (Set.univ ∩ {ω | τ ω ≤ π ω})

Tactic:
← hτ.measurableSet_inter_le_iff hπ,

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ MeasurableSet (Set.univ ∩ {ω | τ ω ≤ π ω})
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
inst✝ : LinearOrder ι
⊢ (stoppedProcess u fun x ↦ ⊤) = u

Tactic:
ext; simp [stoppedProcess]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ centralMoment X 1 μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ

Tactic:
simp only [centralMoment, Pi.sub_apply, pow_one]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ centralMoment X 1 μ = 0

Tactic:
simp only [centralMoment, Pi.sub_apply, pow_one]

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = 0
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ 0 < ∫ (x : Ω), rexp (t * X x) ∂μ

Tactic:
this,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ 0 < ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
h_eq_univ : (Function.support fun x ↦ rexp (t * X x)) = Set.univ
⊢ 0 < μ Set.univ

Tactic:
refine Ne.bot_lt ?_

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
h_eq_univ : (Function.support fun x ↦ rexp (t * X x)) = Set.univ
⊢ μ Set.univ ≠ ⊥
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : 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 : Ω
this : {i ∈ s | y ∈ {ω | τ ω = ↑i}} = {(τ y).untopA}
⊢ u (τ y).untopA y = ∑ i ∈ s with y ∈ {ω | τ ω = ↑i}, u i y

Tactic:
this,

Goal state after:
Ω : 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 : Ω
this : {i ∈ s | y ∈ {ω | τ ω = ↑i}} = {(τ y).untopA}
⊢ u (τ y).untopA y = ∑ i ∈ {(τ y).untopA}, u i y
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)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
⊢ (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ BddBelow (Set.range fun n ↦ f n ω)

Tactic:
this,

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)
ω : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
⊢ (∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)) ↔ BddBelow (Set.range fun n ↦ f n ω)
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω ↦ rexp (t * Y ω)) μ
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

Tactic:
by
  by_cases hμ : μ = 0
  · simp [hμ]
  simp only [cgf, h_indep.mgf_add h_int_X.aestronglyMeasurable h_int_Y.aestronglyMeasurable]
  exact log_mul (mgf_pos' hμ h_int_X).ne' (mgf_pos' hμ h_int_Y).ne'

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Measure.map X μ = Measure.dirac x
t : ℝ
this : IsProbabilityMeasure (Measure.map X μ)
⊢ rexp (id x * t) = rexp (x * t)

Tactic:
id_def

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Measure.map X μ = Measure.dirac x
t : ℝ
this : IsProbabilityMeasure (Measure.map X μ)
⊢ rexp (x * t) = rexp (x * t)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
this : {a | ↑n + 1 ≤ τ a} = {a | ↑n < τ a}
⊢ {a | ↑n = τ a ∨ ↑n < τ a}.indicator (u n) x = ({a | ↑n = τ a} ∪ {a | ↑n + 1 ≤ τ a}).indicator (u n) x

Tactic:
this,

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
this : {a | ↑n + 1 ≤ τ a} = {a | ↑n < τ a}
⊢ {a | ↑n = τ a ∨ ↑n < τ a}.indicator (u n) x = ({a | ↑n = τ a} ∪ {a | ↑n < τ a}).indicator (u n) x
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
this : {a | ↑n ≤ τ a}.indicator (u n) = {a | ↑n + 1 ≤ τ a}.indicator (u n) + {a | τ a = ↑n}.indicator (u n)
⊢ {a | ↑n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range n, {ω | τ ω = ↑i}.indicator (u i) =
    {a | ↑n + 1 ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range (n + 1), {a | τ a = ↑i}.indicator (u i)

Tactic:
this,

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
this : {a | ↑n ≤ τ a}.indicator (u n) = {a | ↑n + 1 ≤ τ a}.indicator (u n) + {a | τ a = ↑n}.indicator (u n)
⊢ {a | ↑n + 1 ≤ τ a}.indicator (u n) + {a | τ a = ↑n}.indicator (u n) +
      ∑ i ∈ Finset.range n, {ω | τ ω = ↑i}.indicator (u i) =
    {a | ↑n + 1 ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range (n + 1), {a | τ a = ↑i}.indicator (u i)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = max (rexp (t * x)) (rexp (-t * x))

Tactic:
· rw [rpow_max (by positivity) (by positivity) hp, ← exp_mul, ← exp_mul]
      ring_nf
      congr <;> rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]

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

Goal state before:
pp: case a
Ω : 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)
this : ε = z + (ε - z)
⊢ ε.re * X ω ≤ z.re * X ω + t / 2 * |X ω|

Tactic:
this,

Goal state after:
case a
Ω : 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)
this : ε = z + (ε - z)
⊢ (z + (ε - z)).re * X ω ≤ z.re * X ω + t / 2 * |X ω|
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
h_pos : 0 < min (v - l) (u - v)
ht : 0 < t
hvt : ¬v + t = 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul hvt
      (h_subset (add_half_inf_sub_mem_Ioo hvlu)).aemeasurable

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
this : |c⁻¹| * |c| = 1
⊢ |c⁻¹| * |c| * gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x =
    gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x

Tactic:
this,

Goal state after:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
this : |c⁻¹| * |c| = 1
⊢ 1 * gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x = gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
y : ℝ
this : (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x
⊢ Measure.map (fun x ↦ y + -x) (gaussianReal μ v) = gaussianReal (y + -μ) v

Tactic:
this,

Goal state after:
μ : ℝ
v : ℝ≥0
y : ℝ
this : (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x
⊢ Measure.map ((fun x ↦ y + x) ∘ fun x ↦ -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
⊢ HasLaw (-X) (gaussianReal (-μ) v) P

Tactic:
Pi.neg_def,

Goal state after:
μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
⊢ HasLaw (fun i ↦ -X i) (gaussianReal (-μ) v) P
Module: Mathlib.Probability.Distributions.Gaussian.Real

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

Tactic:
this,

Goal state after:
μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ deriv (fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)) 0 = ↑v
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : ⇑L = fun x ↦ L 1 * x
⊢ Measure.map (⇑L) (gaussianReal μ v) = gaussianReal (L μ) ((L 1 ^ 2).toNNReal * v)

Tactic:
this,

Goal state after:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : ⇑L = fun x ↦ L 1 * x
⊢ Measure.map (fun x ↦ L 1 * x) (gaussianReal μ v) =
    gaussianReal ((fun x ↦ L 1 * x) μ) (((fun x ↦ L 1 * x) 1 ^ 2).toNNReal * v)
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 μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
this : ∫ (x : E), L x ∂μ ∗ ν = ∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν
⊢ Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν = gaussianReal (∫ (x : E), L x ∂μ ∗ ν) Var[⇑L; μ ∗ ν].toNNReal

Tactic:
this,

Goal state after:
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 μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
this : ∫ (x : E), L x ∂μ ∗ ν = ∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν
⊢ Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν =
    gaussianReal (∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν) Var[⇑L; μ ∗ ν].toNNReal
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
⊢ ∃ n, t n < x ∧ x ≤ t (n + 1)

Tactic:
have h' m := Nat.find_min h (m := m)

Goal state after:
β : 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, ¬x ≤ t m
⊢ ∃ n, t n < x ∧ x ≤ t (n + 1)
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
⊢ x ≤ t (Nat.find h - 1 + 1)

Tactic:
by simp [Nat.find_spec h, hx]

Goal state after:
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
⊢ (fun x ↦ ‖L₁ x‖ * ‖L₂ x‖) x ≤ (fun x ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) x

Tactic:
simp only
      rw [mul_assoc]
      gcongr
      · exact ContinuousLinearMap.le_opNorm L₁ x
      · exact ContinuousLinearMap.le_opNorm L₂ x

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
L : StrongDual ℝ E
this : (⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i) = ∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i
⊢ Var[⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i; Measure.pi fun x ↦ gaussianReal 0 1] = ‖L‖ ^ 2

Tactic:
this,

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
L : StrongDual ℝ E
this : (⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i) = ∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i
⊢ Var[∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i; Measure.pi fun x ↦ gaussianReal 0 1] = ‖L‖ ^ 2
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
⊢ charFun (stdGaussian E) t = cexp (-↑‖t‖ ^ 2 / 2)

Tactic:
rw [charFun_apply, stdGaussian, integral_map (Measurable.aemeasurable (by fun_prop))
    (Measurable.aestronglyMeasurable (by fun_prop))]

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ (∫ (x : Fin (finrank ℝ E) → ℝ),
      cexp (↑⟪∑ i, x i • (stdOrthonormalBasis ℝ E) i, t⟫ * I) ∂Measure.pi fun x ↦ gaussianReal 0 1) =
    cexp (-↑‖t‖ ^ 2 / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : OrthonormalBasis ι ℝ E
this : (fun x ↦ ∑ i, x i • b i) = ⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ toLp 2
⊢ stdGaussian E = Measure.map (fun x ↦ ∑ i, x i • b i) (Measure.pi fun x ↦ gaussianReal 0 1)

Tactic:
this,

Goal state after:
ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : OrthonormalBasis ι ℝ E
this : (fun x ↦ ∑ i, x i • b i) = ⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ toLp 2
⊢ stdGaussian E =
    Measure.map (⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ toLp 2) (Measure.pi fun x ↦ gaussianReal 0 1)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ cov[fun x ↦ x.ofLp i, fun x ↦ x.ofLp j; multivariateGaussian μ S] = S i j

Tactic:
this,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ cov[fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫, fun x ↦ x.ofLp j; multivariateGaussian μ S] = S i j
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ cov[fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫, fun x ↦ x.ofLp j; multivariateGaussian μ S] = S i j

Tactic:
this,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ cov[fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫, fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) j, x⟫;
      multivariateGaussian μ S] =
    S i j
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: case hv
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
this :
  ∀ (i : ↥J),
    (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI) = fun u ↦ u.ofLp ⟨↑i, ⋯⟩
⊢ cov[(fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI),
      (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis j, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI);
      multivariateGaussian μ S] =
    ((covarianceBilin
          (multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ) (S.submatrix (fun i ↦ ⟨↑i, ⋯⟩) fun i ↦ ⟨↑i, ⋯⟩)))
        ((EuclideanSpace.basisFun ↥J ℝ).toBasis i))
      ((EuclideanSpace.basisFun ↥J ℝ).toBasis j)

Tactic:
this,

Goal state after:
case hv
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
this :
  ∀ (i : ↥J),
    (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI) = fun u ↦ u.ofLp ⟨↑i, ⋯⟩
⊢ cov[fun u ↦ u.ofLp ⟨↑i, ⋯⟩, fun u ↦ u.ofLp ⟨↑j, ⋯⟩; multivariateGaussian μ S] =
    ((covarianceBilin
          (multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ) (S.submatrix (fun i ↦ ⟨↑i, ⋯⟩) fun i ↦ ⟨↑i, ⋯⟩)))
        ((EuclideanSpace.basisFun ↥J ℝ).toBasis i))
      ((EuclideanSpace.basisFun ↥J ℝ).toBasis j)