mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case right.a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f a y

Tactic:
apply iSup₂_mono

Goal state after:
case right.a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ∀ i ∈ Y, ⨅ x ∈ X, f x i ≤ f a i
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x y : α
u : Set α
P : Partition u
hx : x ∈ u
hy : y ∈ u
⊢ P.Rel x y ↔ P.partOf x = P.partOf y

Tactic:
refine ⟨fun ⟨t, htP, hxt, hyt⟩ ↦ eq_partOf_of_mem (P.partOf_mem hx) ?_,
    fun h ↦ ⟨P.partOf x, P.partOf_mem hx, P.mem_partOf hx, h ▸ mem_partOf hy⟩⟩

Goal state after:
α : Type u_1
x y : α
u : Set α
P : Partition u
hx : x ∈ u
hy : y ∈ u
x✝ : P.Rel x y
t : Set α
htP : t ∈ P
hxt : x ∈ t
hyt : y ∈ t
⊢ y ∈ P.partOf x
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
⊢ type α ≠ 0 ↔ Nonempty α

Tactic:
by simp [type_eq_zero]

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b < findAtom r
⊢ b = ⊥

Tactic:
apply Order.le_pred_of_lt at hb

Goal state after:
case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b ≤ Order.pred (findAtom r)
⊢ b = ⊥
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : OpensMeasurableSpace β
hu : IsProgressive f u
i : ι
⊢ Measurable fun p ↦ (fun t ω ↦ ‖u t ω‖) (↑p.1) p.2

Tactic:
apply @(hu i).norm

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : OpensMeasurableSpace β
hu : IsProgressive f u
i : ι
⊢ OpensMeasurableSpace β
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
k : ℕ
hk : i ≤ k
this : μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] μ[f (k + 1) - f k | ↑ℱ i]
x : Ω
hx : μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] x = μ[f (k + 1) - f k | ↑ℱ i] x
⊢ (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i]) x = 0 x

Tactic:
Pi.sub_apply,

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
k : ℕ
hk : i ≤ k
this : μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] μ[f (k + 1) - f k | ↑ℱ i]
x : Ω
hx : μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] x = μ[f (k + 1) - f k | ↑ℱ i] x
⊢ μ[f (k + 1) - f k | ↑ℱ i] x - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] x = 0 x
Module: Mathlib.Probability.Martingale.Centering

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✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted ℱ fun n ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
ω : Ω
hω : (f n - martingalePart (f + g) ℱ μ n) ω = (f - martingalePart (f + g) ℱ μ) 0 ω
⊢ (f - martingalePart (f + g) ℱ μ) 0 ω = 0 ω

Tactic:
Pi.sub_apply,

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted ℱ fun n ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
ω : Ω
hω : (f n - martingalePart (f + g) ℱ μ n) ω = (f - martingalePart (f + g) ℱ μ) 0 ω
⊢ (f 0 - martingalePart (f + g) ℱ μ 0) ω = 0 ω
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
i : ι
⊢ m ≤ i → i ≤ m → u i ω ∈ s → sInf ({m} ∩ {i | u i ω ∈ s}) = m

Tactic:
hi₁

Goal state after:
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
⊢ i ≤ m → u i ω ∈ s → sInf ({m} ∩ {i | u i ω ∈ s}) = m
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono fun n ↦ upperCrossingTime a b f N n ω
k : ℕ
hk : N < (fun n ↦ upperCrossingTime a b f N n ω) k
⊢ False

Tactic:
exact not_le.2 hk upperCrossingTime_le

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ upperCrossingTime a b f N N ω = N

Tactic:
by
  by_cases hN' : N < Nat.find (exists_upperCrossingTime_eq f N ω hab)
  · refine le_antisymm upperCrossingTime_le ?_
    have hmono : StrictMonoOn (fun n => upperCrossingTime a b f N n ω)
        (Set.Iic (Nat.find (exists_upperCrossingTime_eq f N ω hab)).pred) := by
      refine strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_
      rw [Nat.lt_pred_iff] at hm
      convert! Nat.find_min _ hm
    convert! StrictMonoOn.Iic_id_le hmono N (Nat.le_sub_one_of_lt hN')
  · rw [not_lt] at hN'
    exact upperCrossingTime_stabilize hN' (Nat.find_spec (exists_upperCrossingTime_eq f N ω hab))

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ -
      ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ

Tactic:
Finset.sum_range_sub,

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ -
      ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), (f n - f 0) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, a_1 ≤ b ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, a ≤ b_1 ∧ b < f b_1 ω
