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

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

Tactic:
constructor

Goal state after:
case mp
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossings a b f ω < ∞ → ∃ k, upcrossings a b f ω ≤ ↑k

case mpr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ (∃ k, upcrossings a b f ω ≤ ↑k) → upcrossings a b f ω < ∞
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
⊢ (∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k) ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
constructor

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

case mpr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ (∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k) → ∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
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 π
s : Set Ω
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω}) ↔ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Tactic:
constructor

Goal state after:
case mp
Ω : 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 π
s : Set Ω
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω}) → MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

case mpr
Ω : 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 π
s : Set Ω
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω}) → MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
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 π
j : ι
⊢ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ ↑j} = {ω | min (τ ω) ↑j ≤ min (π ω) ↑j} ∩ {ω | τ ω ≤ ↑j}

Tactic:
ext

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 π
j : ι
x✝ : Ω
⊢ x✝ ∈ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ ↑j} ↔ x✝ ∈ {ω | min (τ ω) ↑j ≤ min (π ω) ↑j} ∩ {ω | τ ω ≤ ↑j}
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✝¹ : OrderTopology ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ {ω | τ ω = π ω} = {ω | τ ω ≤ π ω} ∩ {ω | π ω ≤ τ ω}

Tactic:
ext

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
x✝ : Ω
⊢ x✝ ∈ {ω | τ ω = π ω} ↔ x✝ ∈ {ω | τ ω ≤ π ω} ∩ {ω | π ω ≤ τ ω}
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✝¹ : OrderTopology ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : {ω | τ ω = π ω} = {ω | τ ω ≤ π ω} ∩ {ω | π ω ≤ τ ω}
x✝ : Ω
⊢ min (τ x✝) (π x✝) = min (π x✝) (τ x✝)

Tactic:
rw [min_comm]

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

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

Tactic:
ext

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
inst✝ : Bot ι
x✝ : Ω
⊢ stoppedValue u (fun x ↦ ⊥) x✝ = u ⊥ x✝
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case hg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ Integrable (fun ω ↦ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω) μ

Tactic:
refine hsub.integrable_stoppedValue ?_ (fun ω ↦ mod_cast hittingBtwn_le ω)

Goal state after:
case hg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IsStoppingTime 𝒢 fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)
Module: Mathlib.Probability.Process.Stopping

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

Tactic:
ext

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝² : Nonempty ι
u : ι → Ω → β
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
x✝¹ : ι
x✝ : Ω
⊢ stoppedProcess u (fun x ↦ ⊥) x✝¹ x✝ = u ⊥ x✝
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

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
inst✝ : LinearOrder ι
x✝¹ : ι
x✝ : Ω
⊢ stoppedProcess u (fun x ↦ ⊤) x✝¹ x✝ = u x✝¹ x✝
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun f μ
hij : i < j
⊢ Indep (MeasurableSpace.comap (f j) mβ) (↑(Filtration.natural f hf) i) μ

Tactic:
suffices Indep (⨆ k ∈ ({j} : Set ι), MeasurableSpace.comap (f k) mβ)
      (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ by rwa [iSup_singleton] at this
  exact indep_iSup_of_disjoint (fun k => (hf k).measurable.comap_le) hfi (by simpa)

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : 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)

Tactic:
have hgbdd : ∀ᵐ ω ∂μ, ∀ i : ℕ, |g (i + 1) ω - g i ω| ≤ ↑R := by
    simpa only [g, sub_sub_sub_cancel_right]

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
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: 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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
⊢ Measurable (sᶜ.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))

Tactic:
suffices h_min_eq_left :
      (fun x : sc => min (↑(x : Set.Iic i × Ω).fst) (τ (x : Set.Iic i × Ω).snd)) = fun x : sc =>
        ↑(x : Set.Iic i × Ω).fst by
      simp +unfoldPartialApp only [sc, Set.domRestrict, h_min_eq_left]
      exact (h_meas_fst _).withTop_coe

