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

Goal state before:
pp: case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ (f i ω - a)⁺ + a}) =
    sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})

Tactic:
← sub_le_iff_le_add,

Goal state after:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b - a ≤ (f i ω - a)⁺}) =
    sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})
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✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet (Set.univ ∩ {ω | τ ω = ↑i})

Tactic:
measurableSet_inter_eq_iff,

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet (Set.univ ∩ {ω | τ ω = ↑i})
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✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
x✝ : WithTop ι
⊢ ↑i < x✝ ∨ ↑i = x✝ ↔ x✝ = ↑i ∨ ↑i < x✝

Tactic:
cases τ ω with

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet (Set.univ ∩ {ω | τ ω = ↑i})

Tactic:
measurableSet_inter_eq_iff,

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet (Set.univ ∩ {ω | τ ω = ↑i})
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
x✝ : WithTop ι
⊢ ↑i < x✝ ∨ ↑i = x✝ ↔ x✝ = ↑i ∨ ↑i < x✝

Tactic:
cases τ ω with

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

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

Tactic:
refine ⟨measurableSet_le hτ.measurable_iSup hπ.measurable_iSup, fun j ↦ ?_⟩

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 : ι
⊢ MeasurableSet ({ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ ↑j})
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n ↦ μ[g | ↑ℱ n] x) atTop (𝓝 (μ[g | ⨆ n, ↑ℱ n] x))

Tactic:
by
  have ht : ∀ᵐ x ∂μ, Tendsto (fun n => (μ[μ[g | ⨆ n, ℱ n] | ℱ n]) x)
      atTop (𝓝 ((μ[g | ⨆ n, ℱ n]) x)) :=
    integrable_condExp.tendsto_ae_condExp stronglyMeasurable_condExp
  have heq : ∀ n, ∀ᵐ x ∂μ, (μ[μ[g | ⨆ n, ℱ n] | ℱ n]) x = (μ[g | ℱ n]) x := fun n =>
    condExp_condExp_of_le (le_iSup _ n) (iSup_le fun n => ℱ.le n)
  rw [← ae_all_iff] at heq
  filter_upwards [heq, ht] with x hxeq hxt
  exact hxt.congr hxeq

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n ↦ eLpNorm (μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] x = μ[g | ↑ℱ n] x
n : ℕ
x : Ω
hxeq : μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] x = μ[g | ↑ℱ n] x
⊢ (μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n]) x = (μ[g | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n]) x

Tactic:
simp only [hxeq, Pi.sub_apply]

Goal state after:
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos
Ω : 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 : Integrable f μ
⊢ μ[f | m₂] =ᵐ[μ] fun x ↦ ∫ (x : Ω), f x ∂μ

pp: case neg
Ω : 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 : ¬Integrable f μ
⊢ μ[f | m₂] =ᵐ[μ] fun x ↦ ∫ (x : Ω), f x ∂μ

Tactic:
swap

Goal state after:
case neg
Ω : 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 : ¬Integrable f μ
⊢ μ[f | m₂] =ᵐ[μ] fun x ↦ ∫ (x : Ω), f x ∂μ

case pos
Ω : 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 : Integrable f μ
⊢ μ[f | m₂] =ᵐ[μ] fun x ↦ ∫ (x : Ω), f x ∂μ
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 : σ ≤ τ
⊢ stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u σ

Tactic:
simp [h]

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 : τ ≤ σ
⊢ stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u τ

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  {ω |
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑(filtrationOfSet hsm) k] ω) atTop atTop} =ᵐ[μ]
    Set.univ
⊢ μ {ω | Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑(filtrationOfSet hsm) k] ω) atTop atTop} =
    1

Tactic:
measure_congr this,

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  {ω |
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑(filtrationOfSet hsm) k] ω) atTop atTop} =ᵐ[μ]
    Set.univ
⊢ μ Set.univ = 1
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : 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ᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2

Tactic:
simp [h]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : MeasurableSpace ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : SecondCountableTopology ι
inst✝² : BorelSpace ι
inst✝¹ : TopologicalSpace β
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
i : ι
ω : Ω
x✝ : WithTop ι
⊢ (min (↑i) x✝).untopA ≤ i

Tactic:
cases τ ω with

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

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

Tactic:
h_eq_univ,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
h_eq_univ : (Function.support fun x ↦ rexp (t * X x)) = Set.univ
⊢ 0 < μ (Set.univ ∩ Set.univ)
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)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)