⊢ ∃ N, 0 ≤ upcrossingsBefore a b f N ω

Tactic:
simp only [zero_le, exists_const]

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

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ x ∈ Finset.range N,
      ∑ x_1 ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N x_1 ω) (upperCrossingTime a b f N (x_1 + 1) ω)).indicator
          (fun j ↦ 1 * (f (j + 1) - f j) ω) x

Tactic:
Pi.sub_apply,

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ x ∈ Finset.range N,
      ∑ x_1 ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N x_1 ω) (upperCrossingTime a b f N (x_1 + 1) ω)).indicator
          (fun j ↦ 1 * (f (j + 1) ω - f j ω)) x
Module: Mathlib.Probability.Martingale.Upcrossing

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

Tactic:
refine ⟨k, fun N => ?_⟩

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

Goal state before:
pp: case pos.refine_3
Ω : 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 : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
a✝ : Disjoint (Function.support u) (Function.support v)
huint : Integrable u μ
hvint : Integrable v μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
hv_eq : μ.real s • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
⊢ ∫ (x : Ω) in s, u x ∂μ + ∫ (x : Ω) in s, v x ∂μ = ∫ (x : Ω) in s, (u + v) x ∂μ

Tactic:
integral_add' huint.integrableOn hvint.integrableOn

Goal state after:
case pos.refine_3
Ω : 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 : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
a✝ : Disjoint (Function.support u) (Function.support v)
huint : Integrable u μ
hvint : Integrable v μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
hv_eq : μ.real s • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
⊢ ∫ (x : Ω) in s, u x ∂μ + ∫ (x : Ω) in s, v x ∂μ = ∫ (a : Ω) in s, u a ∂μ + ∫ (a : Ω) in s, v a ∂μ
Module: Mathlib.Probability.Martingale.BorelCantelli

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

Tactic:
have hg0 : g 0 = 0 := by
    ext ω
    simp only [g, sub_self, Pi.zero_apply]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (fun ω ↦ α + X ω) μ t = rexp (t * α) * mgf X μ t

Tactic:
rw [mgf, mgf, ← integral_const_mul]
  congr with x
  dsimp
  rw [mul_add, exp_add]

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

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : τ ω < ↑n
⊢ stoppedProcess u τ n ω = {a | ↑n ≤ τ a}.indicator (u n) ω + ∑ c ∈ s with c < n, {ω | τ ω = ↑c}.indicator (u c) ω

Tactic:
rw [stoppedProcess_eq_of_ge (le_of_lt h)]

Goal state after:
case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : τ ω < ↑n
⊢ u (τ ω).untopA ω = {a | ↑n ≤ τ a}.indicator (u n) ω + ∑ c ∈ s with c < n, {ω | τ ω = ↑c}.indicator (u c) ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), ↑(π ω) ≠ ∞
ω : Ω
h_le' : untopA (τ ω) ≤ untopA (π ω)
⊢ (stoppedValue u π - stoppedValue u τ) ω =
    (∑ k ∈ Finset.range (untopA (π ω)), (u (k + 1) - u k) - ∑ k ∈ Finset.range (untopA (τ ω)), (u (k + 1) - u k)) ω

Tactic:
Finset.sum_range_sub,

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), ↑(π ω) ≠ ∞
ω : Ω
h_le' : untopA (τ ω) ≤ untopA (π ω)
⊢ (stoppedValue u π - stoppedValue u τ) ω =
    (u (untopA (π ω)) - u 0 - ∑ k ∈ Finset.range (untopA (τ ω)), (u (k + 1) - u k)) ω
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e_a.e_a.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))
⊢ t * 1 = t

Tactic:
mul_one

Goal state after:
case e_a.e_a.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))
⊢ t = t
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e_a.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))
⊢ t * 1 = t

Tactic:
mul_one

Goal state after:
case e_a.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))
⊢ t = t
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case e_a
Ω : 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 ω) ∂μ) v * 1 / mgf X μ v =
    deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v

pp: case e_a
Ω : 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 ∂μ
⊢ mgf X μ v ≠ 0

Tactic:
mul_one

