Is Brownian Real indep zero

lemma IsBrownianReal.indep_zero (h : IsBrownianReal X P) (hX : ∀ t, Measurable (X t))    (hX' : ∀ ω, Continuous (X · ω)) {A : Set Ω}    (hA : MeasurableSet[⨅ s > 0, natural X (fun t ↦ (hX t).stronglyMeasurable) s] A) :    P A = 0 ∨ P A = 1 := by  have := h.isGaussianProcess.isProbabilityMeasure  -- We consider three different `σ`-algebras. `m1` is the one generated by the process `X`.  let m1 : MeasurableSpace Ω := .comap (fun ω t ↦ X t ω) inferInstance  -- `m2` is the one generated by the restriction of `X` to positive real numbers.  let m2 : MeasurableSpace Ω := .comap (fun ω (t : Set.Ioi (0 : ℝ≥0)) ↦ X t ω) inferInstance  -- `m3` is `⨅ s > 0, 𝓕 s`, which we want to show to be trivial.  set m3 : MeasurableSpace Ω := ⨅ s > 0, natural X (fun t ↦ (hX t).stronglyMeasurable) s-- We easily have that `m3 ≤ m1 ≤ mΩ`.  have hm1 : m1 ≤ mΩ := by    apply Measurable.comap_le    apply @measurable_pi_lambda _ _ _ mΩ    exact hX  have hm3 : m3 ≤ m1 := by    apply iInf₂_le_of_le 1 (by simp)    rw [natural_eq_comap]    exact comap_le_comap (fun x t ↦ x t.1) (by fun_prop) (by ext; simp)  have hm3' := hm3.trans hm1  -- Because `X` is continuous, `X t ⟶ X 0` as `t → 0⁺`, thus  -- the random variable `X 0` is actually measurable with respect to `m2`, so `m1 ≤ m2`.  have : m1 ≤ m2 := by    simp_rw [m1, m2, comap_process]    rw [iSup_split_single _ 0, sup_le_iff]    constructor; swap    · simp_rw [← pos_iff_ne_zero, iSup_subtype, Set.mem_Ioi]      rfl    rw [← measurable_iff_comap_le]    have this : Filter.Tendsto (X ∘ ((↑) : Set.Ioi (0 : ℝ≥0) → ℝ≥0))        ((𝓝[≠] 0).comap ((↑) : _ → ℝ≥0)) (𝓝 (X 0)) := by      refine Filter.tendsto_comap'_iff ?_ |>.2        (tendsto_pi_nhds.2 fun ω ↦ continuousAt_iff_punctured_nhds.1 (hX' ω).continuousAt)      convert self_mem_nhdsWithin      ext; simp [pos_iff_ne_zero]    have l : NeBot ((𝓝[≠] (0 : ℝ≥0)).comap ((↑) : Set.Ioi (0 : ℝ≥0) → ℝ≥0)) := by      refine comap_coe_neBot_of_le_principal <| le_principal_iff.2 ?_      convert self_mem_nhdsWithin      ext; simp [pos_iff_ne_zero]    exact @measurable_of_tendsto_metrizable' _ _ (iSup _) _ _ _ _ _ _ _ _ l _      (fun t ↦ (comap_measurable _).iSup' t) this  -- We prove the result by showing that `m3` is independent of itself.  refine measure_eq_zero_or_one_of_indep_self ?_ hA  -- To do so, we show that for all `A ∈ m3`, all finite set `I ⊆ (0, +∞)` and all  -- bounded continuous function `f : (I → ℝ) → ℝ`,  -- `∫ ω in A, f (fun t ↦ X t) ∂P = P.real A * ∫ ω, f (fun t ↦ X t) ∂P`.  refine indep_of_indep_of_le_right ?_ (hm3.trans this)  refine indep_comap_process_of_bcf hm3' (fun _ ↦ (hX _).aemeasurable) fun A hA I f ↦ ?_  -- If `I` is empty, there is nothing to do.  obtain rfl | hI := I.eq_empty_or_nonempty  · have : Subsingleton ((∅ : Finset (Set.Ioi (0 : ℝ≥0))) → ℝ) := inferInstance    simp [this.eq_zero]  -- We now assume `I` is not empty. We then prove that for all `ε > 0` such that `ε ≤ min I`,  -- `∫ ω in A, f (fun t ↦ X t ω - X ε ω) ∂P = P.real A * ∫ ω, f (fun t ↦ X t ω - X ε ω) ∂P`.  -- This follows from the fact that, because `A ∈ m3` in particular `A` is measurable  -- with respect to `σ(X t | t ≤ ε)`. This `σ`-algebra is independent from  -- `σ(X (ε + t) - X ε | t ≥ 0)` by the weak Markov property.  have key (ε : ℝ≥0) (hε1 : 0 < ε) (hε2 : ε ≤ I.min' hI) :      ∫ ω in A, f (fun t ↦ X t ω - X ε ω) ∂P = P.real A * ∫ ω, f (fun t ↦ X t ω - X ε ω) ∂P := by    rw [IndepSets.setIntegral_eq_mul _ (by fun_prop) (hm3' A hA) (by fun_prop)]    have := (IndepFun_iff_Indep _ _ _).1 <| h.indepFun_shift ε |>.symm    refine indepSets_of_indepSets_of_le_right (Indep.singleton_indepSets this ?_) ?_    · suffices m3 ≤ (.comap (fun ω (t : Set.Iic ε) ↦ X t ω) MeasurableSpace.pi) from this A hA      apply iInf₂_le_of_le ε hε1      rw [natural_eq_comap]    simp only [Set.ofPred_subset_ofPred, ← measurableSpace_le_iff]    apply comap_le_comap (fun x t ↦ x (t.1 - ε)) (by fun_prop)    ext ω t    simp only [Function.comp_apply, sub_left_inj]    rw [add_tsub_cancel_of_le]    exact hε2.trans (I.min'_le t.1 t.2)  -- Because `f` is continuous and `X t ⟶ 0` almost surely as `t → 0`,  -- we deduce that almost surely `f (fun t ↦ X t - X ε) ⟶ f (fun t ↦ X t)` as `t → 0`.  have lol : ∀ᵐ ω ∂P, Tendsto (fun ε ↦ f (fun t ↦ X t ω - X ε ω)) (𝓝[>] 0)      (𝓝 (f (fun t ↦ X t ω))) := by    filter_upwards [h.tendsto_nhds_zero] with ω hω    refine f.continuous.tendsto _ |>.comp (tendsto_pi_nhds.2 fun t ↦ ?_)    convert (tendsto_nhdsWithin_of_tendsto_nhds hω).const_sub (X t ω)    simp  -- Because `f` is also bounded, we can apply the dominated convergence theorem to show that  -- `∫ ω in A, f (fun t ↦ X t ω - X ε ω) ∂P ⟶ ∫ ω in A, f (fun t ↦ X t ω) ∂P`  -- as `ε → 0⁺`.  have h1 : Tendsto (fun ε ↦ ∫ ω in A, f (fun t ↦ X t ω - X ε ω) ∂P) (𝓝[>] 0)      (𝓝 (∫ ω in A, f (fun t ↦ X t ω) ∂P)) := by    refine tendsto_integral_filter_of_dominated_convergence (fun _ ↦ ‖f‖) ?_ ?_      (integrable_const _) (ae_restrict_of_ae lol)    · exact Eventually.of_forall fun _ ↦ Measurable.aestronglyMeasurable (by fun_prop)    · exact Eventually.of_forall fun _ ↦ ae_of_all _ fun _ ↦ f.norm_coe_le_norm _  -- But similarly we have that  -- `P.real A * ∫ ω, f (fun t ↦ X t ω - X ε ω) ∂P ⟶ P.real A * ∫ ω in A, f (fun t ↦ X t ω) ∂P`  -- as `ε → 0⁺`, and we can conclude by uniqueness of the limit.  refine tendsto_nhds_unique h1 ?_  refine Tendsto.congr' (f₁ := fun ε ↦ P.real A * ∫ ω, f (fun t ↦ X t ω - X ε ω) ∂P) ?_ ?_  · apply eventually_nhdsGT (I.min' hI |>.2)    rintro ε ⟨h1, h2⟩    exact (key ε h1 h2).symm  refine Filter.Tendsto.const_mul (b := P.real A) ?_  refine tendsto_integral_filter_of_dominated_convergence (fun _ ↦ ‖f‖) ?_ ?_    (integrable_const _) lol  · exact Eventually.of_forall fun _ ↦ Measurable.aestronglyMeasurable (by fun_prop)  · exact Eventually.of_forall fun _ ↦ ae_of_all _ fun _ ↦ f.norm_coe_le_norm _