[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