Goal state after:
case e_a
Ω : 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 ω) ∂μ) v / mgf X μ v =
    deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v

case e_a
Ω : 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 ∂μ
⊢ mgf X μ v ≠ 0
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
this : ∀ (x : ℝ), HasDerivAt (fun x ↦ c⁻¹ * x) (c⁻¹ * 1) x
⊢ ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x

Tactic:
mul_one

Goal state after:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
this : ∀ (x : ℝ), HasDerivAt (fun x ↦ c⁻¹ * x) c⁻¹ x
⊢ ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

Tactic:
by_cases hv : v = 0
  · simp [hv, mul_zero, gaussianReal_zero_var]
  by_cases hc : c = 0
  · simp [hc, zero_mul]
  let e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
  have he' : ∀ x, HasDerivAt e ((fun _ ↦ c⁻¹) x) x := by
    suffices ∀ x, HasDerivAt (fun x => c⁻¹ * x) (c⁻¹ * 1) x by rwa [mul_one] at this
    exact fun _ ↦ HasDerivAt.const_mul _ (hasDerivAt_id _)
  change (gaussianReal μ v).map e.symm = gaussianReal (c * μ) (.mk (c ^ 2) (sq_nonneg _) * v)
  ext s' hs'
  rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs',
    gaussianReal_apply_eq_integral _ _ s']
  swap
  · simp only [ne_eq, mul_eq_zero, hv, or_false]
    rw [← NNReal.coe_inj]
    simp [hc]
  simp only [e, Homeomorph.mulLeft₀,
    Equiv.mulLeft₀_symm_apply, Homeomorph.toMeasurableEquiv_coe, Homeomorph.homeomorph_mk_coe_symm,
    gaussianPDFReal_inv_mul hc]
  congr with x
  suffices |c⁻¹| * |c| = 1 by rw [← mul_assoc, this, one_mul]
  rw [abs_inv, inv_mul_cancel₀]
  rwa [ne_eq, abs_eq_zero]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
⊢ covarianceBilin (Measure.map (fun x ↦ c + x) μ) = covarianceBilin μ

Tactic:
by_cases h : MemLp id 2 μ
  · ext x y
    have h_Lp : MemLp id 2 (μ.map (fun x ↦ c + x)) :=
      (measurableEmbedding_addLeft _).memLp_map_measure_iff.mpr <| (memLp_const c).add h
    rw [covarianceBilin_apply h_Lp,
      covarianceBilin_apply h, integral_map (by fun_prop) (by fun_prop)]
    congr with z
    rw [integral_map (by fun_prop) h_Lp.1]
    simp only [id_eq]
    rw [integral_add (integrable_const _)]
    · simp
    · exact h.integrable (by simp)
  · ext
    rw [covarianceBilin_of_not_memLp, covarianceBilin_of_not_memLp h]
    rw [(measurableEmbedding_addLeft _).memLp_map_measure_iff.not]
    contrapose h
    convert! (memLp_const (-c)).add h
    ext; simp

Goal state after:
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 μ
c : E
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2 + ↑(L c) * I) =
    cexp ((∫ (x : E), ↑(L x) ∂Measure.map (fun x ↦ x + c) μ) * I - ↑Var[⇑L ∘ fun x ↦ x + c; μ] / 2)

Tactic:
integral_map (by fun_prop) (by fun_prop),

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 μ
c : E
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2 + ↑(L c) * I) =
    cexp ((∫ (x : E), ↑(L (x + c)) ∂μ) * I - ↑Var[⇑L ∘ fun x ↦ x + c; μ] / 2)
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:
simp [Nat.find_spec h, hx]

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

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
⊢ ∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ ≤ ∫⁻ (x : E), ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal ∂μ

Tactic:
refine lintegral_mono fun x ↦ ?_
    rw [← ENNReal.mul_rpow_of_nonneg]
    swap; · positivity
    gcongr
    exact L.le_opENorm x

Goal state after:
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
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ (√2)⁻¹ * 1 = (√2)⁻¹

Tactic:
mul_one

Goal state after:
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 : ℝ
⊢ (√2)⁻¹ = (√2)⁻¹
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✝ : BorelSpace E
h : ¬MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ((covarianceBilinDual μ) L₁) L₂ = 0

Tactic:
covarianceBilinDual,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
h : ¬MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ((uncenteredCovarianceBilinDual (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)) L₁) L₂ = 0