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

Goal state before:
pp: case refine_2.ht
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ ∃ i, ∃ (_ : i ∈ Finset.range (m + 1)), e ∈ Set.range (Function.curry (X m) i)

Tactic:
Set.mem_range

Goal state after:
case refine_2.ht
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ ∃ i, ∃ (_ : i ∈ Finset.range (m + 1)), ∃ y, Function.curry (X m) i y = e
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
⊢ Submartingale f 𝒢 μ

Tactic:
by
  refine ⟨hadp, fun i j hij ↦ ?_, hint⟩
  induction j, hij using Nat.le_induction with
  | base =>
    refine ae_of_all _ fun _ ↦ ?_
    rw [condExp_of_stronglyMeasurable (𝒢.le i) (hadp i) (hint i)]
  | succ k hik hk =>
    filter_upwards [hk, condExp_mono (hint k) integrable_condExp (hf k),
      𝒢.condExp_condExp (f (k + 1)) hik] with ω hω1 hω2 hω3
    grw [hω1, hω2, hω3]

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

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ sInf (Set.Icc n m ∩ {i | u i ω ∈ s})

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ m

Tactic:
· refine le_csInf ?_ fun b hb => ?_
    · obtain ⟨k, hk_Icc, hk_s⟩ := h
      exact ⟨k, hk_Icc, hk_s⟩
    · rw [Set.mem_inter_iff] at hb
      exact hb.1.1

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ m
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s

Tactic:
have h_mem := csInf_mem h_nonempty

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty
h_mem : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s}
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
j : ℕ
hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N
hj₂ : f j ω ∈ Set.Ici b
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω

Tactic:
ih.2

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
j : ℕ
hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N
hj₂ : f j ω ∈ Set.Ici b
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) M ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Add ι
inst✝⁴ : LinearOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : Countable ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ IsStoppingTime f fun ω ↦ τ ω + ↑i

Tactic:
intro j
  have h : {ω | τ ω + i ≤ j} = ⋃ k : {k | k + i ≤ j}, {ω | τ ω = k} := by
    ext ω
    simp only [Set.mem_ofPred_eq, Set.mem_iUnion]
    cases τ ω with
    | top => simp
    | coe a => simp; norm_cast
  exact h ▸ MeasurableSet.iUnion fun k => hτ.measurableSet_eq_le (le_of_add_le_left k.2)

Goal state after:
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
⊢ 0 ≤ ∫ (a : Ω), (fun ω ↦ (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (f (i + 1) - f i)) ω) a ∂μ

Tactic:
simp only [Finset.sum_apply]

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
⊢ 0 ≤ ∫ (a : Ω), ∑ c ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑c ∧ ↑c < π ω}.indicator (f (c + 1) - f c) a ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | π ω ≤ ↑i})

pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ s ∩ {ω | π ω ≤ ↑i} = s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | π ω ≤ ↑i}

Tactic:
· exact (hs.2 i).inter (hπ i)

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ s ∩ {ω | π ω ≤ ↑i} = s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | π ω ≤ ↑i}
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:
by
      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.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ ∀ᵐ (ω : Ω) ∂μ, stoppedAbove f r i ω ≤ r + ↑R

