Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjection

Fourier projection of periodic weak gradients #

The weak-gradient Fourier multiplier identifies the derivative of each real Fourier projection with the real Fourier projection of the weak gradient. This gives the slice-wise H¹ convergence needed in the weak energy passage.

source
@[instance_reducible]
noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.weakProjectionMeasureSpace :
MeasureTheory.MeasureSpace UnitAddCircle

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

Equations
Instances For
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakProjectionMeasureIsAddHaar :
    MeasureTheory.volume.IsAddHaarMeasure
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakProjectionProbabilityUnitAddCircle :
    MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakProjectionProbability :
    MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjection.weakProjection_mFourierCoeff_congr_ae {f g : FourierGalerkin.Torus → ℂ} (hfg : f =ᵐ[MeasureTheory.volume] g) (k : Fin 2 → ℤ) :
    UnitAddTorus.mFourierCoeff f k = UnitAddTorus.mFourierCoeff g k
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjection.weakProjection_frozenCellToTorus_coeff {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (k : Fin 2 → ℤ) :
    UnitAddTorus.mFourierCoeff (fun (x : FourierGalerkin.Torus) => Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => ↑(f y)) x) k = UnitAddTorus.mFourierCoeff (↑↑(Heat.frozenCellToTorusL2 hf)) k
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakProjection_realCellToTorus_memLp {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) :
    MeasureTheory.MemLp (Torus.periodicToTorus f) 2 MeasureTheory.volume
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakProjection.weakProjection_realFourierMultiplier {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (i : Fin 2) (k : Fin 2 → ℤ) :
    UnitAddTorus.mFourierCoeff (fun (x : FourierGalerkin.Torus) => Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => ↑(Du y i)) x) k = 2 * ↑Real.pi * Complex.I * ↑(k i) * UnitAddTorus.mFourierCoeff (fun (x : FourierGalerkin.Torus) => Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => ↑(u y)) x) k
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakGradient_realFourierProjectionCoefficients {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (N : ℕ) (i : Fin 2) :
    Classical.realFourierModeDerivativeCoefficients N (FourierGalerkin.modeProjectionCoefficients (FourierGalerkin.RealFourierDimension N) (FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus u)) i = FourierGalerkin.modeProjectionCoefficients (FourierGalerkin.RealFourierDimension N) (FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => Du x i)

    The finite real Fourier derivative coefficients of a periodic H¹ value are exactly the real Fourier coefficients of the corresponding weak-gradient component.