Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Parabolic.FourierGalerkin.Density

Density of the real symmetric Fourier cutoffs #

The union of the finite real Fourier synthesis ranges is dense in scalar torus L². This is the test space used by the weak path compactness argument.

source
@[instance_reducible]
noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.densityMeasureSpaceUnitAddCircle :
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.densityMeasureIsAddHaarUnitAddCircle :
    MeasureTheory.volume.IsAddHaarMeasure
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.densityProbabilityUnitAddCircle :
    MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.densityScalarTorusMeasureSeparable :
    MeasureTheory.IsSeparable MeasureTheory.volume
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.densityTwoNeTopFact :
    Fact (2 ≠ ⊤)
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.densityOneLeTwoFact :
    Fact (1 ≤ 2)
    source
    @[irreducible]
    noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierProjectionCoefficients (N : ℕ) (v : ↥ScalarTorusL2) :
    Coefficients (RealFourierDimension N)

    The coefficient vector of the orthogonal cutoff projection of a torus L² class.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem AVenhance.Infra.Parabolic.FourierGalerkin.Density.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.realFourierScalarMap_projection_eq_realPartFourierSum (N : ℕ) (v : ↥ScalarTorusL2) :
      (realFourierScalarMap N) (realFourierProjectionCoefficients N v) = Complex.reCLM.compLp (complexFourierPartialSumLp N (Complex.ofRealCLM.compLp v))

      Real synthesis of the torus orthogonal projection agrees with the real part of the complex Fourier cutoff in L².

      source
      theorem AVenhance.Infra.Parabolic.FourierGalerkin.tendsto_realFourierProjection (v : ↥ScalarTorusL2) :
      Filter.Tendsto (fun (N : ℕ) => (realFourierScalarMap N) (realFourierProjectionCoefficients N v)) Filter.atTop (nhds v)

      The concrete real Galerkin synthesis ranges exhaust scalar torus L².

      source
      def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierSpan :
      Set ↥ScalarTorusL2

      Union of all finite real symmetric Fourier synthesis ranges.

      Equations
      Instances For
        source
        theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierSpan_dense :
        Dense realFourierSpan

        Finite real Fourier synthesis ranges form a dense family in scalar torus L².