[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s : ι → Set Ω
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f
hij : i < j
⊢ Indep (MeasurableSpace.comap (f j) mβ) (↑(Filtration.natural f hf) i)
[PROOFSTEP]
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 
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s : ι → Set Ω
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f
hij : i < j
this :
  Indep (⨆ (k : ι) (_ : k ∈ {j}), MeasurableSpace.comap (f k) mβ)
    (⨆ (k : ι) (_ : k ∈ {k | k ≤ i}), MeasurableSpace.comap (f k) mβ)
⊢ Indep (MeasurableSpace.comap (f j) mβ) (↑(Filtration.natural f hf) i)
[PROOFSTEP]
rwa [iSup_singleton] at this 
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s : ι → Set Ω
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f
hij : i < j
⊢ Indep (⨆ (k : ι) (_ : k ∈ {j}), MeasurableSpace.comap (f k) mβ)
    (⨆ (k : ι) (_ : k ∈ {k | k ≤ i}), MeasurableSpace.comap (f k) mβ)
[PROOFSTEP]
exact indep_iSup_of_disjoint (fun k => (hf k).measurable.comap_le) hfi (by simpa)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s : ι → Set Ω
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f
hij : i < j
⊢ Disjoint {j} {k | k ≤ i}
[PROOFSTEP]
simpa
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
hij : i < j
⊢ μ[Set.indicator (s j) fun x => 1|↑(filtrationOfSet hsm) i] =ᵐ[μ] fun x => ENNReal.toReal (↑↑μ (s j))
[PROOFSTEP]
rw [Filtration.filtrationOfSet_eq_natural (β := ℝ) hsm]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
hij : i < j
⊢ μ[Set.indicator (s j) fun x =>
        1|↑(Filtration.natural (fun i => Set.indicator (s i) fun x => 1)
            (_ : ∀ (i : ι), StronglyMeasurable (Set.indicator (s i) 1)))
        i] =ᵐ[μ]
    fun x => ENNReal.toReal (↑↑μ (s j))
[PROOFSTEP]
refine' (iIndepFun.condexp_natural_ae_eq_of_lt _ hs.iIndepFun_indicator hij).trans _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
hij : i < j
⊢ (fun x => ∫ (x : Ω), Set.indicator (s j) (fun _ω => 1) x ∂μ) =ᵐ[μ] fun x => ENNReal.toReal (↑↑μ (s j))
[PROOFSTEP]
simp only [integral_indicator_const _ (hsm _), Algebra.id.smul_eq_mul, mul_one]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
hij : i < j
⊢ (fun x => ENNReal.toReal (↑↑μ (s j))) =ᵐ[μ] fun x => ENNReal.toReal (↑↑μ (s j))
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
⊢ ↑↑μ (limsup s atTop) = 1
[PROOFSTEP]
rw [measure_congr
    (eventuallyEq_set.2 (ae_mem_limsup_atTop_iff μ <| measurableSet_filtrationOfSet' hsm) :
      (limsup s atTop : Set Ω) =ᵐ[μ]
        {ω |
          Tendsto (fun n => ∑ k in Finset.range n, (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω) atTop
            atTop})]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
⊢ ↑↑μ
      {ω |
        Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑(filtrationOfSet hsm) k]) ω) atTop
          atTop} =
    1
[PROOFSTEP]
suffices
  {ω |
      Tendsto (fun n => ∑ k in Finset.range n, (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω) atTop
        atTop} =ᵐ[μ]
    Set.univ
  by rw [measure_congr this, measure_univ]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  {ω |
      Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑(filtrationOfSet hsm) k]) ω) atTop
        atTop} =ᵐ[μ]
    Set.univ
⊢ ↑↑μ
      {ω |
        Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑(filtrationOfSet hsm) k]) ω) atTop
          atTop} =
    1
[PROOFSTEP]
rw [measure_congr this, measure_univ]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
⊢ {ω |
      Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑(filtrationOfSet hsm) k]) ω) atTop
        atTop} =ᵐ[μ]
    Set.univ
[PROOFSTEP]
have : ∀ᵐ ω ∂μ, ∀ n, (μ[(s (n + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm n]) ω = _ :=
  ae_all_iff.2 fun n => hs.condexp_indicator_filtrationOfSet_ae_eq hsm n.lt_succ_self
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
⊢ {ω |
      Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑(filtrationOfSet hsm) k]) ω) atTop
        atTop} =ᵐ[μ]
    Set.univ
[PROOFSTEP]
filter_upwards [this] with ω hω
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
⊢ setOf
      (fun ω =>
        Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑(filtrationOfSet hsm) k]) ω) atTop
          atTop)
      ω =
    Set.univ ω