Goal state after:
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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
⊢ (fun x ↦ min (↑↑(↑x).1) (τ (↑x).2)) = fun x ↦ ↑↑(↑x).1
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
⊢ mgf X 0 = 0

Tactic:
ext

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
x✝ : ℝ
⊢ mgf X 0 x✝ = 0 x✝
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
⊢ cgf X 0 = 0

Tactic:
ext

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
x✝ : ℝ
⊢ cgf X 0 x✝ = 0 x✝
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ μ.real Set.univ ≠ 0

Tactic:
rw [Ne, measureReal_eq_zero_iff, Measure.measure_univ_eq_zero]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ ¬μ = 0
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : IsZeroOrProbabilityMeasure 0
⊢ cgf X 0 0 = 0

Tactic:
simp [cgf_zero']

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

Goal state before:
pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ cgf X μ 0 = 0

Tactic:
simp [cgf_zero']

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
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)
⊢ (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)

Tactic:
constructor

Goal state after:
case mp
Ω : 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)
⊢ (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) → ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)

case mpr
Ω : 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)
⊢ (∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)) → ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
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 : Ω
ω : ι
⊢ ω ∈ s ∧ τ y = ↑ω ↔ ω = (τ y).untopA

Tactic:
constructor

Goal state after:
case mp
Ω : 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 : Ω
ω : ι
⊢ ω ∈ s ∧ τ y = ↑ω → ω = (τ y).untopA

case mpr
Ω : 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 : Ω
ω : ι
⊢ ω = (τ y).untopA → ω ∈ s ∧ τ y = ↑ω
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 ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t

Tactic:
rw [mgf_undef htY]
    exact mgf_nonneg

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
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)
⊢ BddAbove (Set.range fun n ↦ (-f) n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)

Tactic:
constructor

Goal state after:
case mp
Ω : 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)
⊢ BddAbove (Set.range fun n ↦ (-f) n ω) → BddBelow (Set.range fun n ↦ f n ω)

case mpr
Ω : 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)
⊢ BddBelow (Set.range fun n ↦ f n ω) → BddAbove (Set.range fun n ↦ (-f) n ω)
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), Measurable (X i)
h_int : ∀ i ∈ ∅, Integrable (fun ω ↦ rexp (t * X i ω)) μ
⊢ Integrable (fun ω ↦ 1) μ

Tactic:
exact integrable_const _

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

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ

pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -|u| ≤ t

pp: case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ t ≤ |u|

Tactic:
· rcases le_total 0 u with hu | hu
    · rwa [abs_of_nonneg hu]
    · rwa [abs_of_nonpos hu]

Goal state after:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -|u| ≤ t

case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ t ≤ |u|
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
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
⊢ Integrable (stoppedValue u τ) μ

Tactic:
simp_rw [← memLp_one_iff_integrable] at hu ⊢

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
hu : ∀ (n : ι), MemLp (u n) 1 μ
⊢ MemLp (stoppedValue u τ) 1 μ
Module: Mathlib.Probability.Martingale.BorelCantelli

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

Tactic:
constructor

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

case mpr
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
ω : Ω
hω₁ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
⊢ Tendsto (fun n ↦ predictablePart f ℱ μ n ω) atTop atTop → Tendsto (fun n ↦ f n ω) atTop atTop
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
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ Integrable (stoppedProcess u τ n) μ

Tactic:
simp_rw [← memLp_one_iff_integrable] at hu ⊢

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
hu : ∀ (n : ι), MemLp (u n) 1 μ
⊢ MemLp (stoppedProcess u τ n) 1 μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
⊢ gaussianPDF μ 0 = 0

Tactic:
ext

Goal state after:
μ x✝ : ℝ
⊢ gaussianPDF μ 0 x✝ = 0 x✝
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 ∈ Set.Ioo l u

Tactic:
constructor

Goal state after:
case left
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ l < v + min (v - l) (u - v) / 2

case right
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 < u