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

Goal state before:
pp: case pos.refine_1
Ω : 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 < ∞
⊢ AEStronglyMeasurable f μ

pp: case pos.refine_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ (c : E) ⦃s_1 : Set Ω⦄,
    MeasurableSet s_1 →
      μ s_1 < ∞ → μ.real s • ∫ (x : Ω), s_1.indicator (fun x ↦ c) x ∂μ = ∫ (x : Ω) in s, s_1.indicator (fun x ↦ c) x ∂μ

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 < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
                μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  μ.real s • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ

pp: case pos.refine_4
Ω : 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 < ∞
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

pp: case pos.refine_5
Ω : 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 < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      MemLp f 1 μ →
        μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ

Tactic:
·

Goal state after:
case pos.refine_1
Ω : 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 < ∞
⊢ AEStronglyMeasurable f μ
Module: Mathlib.Probability.ConditionalExpectation

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

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 < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
                μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  μ.real s • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ

pp: case pos.refine_4
Ω : 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 < ∞
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

pp: case pos.refine_5
Ω : 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 < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      MemLp f 1 μ →
        μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ

Tactic:
·

Goal state after:
case pos.refine_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ (c : E) ⦃s_1 : Set Ω⦄,
    MeasurableSet s_1 →
      μ s_1 < ∞ → μ.real s • ∫ (x : Ω), s_1.indicator (fun x ↦ c) x ∂μ = ∫ (x : Ω) in s, s_1.indicator (fun x ↦ c) x ∂μ
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 : ℕ
⊢ ENNReal.ofReal
      (∫ (x : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ∪ {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε},
        stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) x ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω), stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ)

pp: case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ Disjoint {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}

pp: case ht
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ MeasurableSet {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}

pp: case hfs
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} μ

pp: case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε} μ

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

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

Tactic:
·

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

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : τ ω = ⊤
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : τ ω = ⊤
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : σ ω = ⊤
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : σ ω = ⊤
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ u ((↑(min (↑i) (σ ω)).untopA).untop ⋯) ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ ↑(min (↑i) (σ ω)).untopA ≤ τ ω

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ u ((↑(min (↑i) (σ ω)).untopA).untop ⋯) ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ Disjoint {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}

pp: case ht
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ MeasurableSet {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}

pp: case hfs
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} μ

pp: case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε} μ

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

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

Tactic:
·

Goal state after:
case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ Disjoint {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ ↑(min (↑i) (σ ω)).untopA ≤ τ ω

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ ↑(min (↑i) (σ ω)).untopA ≤ τ ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case ht
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ MeasurableSet {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}

pp: case hfs
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} μ

pp: case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε} μ

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

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

Tactic:
·

Goal state after:
case ht
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ MeasurableSet {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (↑((min (↑i) (σ ω)).untop ?neg✝)) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ min (↑i) (σ ω) ≠ ⊤

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (↑((min (↑i) (σ ω)).untop ?neg✝)) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω
Module: Mathlib.Probability.Martingale.OptionalStopping

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

pp: case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε} μ

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

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

Tactic:
·

Goal state after:
case hfs
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f 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 < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
                μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  μ.real s • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ

pp: case pos.refine_4
Ω : 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 < ∞
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

pp: case pos.refine_5
Ω : 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 < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      MemLp f 1 μ →
        μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ

Tactic:
·

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 < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
                μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  μ.real s • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ
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 ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
hωb : (upperBounds (Set.range fun n ↦ f n ω)).Nonempty
i : ℕ
hi : hωb.some < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ f (min ↑n ⊤).untopA ω = f n ω

pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
hωb : (upperBounds (Set.range fun n ↦ f n ω)).Nonempty
i : ℕ
hi : hωb.some < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ ∀ (j : ℕ), ⊥ ≤ j → f j ω ∉ Set.Ici ↑i

Tactic:
·

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
hωb : (upperBounds (Set.range fun n ↦ f n ω)).Nonempty
i : ℕ
hi : hωb.some < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ f (min ↑n ⊤).untopA ω = f n ω