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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
hab : a < b
⊢ Measurable (upcrossingsBefore a b f N)

Tactic:
have : upcrossingsBefore a b f N = fun ω =>
      ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i := by
    ext ω
    exact upcrossingsBefore_eq_sum hab
  rw [this]
  refine Finset.measurable_fun_sum _ fun i _ => Measurable.indicator measurable_const <|
    ℱ.le N _ ?_
  simpa only [ENat.some_eq_natCast, Nat.cast_lt] using!
    hf.isStoppingTime_upperCrossingTime.measurableSet_lt_of_pred N

Goal state after:
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:
simp_rw [this, ENNReal.mul_iSup, iSup_le_iff]

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)⁺ ∂μ)
⊢ ∀ (i : ℕ),
    ENNReal.ofReal (b - a) * ∫⁻ (a_1 : Ω), ↑(upcrossingsBefore a b f i a_1) ∂μ ≤
      ⨆ N, ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal
        (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
          stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε},
          stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ)

Tactic:
gcongr with ω hω
      · exact smul_le_stoppedValue_hittingBtwn hsub n
      · exact (hsub.integrable n).integrableOn
      · refine Integrable.integrableOn ?_
        refine hsub.integrable_stoppedValue ?_ (fun ω ↦ mod_cast hittingBtwn_le ω)
        exact hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici
      · exact nullMeasurableSet_lt (measurable_range_sup'' fun n _ ↦
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)).aemeasurable aemeasurable_const
      rw [Set.mem_ofPred_eq] at hω
      have : hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω = n := by
        simp only [hittingBtwn, Set.mem_ofPred_eq, ite_eq_right_iff, forall_exists_index, and_imp]
        intro m hm hεm
        exact False.elim
          ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩))
      simp only [stoppedValue, this, ge_iff_le]
      refine le_of_eq ?_
      congr

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
ω : Ω
hω : σ ω ≠ ⊤
⊢ stoppedValue (stoppedProcess u τ) σ ω = stoppedValue u (fun ω ↦ min (σ ω) (τ ω)) ω

Tactic:
by
  simp [stoppedValue_stoppedProcess, hω]

Goal state after:
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
c : E
t : Set Ω
hmt : MeasurableSet t
a✝ : μ t < ∞
⊢ (μ t * μ s).toReal • c = ∫ (x : Ω) in s, t.indicator (fun x ↦ c) x ∂μ

Tactic:
← hindp _ _ hmt hms,

Goal state after:
case pos.refine_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
c : E
t : Set Ω
hmt : MeasurableSet t
a✝ : μ t < ∞
⊢ (μ (t ∩ s)).toReal • c = ∫ (x : Ω) in s, t.indicator (fun x ↦ c) x ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
⊢ Measurable fun p ↦ min (↑↑p.1) (τ p.2)

Tactic:
refine measurable_of_restrict_of_restrict_compl hs ?_ ?_

Goal state after:
case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
⊢ Measurable (s.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))

case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
⊢ Measurable (sᶜ.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))
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:
neg_mul

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

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω ↦ rexp (t * Y ω)) μ
htX : ¬Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ 0 ≤ mgf Y μ t

Tactic:
exact mgf_nonneg

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

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : t ≤ 0
htX : Integrable (fun ω ↦ rexp (t * X ω)) μ
htY : ¬Integrable (fun ω ↦ rexp (t * Y ω)) μ
⊢ 0 ≤ mgf X μ t

Tactic:
exact mgf_nonneg

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

Goal state before:
pp: case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (fun ω ↦ rexp (t * X i ω)) μ
⊢ mgf (X i + ∑ x ∈ s, X x) μ t = ∏ i ∈ insert i s, mgf (X i) μ t

Tactic:
IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),

Goal state after:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (fun ω ↦ rexp (t * X i ω)) μ
⊢ mgf (X i) μ t * mgf (∑ j ∈ s, X j) μ t = ∏ i ∈ insert i s, mgf (X i) μ t
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ ↑n} = s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n}
hin : ¬i ≤ n
hτn : ∀ (ω : Ω), ¬τ ω ≤ ↑n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n})

Tactic:
have hηn : ∀ ω, ¬η ω ≤ n := fun ω hηn => hin (mod_cast (hη ω).trans hηn)

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ ↑n} = s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n}
hin : ¬i ≤ n
hτn : ∀ (ω : Ω), ¬τ ω ≤ ↑n
hηn : ∀ (ω : Ω), ¬η ω ≤ ↑n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n})
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case e_f
μ : Measure ℝ
t x : ℝ
⊢ cexp (↑t * I * ↑x) = cexp (↑t * ↑x * I)

Tactic:
ring_nf

Goal state after:
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 * p)) (rexp (-t / p * x * p)) = max (rexp (t * x)) (rexp (-t * x))

Tactic:
ring_nf

Goal state after:
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 * p⁻¹ * x)) (rexp (-(t * p * p⁻¹ * x))) = max (rexp (t * x)) (rexp (-(t * x)))
Module: Mathlib.Probability.Moments.MGFAnalytic

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

Tactic:
rw [deriv_fun_div]
    · rw [h_d_mgf.symm.differentiableAt_iff, ← iteratedDeriv_one]
      exact differentiableAt_iteratedDeriv_mgf h 1
    · exact differentiableAt_mgf h
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'

Goal state after:
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 ω)) μ
n : ℕ
⊢ Integrable (fun ω ↦ |X ω| ^ n * rexp (v * X ω)) μ

