Is Locally Square Integrable is Local Submartingale sq norm

lemma IsLocallySquareIntegrable.isLocalSubmartingale_sq_norm    [OrderBot ι] [OrderTopology ι] [CompleteSpace E]    (hX : IsLocallySquareIntegrable X 𝓕 P) :    IsLocalSubmartingale (fun t ω ↦ ‖X t ω‖ ^ 2) 𝓕 P := by  have h_stopped_sq_norm {τ : Ω → WithTop ι} :      stoppedProcess (fun t ↦ {ω | ⊥ < τ ω}.indicator (fun ω ↦ ‖X t ω‖ ^ 2)) τ =        fun t ω ↦ ‖stoppedProcess (fun t ↦ {ω | ⊥ < τ ω}.indicator (X t)) τ t ω‖ ^ 2 := by    ext t ω    by_cases hτ : ⊥ < τ ω <;> simp [stoppedProcess, hτ]  unfold IsLocalSubmartingale  change Locally (fun Y : ι → Ω → ℝ ↦ Submartingale Y 𝓕 P ∧      ∀ ω, IsCadlag (Y · ω)) 𝓕 (fun t ω ↦ ‖X t ω‖ ^ 2) P  refine ⟨hX.localSeq, hX.isLocalizingSequence_localSeq, fun n ↦ ?_⟩  have hXn := hX.stoppedProcess_localSeq n  constructor  · simpa [h_stopped_sq_norm] using hXn.submartingale_sq_norm  · intro ω    simpa [h_stopped_sq_norm] using IsCadlag.norm_sq (hXn.cadlag ω)