Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Parabolic.FourierGalerkin.LimitPassage

The projected trace and the real Fourier limit #

These lemmas identify the initial value of the concrete Galerkin paths with the real part of the complex torus Fourier cutoff. Combined with Parseval convergence, they supply the weak path compactness theorem with the exact initial trace.

source
@[instance_reducible]
noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.limitPassageMeasureSpaceUnitAddCircle :
MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.limitPassageMeasureIsAddHaarUnitAddCircle :
    MeasureTheory.volume.IsAddHaarMeasure
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.limitPassageProbabilityUnitAddCircle :
    MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.coefficientPath_initial (P : FrozenDriftProblem) (N : ℕ) :
    (P.coefficientPath N) ⟨0, ⋯⟩ = (P.galerkinData N).initial

    The chosen finite Galerkin coefficient path starts at its orthogonal initial projection.

    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitPassage.mFourierCoeff_congr_ae {f g : Torus → ℂ} (hfg : f =ᵐ[MeasureTheory.volume] g) (k : Fin 2 → ℤ) :
    UnitAddTorus.mFourierCoeff f k = UnitAddTorus.mFourierCoeff g k
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.initialComplexification_ae (P : FrozenDriftProblem) :
    (fun (x : Torus) => ↑↑(Complex.ofRealCLM.compLp P.initialTorusL2) x) =ᵐ[MeasureTheory.volume] fun (x : Torus) => ↑(Torus.periodicToTorus P.θ₀ x)

    The complexified initial datum has the canonical real representative a.e.

    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.initialProjection_eq_realPartFourierSum (P : FrozenDriftProblem) (N : ℕ) :
    (realFourierScalarMap N) (P.galerkinData N).initial = Complex.reCLM.compLp (complexFourierPartialSumLp N (Complex.ofRealCLM.compLp P.initialTorusL2))

    The coefficient path's real scalar initial state is the real Fourier cutoff of the datum.

    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.scalarPath_initial (P : FrozenDriftProblem) (N : ℕ) :
    (P.scalarPath N) ⟨0, ⋯⟩ = (realFourierScalarMap N) (P.galerkinData N).initial

    The concrete Galerkin paths start at the projected initial datum.

    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.initialTrace_weak_tendsto (P : FrozenDriftProblem) (v : ↥ScalarTorusL2) :
    Filter.Tendsto (fun (N : ℕ) => inner ℝ ((P.scalarPath N) ⟨0, ⋯⟩) v) Filter.atTop (nhds (inner ℝ P.initialTorusL2 v))

    The finite Galerkin initial traces converge weakly to the L² datum.