Tactic:
filter_upwards [hup, hdown] with ω hω₁ hω₂

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t = (⋃ n, stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑(seq n)}) ∪ stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}
ω : Ω
h : τ ω = ⊤
⊢ u (untopD (Classical.arbitrary ι) (τ ω)) ω ∈ t ↔ u (Classical.arbitrary ι) ω ∈ t

Tactic:
simp [h]

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

Goal state before:
pp: case inl
Ω : 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 ≤ τ ω
m : ι
hm : m ∈ {i ∈ s | i < n}
⊢ ω ∉ {ω | τ ω = ↑m}

Tactic:
Finset.mem_filter

Goal state after:
case inl
Ω : 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 ≤ τ ω
m : ι
hm : m ∈ s ∧ m < n
⊢ ω ∉ {ω | τ ω = ↑m}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ i ∈ {i ∈ s | i < n}

Tactic:
Finset.mem_filter

Goal state after:
case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ i ∈ s ∧ i < n
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ i ∈ {i ∈ s | i < n}

Tactic:
rw [Finset.mem_filter]
      simp only [Set.mem_image, Finset.mem_coe, coe_eq_coe, exists_eq_right] at hbdd
      exact ⟨hbdd, mod_cast h⟩

Goal state after:
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✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
i : ι
x✝ : i ∈ s
y : Ω
⊢ τ y ∈ WithTop.some '' ↑s

Tactic:
exact hbdd y

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

Goal state before:
pp: case neg.refine_1
Ω : 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 ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
⊢ v + t - (v - t) ≠ 0

Tactic:
simp [ht]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ (fun ω ↦ (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω) = fun ω ↦
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (u (i + 1) - u i)) ω

pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ ∀ (ω : Ω), ↑(π ω) ≠ ∞

Tactic:
swap

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ ∀ (ω : Ω), ↑(π ω) ≠ ∞

Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ (fun ω ↦ (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω) = fun ω ↦
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (u (i + 1) - u i)) ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x ω : Ω
x✝ : ℕ∞
⊢ ↑n + 1 ≤ x✝ ↔ ↑n < x✝

Tactic:
cases τ ω with

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

Goal state before:
pp: case refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ process s n ω) atTop atTop ↔ Tendsto (fun n ↦ predictablePart (process s) ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) atTop atTop

pp: case refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ process s n ω ≤ process s (n + 1) ω

Tactic:
swap

Goal state after:
case refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ process s n ω ≤ process s (n + 1) ω

case refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ process s n ω) atTop atTop ↔ Tendsto (fun n ↦ predictablePart (process s) ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) atTop atTop
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
⊢ MeasurableSet ({ω | τ ω ≤ ↑i} ∩ t) ↔ MeasurableSet ({ω | τ ω ≤ ↑i} ∩ t)

Tactic:
rw [Set.inter_comm _ t, hτ.measurableSet_inter_le_const_iff]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
h_re_of_mem :
  ∀ (n : ℕ),
    ∀ t ∈ interior (integrableExpSet X μ),
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
h_re :
  ∀ (n : ℕ),
    ∀ᶠ (t' : ℝ) in 𝓝 t,
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t' * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
⊢ (↑t).re ∈ interior (integrableExpSet X μ)

Tactic:
simp [ht]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (↑t).re ∈ interior (integrableExpSet X μ)

Tactic:
simp [ht]

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

Goal state before:
pp: case refine_1
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ 0 < |t|

Tactic:
simp [ht]

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

Goal state before:
pp: case refine_2
Ω : 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
ht : t ≠ 0
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ

pp: case refine_1
Ω : 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
ht : t ≠ 0
⊢ v + t ≠ v - t

Tactic:
swap

Goal state after:
case refine_1
Ω : 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
ht : t ≠ 0
⊢ v + t ≠ v - t

case refine_2
Ω : 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
ht : t ≠ 0
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1
Ω : 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
ht : t ≠ 0
⊢ v + t - (v - t) ≠ 0

Tactic:
simp [ht]

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

Goal state before:
pp: case refine_2
Ω : 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
ht : t ≠ 0
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖|X a| ^ p * rexp (v * X a + x * |X a|)‖) μ

pp: case refine_2
Ω : 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
ht : t ≠ 0
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun a ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ

Tactic:
swap

Goal state after:
case refine_2
Ω : 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
ht : t ≠ 0
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun a ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ

case refine_2
Ω : 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
ht : t ≠ 0
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖|X a| ^ p * rexp (v * X a + x * |X a|)‖) μ
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 ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ 0 < |t|

Tactic:
simp [ht]

Goal state after: