[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : Preorder ι
u✝ v : ι → Ω → β
f : Filtration ι m
inst✝¹ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝ : BorelSpace β
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
⊢ Adapted (natural u hum) u
[PROOFSTEP]
intro i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : Preorder ι
u✝ v : ι → Ω → β
f : Filtration ι m
inst✝¹ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝ : BorelSpace β
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ StronglyMeasurable (u i)
[PROOFSTEP]
refine' StronglyMeasurable.mono _ (le_iSup₂_of_le i (le_refl i) le_rfl)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : Preorder ι
u✝ v : ι → Ω → β
f : Filtration ι m
inst✝¹ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝ : BorelSpace β
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ StronglyMeasurable (u i)
[PROOFSTEP]
rw [stronglyMeasurable_iff_measurable_separable]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : Preorder ι
u✝ v : ι → Ω → β
f : Filtration ι m
inst✝¹ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝ : BorelSpace β
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ Measurable (u i) ∧ IsSeparable (Set.range (u i))
[PROOFSTEP]
exact ⟨measurable_iff_comap_le.2 le_rfl, (hum i).isSeparable_range⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
⊢ Adapted f u
[PROOFSTEP]
intro i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
i : ι
⊢ StronglyMeasurable (u i)
[PROOFSTEP]
have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) := rfl
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
i : ι
this : u i = (fun p => u (↑p.fst) p.snd) ∘ fun x => ({ val := i, property := (_ : i ∈ Set.Iic i) }, x)
⊢ StronglyMeasurable (u i)
[PROOFSTEP]
rw [this]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
i : ι
this : u i = (fun p => u (↑p.fst) p.snd) ∘ fun x => ({ val := i, property := (_ : i ∈ Set.Iic i) }, x)
⊢ StronglyMeasurable ((fun p => u (↑p.fst) p.snd) ∘ fun x => ({ val := i, property := (_ : i ∈ Set.Iic i) }, x))
[PROOFSTEP]
exact (h i).comp_measurable measurable_prod_mk_left
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
⊢ ProgMeasurable f fun i ω => u (t i ω) ω
[PROOFSTEP]
intro i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
⊢ StronglyMeasurable fun p => (fun i ω => u (t i ω) ω) (↑p.fst) p.snd
[PROOFSTEP]
have :
  (fun p : ↥(Set.Iic i) × Ω => u (t (p.fst : ι) p.snd) p.snd) =
    (fun p : ↥(Set.Iic i) × Ω => u (p.fst : ι) p.snd) ∘ fun p : ↥(Set.Iic i) × Ω =>
      (⟨t (p.fst : ι) p.snd, Set.mem_Iic.mpr ((ht_le _ _).trans p.fst.prop)⟩, p.snd) :=
  rfl
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this :
  (fun p => u (t (↑p.fst) p.snd) p.snd) =
    (fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := t (↑p.fst) p.snd, property := (_ : t (↑p.fst) p.snd ∈ Set.Iic i) }, p.snd)
⊢ StronglyMeasurable fun p => (fun i ω => u (t i ω) ω) (↑p.fst) p.snd
[PROOFSTEP]
rw [this]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this :
  (fun p => u (t (↑p.fst) p.snd) p.snd) =
    (fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := t (↑p.fst) p.snd, property := (_ : t (↑p.fst) p.snd ∈ Set.Iic i) }, p.snd)
⊢ StronglyMeasurable
    ((fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := t (↑p.fst) p.snd, property := (_ : t (↑p.fst) p.snd ∈ Set.Iic i) }, p.snd))
[PROOFSTEP]
exact (h i).comp_measurable ((ht i).measurable.subtype_mk.prod_mk measurable_snd)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : TopologicalSpace β
inst✝³ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ (c : γ), c ∈ s → ProgMeasurable f (U c)
⊢ ProgMeasurable f fun i a => ∏ c in s, U c i a
[PROOFSTEP]
convert ProgMeasurable.finset_prod' h using 1
[GOAL]
case h.e'_9
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : TopologicalSpace β
inst✝³ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ (c : γ), c ∈ s → ProgMeasurable f (U c)
⊢ (fun i a => ∏ c in s, U c i a) = ∏ c in s, U c
[PROOFSTEP]
ext (i a)
[GOAL]
case h.e'_9.h.h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : TopologicalSpace β
inst✝³ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ (c : γ), c ∈ s → ProgMeasurable f (U c)
i : ι
a : Ω
⊢ ∏ c in s, U c i a = Finset.prod s (fun c => U c) i a
[PROOFSTEP]
simp only [Finset.prod_apply]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : NeBot fltr
inst✝ : IsCountablyGenerated fltr
U : γ → ι → Ω → β
h : ∀ (l : γ), ProgMeasurable f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
⊢ ProgMeasurable f u
[PROOFSTEP]
intro i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : NeBot fltr
inst✝ : IsCountablyGenerated fltr
U : γ → ι → Ω → β
h : ∀ (l : γ), ProgMeasurable f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
i : ι
⊢ StronglyMeasurable fun p => u (↑p.fst) p.snd
[PROOFSTEP]
apply @stronglyMeasurable_of_tendsto (Set.Iic i × Ω) β γ (MeasurableSpace.prod _ (f i)) _ _ fltr _ _ _ _ fun l => h l i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : NeBot fltr
inst✝ : IsCountablyGenerated fltr
U : γ → ι → Ω → β
h : ∀ (l : γ), ProgMeasurable f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
i : ι
⊢ Tendsto (fun l p => U l (↑p.fst) p.snd) fltr (𝓝 fun p => u (↑p.fst) p.snd)
[PROOFSTEP]
rw [tendsto_pi_nhds] at h_tendsto ⊢
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : NeBot fltr
inst✝ : IsCountablyGenerated fltr
U : γ → ι → Ω → β
h : ∀ (l : γ), ProgMeasurable f (U l)
h_tendsto : ∀ (x : ι), Tendsto (fun i => U i x) fltr (𝓝 (u x))
i : ι
⊢ ∀ (x : ↑(Set.Iic i) × Ω), Tendsto (fun i_1 => U i_1 (↑x.fst) x.snd) fltr (𝓝 (u (↑x.fst) x.snd))
[PROOFSTEP]
intro x
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : NeBot fltr
inst✝ : IsCountablyGenerated fltr
U : γ → ι → Ω → β
h : ∀ (l : γ), ProgMeasurable f (U l)
h_tendsto : ∀ (x : ι), Tendsto (fun i => U i x) fltr (𝓝 (u x))
i : ι
x : ↑(Set.Iic i) × Ω
⊢ Tendsto (fun i_1 => U i_1 (↑x.fst) x.snd) fltr (𝓝 (u (↑x.fst) x.snd))
[PROOFSTEP]
specialize h_tendsto x.fst
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : NeBot fltr
inst✝ : IsCountablyGenerated fltr
U : γ → ι → Ω → β
h : ∀ (l : γ), ProgMeasurable f (U l)
i : ι
x : ↑(Set.Iic i) × Ω
h_tendsto : Tendsto (fun i_1 => U i_1 ↑x.fst) fltr (𝓝 (u ↑x.fst))
⊢ Tendsto (fun i_1 => U i_1 (↑x.fst) x.snd) fltr (𝓝 (u (↑x.fst) x.snd))
[PROOFSTEP]
rw [tendsto_nhds] at h_tendsto ⊢
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u v : ι → Ω → β
f : Filtration ι m
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : NeBot fltr
inst✝ : IsCountablyGenerated fltr
U : γ → ι → Ω → β
h : ∀ (l : γ), ProgMeasurable f (U l)
i : ι
x : ↑(Set.Iic i) × Ω
h_tendsto : ∀ (s : Set (Ω → β)), IsOpen s → u ↑x.fst ∈ s → (fun i_1 => U i_1 ↑x.fst) ⁻¹' s ∈ fltr
⊢ ∀ (s : Set β), IsOpen s → u (↑x.fst) x.snd ∈ s → (fun i_1 => U i_1 (↑x.fst) x.snd) ⁻¹' s ∈ fltr
[PROOFSTEP]
exact fun s hs h_mem => h_tendsto {g | g x.snd ∈ s} (hs.preimage (continuous_apply x.snd)) h_mem


[GOAL]
Ω : 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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
⊢ μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
[PROOFSTEP]
by_cases hfint : Integrable f μ
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Integrable f
⊢ μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : ¬Integrable f
⊢ μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
[PROOFSTEP]
swap
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : ¬Integrable f
⊢ μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
[PROOFSTEP]
rw [condexp_undef hfint, integral_undef hfint]
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : ¬Integrable f
⊢ 0 =ᵐ[μ] fun x => 0
[PROOFSTEP]
rfl
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Integrable f
⊢ μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
[PROOFSTEP]
refine'
  (ae_eq_condexp_of_forall_set_integral_eq hle₂ hfint (fun s _ hs => integrableOn_const.2 (Or.inr hs))
      (fun s hms hs => _) stronglyMeasurable_const.aeStronglyMeasurable').symm
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Integrable f
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ∫ (x : Ω) in s, ∫ (x : Ω), f x ∂μ ∂μ = ∫ (x : Ω) in s, f x ∂μ
[PROOFSTEP]
rw [set_integral_const]
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Integrable f
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hfint
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ
[PROOFSTEP]
refine' Memℒp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ _ _ _ hfint _
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ AEStronglyMeasurable' m₁ f μ
[PROOFSTEP]
exact ⟨f, hf, EventuallyEq.rfl⟩
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ∀ (c : E) ⦃s_1 : Set Ω⦄,
    MeasurableSet s_1 →
      ↑↑μ s_1 < ⊤ →
        ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), Set.indicator s_1 (fun x => c) x ∂μ =
          ∫ (x : Ω) in s, Set.indicator s_1 (fun x => c) x ∂μ
[PROOFSTEP]
intro c t hmt _
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
c : E
t : Set Ω
hmt : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), Set.indicator t (fun x => c) x ∂μ =
    ∫ (x : Ω) in s, Set.indicator t (fun x => c) x ∂μ
[PROOFSTEP]
rw [Indep_iff] at hindp
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
c : E
t : Set Ω
hmt : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), Set.indicator t (fun x => c) x ∂μ =
    ∫ (x : Ω) in s, Set.indicator t (fun x => c) x ∂μ
[PROOFSTEP]
rw [integral_indicator (hle₁ _ hmt), set_integral_const, smul_smul, ← ENNReal.toReal_mul, mul_comm, ← hindp _ _ hmt hms,
  set_integral_indicator (hle₁ _ hmt), set_integral_const, Set.inter_comm]
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Memℒp f 1 →
        Memℒp g 1 →
          StronglyMeasurable f →
            StronglyMeasurable g →
              ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
                ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ
