Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Parabolic.FourierGalerkin.CutoffNesting

Nested finite real Fourier spaces #

This module transfers a coefficient vector from a cutoff into any larger symmetric cutoff. Both its scalar synthesis and its gradient synthesis are preserved.

source
noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierCoefficientsLift {M N : ℕ} (hMN : M ≤ N) (c : Coefficients (RealFourierDimension M)) :
Coefficients (RealFourierDimension N)

Extend a finite coefficient vector by zero along the injection into a larger Fourier cutoff.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.CutoffNesting.realFourierIndexLiftFin_injective {M N : ℕ} (hMN : M ≤ N) :
    Function.Injective (realFourierIndexLiftFin hMN)
    source
    @[simp]
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierCoefficientsLift_apply_lift {M N : ℕ} (hMN : M ≤ N) (c : Coefficients (RealFourierDimension M)) (i : Fin (RealFourierDimension M)) :
    (realFourierCoefficientsLift hMN c).ofLp (realFourierIndexLiftFin hMN i) = c.ofLp i
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarExpansion_lift {M N : ℕ} (hMN : M ≤ N) (c : Coefficients (RealFourierDimension M)) (x : Torus) :
    modeExpansion (RealFourierDimension N) (realFourierModeFin N) (realFourierCoefficientsLift hMN c) x = modeExpansion (RealFourierDimension M) (realFourierModeFin M) c x

    Pointwise finite Fourier synthesis is unchanged by zero-extending its coefficients to a larger cutoff.

    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierScalarMap_lift {M N : ℕ} (hMN : M ≤ N) (c : Coefficients (RealFourierDimension M)) :
    (realFourierScalarMap N) (realFourierCoefficientsLift hMN c) = (realFourierScalarMap M) c

    Scalar synthesis commutes with embedding a cutoff into a larger one.

    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.CutoffNesting.gradientExpansion_lift {M N : ℕ} (hMN : M ≤ N) (c : Coefficients (RealFourierDimension M)) (x : Torus) :
    ∑ j : Fin (RealFourierDimension N), (realFourierCoefficientsLift hMN c).ofLp j • realFourierModeGradFin N j x = ∑ i : Fin (RealFourierDimension M), c.ofLp i • realFourierModeGradFin M i x
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientMap_lift {M N : ℕ} (hMN : M ≤ N) (c : Coefficients (RealFourierDimension M)) :
    (realFourierGradientMap N) (realFourierCoefficientsLift hMN c) = (realFourierGradientMap M) c

    Finite gradient synthesis commutes with embedding a cutoff into a larger one.