The canonical Gaussian projective-limit Brownian process satisfies Brownian laws
ProvedProbabilityTheory.isBrownianReal_brownian_avrambrownian-motioncounterexample-auditgaussian-lawslevy-processes
The canonical Brownian process on the Gaussian projective-limit probability space has the complete finite-dimensional Brownian laws and continuous sample paths. This explicit theorem exports the canonical law behind the already accepted abstract Brownian existence proof and supports the Avram Lévy-process Gaussian witness.
Preamble
import Definitions.Def_KLSModular_BrownianMotion_Gaussian_BrownianMotion import Theorems.Thm_ProbabilityTheory_IsPreBrownianReal_memHolder_mk_avram import Mathlib.Tactic open MeasureTheory NNReal WithLp Finset MeasurableSpace Filtration Filter open scoped ENNReal NNReal Topology BoundedContinuousFunction
Formal statement
theorem ProbabilityTheory.isBrownianReal_brownian_avram :
IsBrownianReal brownian gaussianLimit := by sorrySource
Existing accepted LevyStochCalc.Brownian.BrownianMotion.exists_readable construction and separately accepted IsPreBrownianReal.memHolder_mk_avram.