Tactic:
filter_upwards [hbdd] with ω hbddω
  rw [stoppedAbove, stoppedProcess, ENat.some_eq_natCast]
  by_cases h_zero : (min (i : ℕ∞) (leastGE f r ω)).untopA = 0
  · simp only [h_zero, hf0, Pi.zero_apply]
    positivity
  obtain ⟨k, hk⟩ := Nat.exists_eq_add_one_of_ne_zero h_zero
  rw [hk, add_comm r, ← sub_le_iff_le_add]
  have := notMem_of_lt_hittingAfter (?_ : k < leastGE f r ω)
  · simp only [bot_eq_zero, zero_le, Set.mem_Ici, not_le, forall_const] at this
    exact (sub_lt_sub_left this _).le.trans ((le_abs_self _).trans (hbddω _))
  · suffices (k : ℕ∞) < min (i : ℕ∞) (leastGE f r ω) from this.trans_le (min_le_right _ _)
    have h_top : min (i : ℕ∞) (leastGE f r ω) ≠ ⊤ :=
      ne_top_of_le_ne_top (by simp) (min_le_left _ _)
    lift min (i : ℕ∞) (leastGE f r ω) to ℕ using h_top with p
    simp only [untopD_coe_enat, Nat.cast_lt, gt_iff_lt] at *
    lia

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
X Y : Ω → ℝ
hXY : X =ᵐ[μ] Y
⊢ ∫ (x : Ω), ((X - fun x ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x ∂μ = ∫ (x : Ω), ((Y - fun x ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x ∂μ

Tactic:
refine integral_congr_ae ?_

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
X Y : Ω → ℝ
hXY : X =ᵐ[μ] Y
⊢ (X - fun x ↦ ∫ (a : Ω), Y a ∂μ) ^ p =ᵐ[μ] (Y - fun x ↦ ∫ (a : Ω), Y a ∂μ) ^ p
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
this : MemLp (fun ω ↦ ∑ i ∈ s with i < n, {a | τ a = ↑i}.indicator (u i) ω) p μ
ω : Ω
⊢ (∑ i ∈ s with i < n, {ω | τ ω = ↑i}.indicator (u i)) ω = ∑ i ∈ s with i < n, {a | τ a = ↑i}.indicator (u i) ω

Tactic:
simp only [Finset.sum_apply]

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

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

Tactic:
abs_of_nonneg ht_nonneg

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (fun ω ↦ rexp (t * |X ω| + v * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (fun ω ↦ rexp (|t| * |X ω|)) μ

Tactic:
abs_of_nonneg ht_nonneg

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (fun ω ↦ rexp (t * |X ω|)) μ
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:
rw [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:
rw [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.Moments.IntegrableExpMul

Goal state before:
pp: case inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : 0 < t
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
rw [abs_of_nonneg ht_pos.le]
    exact rpow_abs_le_mul_max_exp_of_pos x hp ht_pos

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᵐ[ℙ] gaussianPDFReal μ v
⊢ √((2 * π * ↑v)⁻¹ * (π / ((↑v)⁻¹ * 2⁻¹))) = 1

Tactic:
simp [field]

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

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

Tactic:
simp only [gaussianPDFReal]
  rw [sub_add_eq_sub_sub_swap]

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

Goal state before:
pp: Ω : 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
⊢ Integrable (fun a ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ

Tactic:
by
  have ht : t ≠ 0 := by
    suffices |t| ≠ 0 by simpa
    exact (h_nonneg.trans_lt hx).ne'
  have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ h_int_pos h_int_neg
  swap; · rw [← sub_ne_zero]; simp [ht]
  rw [← integrable_norm_iff]
  swap; · fun_prop
  simp only [norm_mul, norm_eq_abs, abs_exp]
  have h_le a : |X a| ^ p * exp (v * X a + x * |X a|)
      ≤ (p / (|t| - x)) ^ p * exp (v * X a + |t| * |X a|) := by
    simp_rw [exp_add, mul_comm (exp (v * X a)), ← mul_assoc]
    gcongr ?_ * _
    have : |t| = |t| - x + x := by simp
    nth_rw 2 [this]
    rw [add_mul, exp_add, ← mul_assoc]
    gcongr ?_ * _
    convert! rpow_abs_le_mul_exp_abs (X a) hp (t := |t| - x) _ using 4
    · nth_rw 2 [abs_of_nonneg]
      simp [hx.le]
    · nth_rw 2 [abs_of_nonneg]
      simp [hx.le]
    · rw [sub_ne_zero]
      exact hx.ne'
  refine Integrable.mono (g := fun a ↦ (p / (|t| - x)) ^ p * exp (v * X a + |t| * |X a|))
    ?_ ?_ <| ae_of_all _ fun ω ↦ ?_
  · refine Integrable.const_mul ?_ _
    simp_rw [add_comm (v * X _)]
    exact integrable_exp_abs_mul_abs_add h_int_pos h_int_neg
  · fun_prop
  · simp only [norm_mul, norm_eq_abs, abs_exp]
    simp_rw [abs_rpow_of_nonneg (abs_nonneg _), abs_abs]
    refine (h_le ω).trans_eq ?_
    congr
    symm
    simp only [abs_eq_self]
    positivity [sub_nonneg_of_le hx.le]

Goal state after:
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 (fun i ↦ -X i) (gaussianReal (-μ) v) P

Tactic:
← Function.comp_def

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
this : ↑↑v ≠ 0
⊢ -↑μ ^ 2 / (2 * ↑↑v) - (z + ↑μ / ↑↑v) ^ 2 / (4 * -↑↑(2 * v)⁻¹) = z * ↑μ + ↑↑v * z ^ 2 / 2

Tactic:
simp [field]

Goal state after:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
this : ↑↑v ≠ 0
⊢ -(↑μ ^ 2 * 4) + 2 ^ 2 * (↑↑v * z + ↑μ) ^ 2 = 4 * ↑↑v * z * (↑μ * 2 + ↑↑v * z)
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✝ : IsFiniteMeasure μ
⊢ IsGaussian μ ↔ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)

Tactic:
refine ⟨fun h ↦ h.charFunDual_eq, fun h ↦ ⟨fun L ↦ Measure.ext_of_charFun ?_⟩⟩

Goal state after:
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
⊢ charFun (Measure.map (⇑L) μ) = charFun (gaussianReal (∫ (x : E), L x ∂μ) Var[⇑L; μ].toNNReal)
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
μ : Measure E
inst✝ : IsGaussian μ
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp (-↑Var[⇑L; μ] / 2)

Tactic:
simp [charFunDual_eq L, integral_complex_ofReal, hμ L, neg_div]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ (⋯.toContinuousLinearMap (MemLp.toLp ⇑L₁ ⋯)) (MemLp.toLp ⇑L₂ ⋯) = ∫ (x : E), L₁ x * L₂ x ∂μ

Tactic:
refine integral_congr_ae ?_

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ (fun a ↦ ↑↑(MemLp.toLp ⇑L₁ ⋯, MemLp.toLp ⇑L₂ ⋯).2 a * ↑↑(MemLp.toLp ⇑L₁ ⋯, MemLp.toLp ⇑L₂ ⋯).1 a) =ᵐ[μ] fun x ↦
    L₁ x * L₂ x
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case ha
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 : ℕ → ℝ := ⋯
c : ℝ≥0∞ := ⋯
C : ℝ := ⋯
x : E
hx : x ∈ closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
⊢ 0 ≤ C

pp: case hab
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 : ℕ → ℝ := ⋯
c : ℝ≥0∞ := ⋯
C : ℝ := ⋯
x : E
hx : x ∈ closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
⊢ ‖x‖ ≤ t (n + 1)

Tactic:
· exact mul_nonneg (logRatio_pos ha_gt ha_lt).le (by positivity)

Goal state after:
case hab
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 : ℕ → ℝ := ⋯
c : ℝ≥0∞ := ⋯
C : ℝ := ⋯
x : E
hx : x ∈ closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
⊢ ‖x‖ ≤ t (n + 1)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ IsSelfAdjoint (toEuclideanCLM (CFC.sqrt S))

Tactic:
exact (CFC.sqrt_nonneg S).isSelfAdjoint.map _

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
⊢ cov[fun x ↦ x.ofLp s, fun x ↦ x.ofLp t; multivariateGaussian 0 (covMatrix I)] = ↑(min ↑s ↑t)

Tactic:
covariance_eval_multivariateGaussian (posSemidef_covMatrix I),

Goal state after:
I : Finset ℝ≥0
s t : ↥I
⊢ covMatrix I s t = ↑(min ↑s ↑t)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case hv
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ((covarianceBilin
          (Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm)
            (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)))
        x)
      x =
    ((covarianceBilin (Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm) (projectiveFamily I))) x) x

Tactic:
rw [PiLp.coe_symm_continuousLinearEquiv, covarianceBilin_apply_pi, covarianceBilin_apply_pi]

Goal state after:
case hv
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ∑ i, ∑ j, x.ofLp i * x.ofLp j * cov[fun ω ↦ ω i, fun ω ↦ ω j; Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P] =
    ∑ i, ∑ j, x.ofLp i * x.ofLp j * cov[fun ω ↦ ω i, fun ω ↦ ω j; projectiveFamily I]

case hv.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ∀ (i : ↥I), MemLp (fun ω ↦ ω i) 2 (projectiveFamily I)

case hv.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ∀ (i : ↥I), MemLp (fun ω ↦ ω i) 2 (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)