Integrability of the constructed displacement

The first result is adapted from the Apache-2.0 upstream module SuperdiffusionAudit/Support/SuperdiffusivityIntegrability.lean at commit 7f20476385d4af418f110303085ad0740c9eba46. It uses the production confinement tail directly, without the comparator's duplicate model vocabulary. The second result makes finiteness of both Bochner observables in Theorem A explicit.

theorem Algsuperdiff.Section5.Provider.exists_ae_integrable_streamProcess_norm_rpow (d : ℕ) [NeZero d] (hd : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gammaI : ℝ), 0 < gammaI ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gammaI → ∀ (t : ℝ), 0 < t → ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), ∀ (p : ℝ), 1 ≤ p → MeasureTheory.Integrable (fun (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) => ‖DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal)‖ ^ p) ((Field.streamProcess M omega) ↑0)

Small coupling gives every norm moment of order at least one.

theorem Algsuperdiff.Section5.Provider.exists_ae_integrable_streamProcess_displacement (d : ℕ) [NeZero d] (hd : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gammaI : ℝ), 0 < gammaI ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gammaI → ∀ (t : ℝ), 0 < t → ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), MeasureTheory.Integrable (fun (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) => DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal)) ((Field.streamProcess M omega) ↑0) ∧ MeasureTheory.Integrable (fun (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) => HCPolySupport.vecNormSq (DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal))) ((Field.streamProcess M omega) ↑0)

The first and second displacement observables have finite Bochner integrals.