[PROOFSTEP]
intro u v _ huint hvint hu hv hu_eq hv_eq
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
u v : Ω → E
a✝ : Disjoint (Function.support u) (Function.support v)
huint : Memℒp u 1
hvint : Memℒp v 1
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
hv_eq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), (u + v) x ∂μ = ∫ (x : Ω) in s, (u + v) x ∂μ
[PROOFSTEP]
rw [memℒp_one_iff_integrable] at huint hvint
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
u v : Ω → E
a✝ : Disjoint (Function.support u) (Function.support v)
huint : Integrable u
hvint : Integrable v
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
hv_eq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), (u + v) x ∂μ = ∫ (x : Ω) in s, (u + v) x ∂μ
[PROOFSTEP]
rw [integral_add' huint hvint, smul_add, hu_eq, hv_eq, integral_add' huint.integrableOn hvint.integrableOn]
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ IsClosed {f | ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}
[PROOFSTEP]
have heq₁ :
  (fun f : lpMeas E ℝ m₁ 1 μ => ∫ x, (f : Ω → E) x ∂μ) = (fun f : Lp E 1 μ => ∫ x, f x ∂μ) ∘ Submodule.subtypeL _ :=
  by
  refine' funext fun f => integral_congr_ae _
  simp_rw [Submodule.coe_subtypeL', Submodule.coeSubtype]; norm_cast
[GOAL]
Ω : 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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
[PROOFSTEP]
refine' funext fun f => integral_congr_ae _
[GOAL]
Ω : 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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f✝
hindp : Indep m₁ m₂
hfint : Memℒp f✝ 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
f : { x // x ∈ lpMeas E ℝ m₁ 1 μ }
⊢ (fun x => ↑↑↑f x) =ᵐ[μ] fun x => ↑↑(↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ)) f) x
[PROOFSTEP]
simp_rw [Submodule.coe_subtypeL', Submodule.coeSubtype]
[GOAL]
Ω : 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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f✝
hindp : Indep m₁ m₂
hfint : Memℒp f✝ 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
f : { x // x ∈ lpMeas E ℝ m₁ 1 μ }
⊢ (fun x => ↑↑↑f x) =ᵐ[μ] fun x => ↑↑↑f x
[PROOFSTEP]
norm_cast
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ IsClosed {f | ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}
[PROOFSTEP]
have heq₂ :
  (fun f : lpMeas E ℝ m₁ 1 μ => ∫ x in s, (f : Ω → E) x ∂μ) =
    (fun f : Lp E 1 μ => ∫ x in s, f x ∂μ) ∘ Submodule.subtypeL _ :=
  by
  refine' funext fun f => integral_congr_ae (ae_restrict_of_ae _)
  simp_rw [Submodule.coe_subtypeL', Submodule.coeSubtype]
  exact eventually_of_forall fun _ => (by trivial)
[GOAL]
Ω : 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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
[PROOFSTEP]
refine' funext fun f => integral_congr_ae (ae_restrict_of_ae _)
[GOAL]
Ω : 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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f✝
hindp : Indep m₁ m₂
hfint : Memℒp f✝ 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
f : { x // x ∈ lpMeas E ℝ m₁ 1 μ }
⊢ ∀ᵐ (x : Ω) ∂μ, (fun x => ↑↑↑f x) x = (fun x => ↑↑(↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ)) f) x) x
[PROOFSTEP]
simp_rw [Submodule.coe_subtypeL', Submodule.coeSubtype]
[GOAL]
Ω : 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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f✝
hindp : Indep m₁ m₂
hfint : Memℒp f✝ 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
f : { x // x ∈ lpMeas E ℝ m₁ 1 μ }
⊢ ∀ᵐ (x : Ω) ∂μ, True
[PROOFSTEP]
exact eventually_of_forall fun _ => (by trivial)
[GOAL]
Ω : 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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f✝
hindp : Indep m₁ m₂
hfint : Memℒp f✝ 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
f : { x // x ∈ lpMeas E ℝ m₁ 1 μ }
x✝ : Ω
⊢ True
[PROOFSTEP]
trivial
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
heq₂ :
  (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ IsClosed {f | ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}
[PROOFSTEP]
refine' isClosed_eq (Continuous.const_smul _ _) _
[GOAL]
case pos.refine'_4.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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
heq₂ :
  (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ Continuous fun f => ∫ (x : Ω), ↑↑↑f x ∂μ
[PROOFSTEP]
rw [heq₁]
[GOAL]
case pos.refine'_4.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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
heq₂ :
  (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ Continuous ((fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ)))
[PROOFSTEP]
exact continuous_integral.comp (ContinuousLinearMap.continuous _)
[GOAL]
case pos.refine'_4.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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
heq₂ :
  (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ Continuous fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ
[PROOFSTEP]
rw [heq₂]
[GOAL]
case pos.refine'_4.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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
heq₂ :
  (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ Continuous ((fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ)))
[PROOFSTEP]
exact (continuous_set_integral _).comp (ContinuousLinearMap.continuous _)
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      Memℒp f 1 →
        ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
          ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ
[PROOFSTEP]
intro u v huv _ hueq
[GOAL]
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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : Memℒp u 1
hueq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
[PROOFSTEP]
rwa [← integral_congr_ae huv, ← (set_integral_congr_ae (hle₂ _ hms) _ : ∫ x in s, u x ∂μ = ∫ x in s, v x ∂μ)]
[GOAL]
Ω : 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 (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : Memℒp u 1
hueq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x
[PROOFSTEP]
filter_upwards [huv] with x hx _ using hx


[GOAL]
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ENNReal.ofReal (↑(cdf μ) x) = ↑↑μ (Iic x)
[PROOFSTEP]
have h := lintegral_condCdf ((Measure.dirac Unit.unit).prod μ) x
[GOAL]
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
h :
  ∫⁻ (a : Unit),
      ENNReal.ofReal
        (↑(condCdf (Measure.prod (Measure.dirac ()) μ) a) x) ∂Measure.fst (Measure.prod (Measure.dirac ()) μ) =
    ↑↑(Measure.prod (Measure.dirac ()) μ) (univ ×ˢ Iic x)
⊢ ENNReal.ofReal (↑(cdf μ) x) = ↑↑μ (Iic x)
[PROOFSTEP]
simpa only [MeasureTheory.Measure.fst_prod, Measure.prod_prod, measure_univ, one_mul, lintegral_dirac] using h
[GOAL]
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ↑(cdf μ) x = ENNReal.toReal (↑↑μ (Iic x))
[PROOFSTEP]
rw [← ofReal_cdf μ x, ENNReal.toReal_ofReal (cdf_nonneg μ x)]
[GOAL]
μ : Measure ℝ
⊢ IsProbabilityMeasure (StieltjesFunction.measure (cdf μ))
[PROOFSTEP]
constructor
[GOAL]
case measure_univ
μ : Measure ℝ
⊢ ↑↑(StieltjesFunction.measure (cdf μ)) univ = 1
[PROOFSTEP]
simp only [StieltjesFunction.measure_univ _ (tendsto_cdf_atBot μ) (tendsto_cdf_atTop μ), sub_zero, ENNReal.ofReal_one]
[GOAL]
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
⊢ StieltjesFunction.measure (cdf μ) = μ
[PROOFSTEP]
refine Measure.ext_of_Iic (cdf μ).measure μ (fun a ↦ ?_)
[GOAL]
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
a : ℝ
⊢ ↑↑(StieltjesFunction.measure (cdf μ)) (Iic a) = ↑↑μ (Iic a)
[PROOFSTEP]
rw [StieltjesFunction.measure_Iic _ (tendsto_cdf_atBot μ), sub_zero, ofReal_cdf]
[GOAL]
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ cdf (StieltjesFunction.measure f) = f
[PROOFSTEP]
refine (cdf f.measure).eq_of_measure_of_tendsto_atBot f ?_ (tendsto_cdf_atBot _) hf0
[GOAL]
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ StieltjesFunction.measure (cdf (StieltjesFunction.measure f)) = StieltjesFunction.measure f
[PROOFSTEP]
have h_prob : IsProbabilityMeasure f.measure := ⟨by rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]⟩
[GOAL]
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ ↑↑(StieltjesFunction.measure f) univ = 1
[PROOFSTEP]
rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]
[GOAL]
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
h_prob : IsProbabilityMeasure (StieltjesFunction.measure f)
⊢ StieltjesFunction.measure (cdf (StieltjesFunction.measure f)) = StieltjesFunction.measure f
[PROOFSTEP]
exact measure_cdf f.measure
[GOAL]
μ ν : Measure ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h : cdf μ = cdf ν
⊢ μ = ν
[PROOFSTEP]
rw [← measure_cdf μ, ← measure_cdf ν, h]
[GOAL]
μ ν : Measure ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h : μ = ν
⊢ cdf μ = cdf ν
[PROOFSTEP]
rw [h]


[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 _ _