Tactic:
convert!
    integrable_rpow_abs_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg
      (by positivity : 0 ≤ (n : ℝ)) with
    ω
  simp

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ ∫ (x : ℝ), (↑√(2 * (π * ↑v)))⁻¹ * (cexp (-(↑x - ↑μ) ^ 2 / (2 * ↑↑v)) * cexp (z * ↑x)) =
    (↑√(2 * (π * ↑v)))⁻¹ * ∫ (x : ℝ), cexp (-(2 * ↑↑v)⁻¹ * ↑x ^ 2 + (z + ↑μ / ↑↑v) * ↑x + -↑μ ^ 2 / (2 * ↑↑v))

Tactic:
integral_const_mul,

Goal state after:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (↑√(2 * (π * ↑v)))⁻¹ * ∫ (a : ℝ), cexp (-(↑a - ↑μ) ^ 2 / (2 * ↑↑v)) * cexp (z * ↑a) =
    (↑√(2 * (π * ↑v)))⁻¹ * ∫ (x : ℝ), cexp (-(2 * ↑↑v)⁻¹ * ↑x ^ 2 + (z + ↑μ / ↑↑v) * ↑x + -↑μ ^ 2 / (2 * ↑↑v))
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case e_a
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (↑π * (2 * ↑↑v)) ^ 2⁻¹ = (2 * ↑π * ↑↑v) ^ 2⁻¹

Tactic:
ring_nf

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

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

Tactic:
exact (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2).sub h_int

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

Goal state before:
pp: case e_a.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ deriv (cgf X μ) v ^ 2 * mgf X μ v = ∫ (a : Ω), deriv (cgf X μ) v ^ 2 * rexp (v * X a) ∂μ

Tactic:
integral_const_mul,

Goal state after:
case e_a.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ deriv (cgf X μ) v ^ 2 * mgf X μ v = deriv (cgf X μ) v ^ 2 * ∫ (a : Ω), rexp (v * X a) ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

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

Tactic:
ring_nf

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : Subsingleton E
inst✝ : IsProbabilityMeasure μ
s : Set E
⊢ μ s = (Measure.dirac 0) s

Tactic:
apply Subsingleton.set_cases (p := fun s ↦ μ s = _)

Goal state after:
case h0
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : Subsingleton E
inst✝ : IsProbabilityMeasure μ
s : Set E
⊢ μ ∅ = (Measure.dirac 0) ∅

case h1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : Subsingleton E
inst✝ : IsProbabilityMeasure μ
s : Set E
⊢ μ Set.univ = (Measure.dirac 0) Set.univ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ ∫ (ω : ℝ), ω ^ 2 ∂gaussianReal 0 v = iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0

Tactic:
rw [iteratedDeriv_mgf_zero] <;> simp

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

Goal state before:
pp: m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
⊢ cexp (↑t * ↑m₁ * Complex.I - ↑↑v₁ * ↑t ^ 2 / 2 + (↑t * ↑m₂ * Complex.I - ↑↑v₂ * ↑t ^ 2 / 2)) =
    cexp (↑t * (↑m₁ + ↑m₂) * Complex.I - (↑↑v₁ + ↑↑v₂) * ↑t ^ 2 / 2)

Tactic:
ring_nf

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

Goal state before:
pp: case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ ∫ (x : E), ↑u * ↑(L x) ∂μ = ↑u * ↑(∫ (x : E), L x ∂μ)

Tactic:
integral_const_mul,

Goal state after:
case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ ↑u * ∫ (a : E), ↑(L a) ∂μ = ↑u * ↑(∫ (x : E), L x ∂μ)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e_a
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✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inl ℝ E F
hL₁ : L₁ = L ∘SL ContinuousLinearMap.inl ℝ E F
L₂ : F →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inr ℝ E F
hL₂ : L₂ = L ∘SL ContinuousLinearMap.inr ℝ E F
⊢ ↑Var[⇑L₁; μ] / 2 + ↑Var[⇑L₂; ν] / 2 = ↑Var[⇑L; μ.prod ν] / 2

Tactic:
· field_simp
    rw [variance_dual_prod' (IsGaussian.memLp_dual μ (L.comp (.inl ℝ E F)) 2 (by simp))
      (IsGaussian.memLp_dual ν (L.comp (.inr ℝ E F)) 2 (by simp))]
    norm_cast

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : ¬S.PosSemidef
⊢ multivariateGaussian μ S = Measure.dirac μ

Tactic:
by
  rw [multivariateGaussian, CFC.sqrt, cfcₙ_apply_of_not_predicate]
  · simp
  change ¬ (S - 0).PosSemidef
  simpa

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ Integrable (⇑(toEuclideanCLM (CFC.sqrt S))) (stdGaussian (EuclideanSpace ℝ ι))

Tactic:
· exact IsGaussian.integrable_id.comp_measurable (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic

Goal state before:
pp: case convert_1
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ Monotone t'

pp: case convert_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ EventuallyConst t' atTop

Tactic:
· exact fun a b hab ↦ ht (by grind)

Goal state after:
case convert_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ EventuallyConst t' atTop
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 μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
h_neg : a < 0
x : E
⊢ a < ‖x‖

Tactic:
exact h_neg.trans_le (norm_nonneg _)

Goal state after:
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
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
⊢ iIndepFun X P

Tactic:
iIndepFun_iff_charFunDual_pi fun i ↦ hX.aemeasurable.eval i

Goal state after:
Ω : 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
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
⊢ ∀ (L : StrongDual ℝ ((x : ι) → E x)),
    charFunDual (Measure.map (fun ω x ↦ X x ω) P) L =
      ∏ i, charFunDual (Measure.map (fun x ↦ X i x) P) (L ∘SL single ℝ E i)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
t : ℝ≥0
⊢ ∫ (x : Ω), (√↑c)⁻¹ * B (c * t) x ∂P = 0

Tactic:
integral_const_mul,

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
t : ℝ≥0
⊢ (√↑c)⁻¹ * ∫ (a : Ω), B (c * t) a ∂P = 0