[PROOFSTEP]
refine' eq_true (_ : Tendsto _ _ _)
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
⊢ Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop
[PROOFSTEP]
simp_rw [hω]
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
⊢ Tendsto (fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1)))) atTop atTop
[PROOFSTEP]
have htends : Tendsto (fun n => ∑ k in Finset.range n, μ (s (k + 1))) atTop (𝓝 ∞) :=
  by
  rw [← ENNReal.tsum_add_one_eq_top hs' (measure_ne_top _ _)]
  exact ENNReal.tendsto_nat_tsum _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
⊢ Tendsto (fun n => ∑ k in Finset.range n, ↑↑μ (s (k + 1))) atTop (𝓝 ⊤)
[PROOFSTEP]
rw [← ENNReal.tsum_add_one_eq_top hs' (measure_ne_top _ _)]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
⊢ Tendsto (fun n => ∑ k in Finset.range n, ↑↑μ (s (k + 1))) atTop (𝓝 (∑' (n : ℕ), ↑↑μ (s (n + 1))))
[PROOFSTEP]
exact ENNReal.tendsto_nat_tsum _
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : Tendsto (fun n => ∑ k in Finset.range n, ↑↑μ (s (k + 1))) atTop (𝓝 ⊤)
⊢ Tendsto (fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1)))) atTop atTop
[PROOFSTEP]
rw [ENNReal.tendsto_nhds_top_iff_nnreal] at htends 
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
⊢ Tendsto (fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1)))) atTop atTop
[PROOFSTEP]
refine' tendsto_atTop_atTop_of_monotone' _ _
[GOAL]
case h.refine'_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
⊢ Monotone fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1)))
[PROOFSTEP]
refine' monotone_nat_of_le_succ fun n => _
[GOAL]
case h.refine'_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
n : ℕ
⊢ ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1))) ≤
    ∑ x in Finset.range (n + 1), ENNReal.toReal (↑↑μ (s (x + 1)))
[PROOFSTEP]
rw [← sub_nonneg, Finset.sum_range_succ_sub_sum]
[GOAL]
case h.refine'_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
n : ℕ
⊢ 0 ≤ ENNReal.toReal (↑↑μ (s (n + 1)))
[PROOFSTEP]
exact ENNReal.toReal_nonneg
[GOAL]
case h.refine'_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
⊢ ¬BddAbove (Set.range fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1))))
[PROOFSTEP]
rintro ⟨B, hB⟩
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
B : ℝ
hB : B ∈ upperBounds (Set.range fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1))))
⊢ False
[PROOFSTEP]
refine' not_eventually.2 (frequently_of_forall fun n => _) (htends B.toNNReal)
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
B : ℝ
hB : B ∈ upperBounds (Set.range fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1))))
n : ℕ
⊢ ¬↑(Real.toNNReal B) < ∑ k in Finset.range n, ↑↑μ (s (k + 1))
[PROOFSTEP]
rw [mem_upperBounds] at hB 
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), (x ∈ Set.range fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1)))) → x ≤ B
n : ℕ
⊢ ¬↑(Real.toNNReal B) < ∑ k in Finset.range n, ↑↑μ (s (k + 1))
[PROOFSTEP]
specialize hB (∑ k : ℕ in Finset.range n, μ (s (k + 1))).toReal _
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), (x ∈ Set.range fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1)))) → x ≤ B
n : ℕ
⊢ ENNReal.toReal (∑ k in Finset.range n, ↑↑μ (s (k + 1))) ∈
    Set.range fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1)))
[PROOFSTEP]
refine' ⟨n, _⟩
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), (x ∈ Set.range fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1)))) → x ≤ B
n : ℕ
⊢ (fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1)))) n =
    ENNReal.toReal (∑ k in Finset.range n, ↑↑μ (s (k + 1)))
[PROOFSTEP]
rw [ENNReal.toReal_sum]
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), (x ∈ Set.range fun n => ∑ x in Finset.range n, ENNReal.toReal (↑↑μ (s (x + 1)))) → x ≤ B
n : ℕ
⊢ ∀ (a : ℕ), a ∈ Finset.range n → ↑↑μ (s (a + 1)) ≠ ⊤
[PROOFSTEP]
exact fun _ _ => measure_ne_top _ _
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
B : ℝ
n : ℕ
hB : ENNReal.toReal (∑ k in Finset.range n, ↑↑μ (s (k + 1))) ≤ B
⊢ ¬↑(Real.toNNReal B) < ∑ k in Finset.range n, ↑↑μ (s (k + 1))
[PROOFSTEP]
rw [not_lt, ← ENNReal.toReal_le_toReal (ENNReal.sum_lt_top _).ne ENNReal.coe_ne_top]
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
B : ℝ
n : ℕ
hB : ENNReal.toReal (∑ k in Finset.range n, ↑↑μ (s (k + 1))) ≤ B
⊢ ENNReal.toReal (∑ a in Finset.range n, ↑↑μ (s (a + 1))) ≤ ENNReal.toReal ↑(Real.toNNReal B)
[PROOFSTEP]
exact hB.trans (by simp)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
B : ℝ
n : ℕ
hB : ENNReal.toReal (∑ k in Finset.range n, ↑↑μ (s (k + 1))) ≤ B
⊢ B ≤ ENNReal.toReal ↑(Real.toNNReal B)
[PROOFSTEP]
simp
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
s✝ : ι → Set Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s
hs' : ∑' (n : ℕ), ↑↑μ (s n) = ⊤
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = (fun x => ENNReal.toReal (↑↑μ (s (n + 1)))) ω
ω : Ω
hω : ∀ (n : ℕ), (μ[Set.indicator (s (n + 1)) 1|↑(filtrationOfSet hsm) n]) ω = ENNReal.toReal (↑↑μ (s (n + 1)))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k in Finset.range a, ↑↑μ (s (k + 1))
B : ℝ
n : ℕ
hB : ENNReal.toReal (∑ k in Finset.range n, ↑↑μ (s (k + 1))) ≤ B
⊢ ∀ (a : ℕ), a ∈ Finset.range n → ↑↑μ (s (a + 1)) ≠ ⊤
[PROOFSTEP]
exact fun _ _ => measure_ne_top _ _
