Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Parabolic.FourierGalerkin.ScalarSpace

Scalar spatial L² synthesis for the real Fourier frame #

The orthonormal scalar Fourier modes synthesize an isometric copy of the finite coefficient space inside scalar torus L². This is the common state space for the cutoff paths and the coefficient energy estimate.

source
@[instance_reducible]
noncomputable def scalarSpaceMeasureSpaceUnitAddCircle :
MeasureTheory.MeasureSpace UnitAddCircle

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

Equations
Instances For
    source
    theorem scalarSpaceMeasureIsAddHaarUnitAddCircle :
    MeasureTheory.volume.IsAddHaarMeasure
    source
    theorem scalarSpaceProbabilityUnitAddCircle :
    MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
    source
    @[reducible, inline]
    noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.ScalarTorusL2 :
    AddSubgroup (Torus →ₘ[MeasureTheory.volume] ℝ)

    Scalar-valued spatial L² on the unit torus.

    Equations
    Instances For
      source
      theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_memLp (N : ℕ) (i : Fin (RealFourierDimension N)) :
      MeasureTheory.MemLp (realFourierModeFin N i) 2 MeasureTheory.volume

      Every real Fourier mode belongs to scalar spatial L².

      source
      noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeL2 (N : ℕ) (i : Fin (RealFourierDimension N)) :
      ↥ScalarTorusL2

      The class of one normalized real cutoff mode in scalar L².

      Equations
      Instances For
        source
        noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierScalarMap (N : ℕ) :
        Coefficients (RealFourierDimension N) →L[ℝ] ↥ScalarTorusL2

        Synthesis of a finite real coefficient vector as a scalar torus L² function.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierScalarMap_apply (N : ℕ) (c : Coefficients (RealFourierDimension N)) :
          (realFourierScalarMap N) c = ∑ i : Fin (RealFourierDimension N), c.ofLp i • realFourierModeL2 N i
          source
          theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeL2_inner (N : ℕ) (i j : Fin (RealFourierDimension N)) :
          inner ℝ (realFourierModeL2 N i) (realFourierModeL2 N j) = if i = j then 1 else 0

          The scalar cutoff modes remain orthonormal in their L² classes.

          source
          theorem AVenhance.Infra.Parabolic.FourierGalerkin.ScalarSpace.finiteModeSynthesis_inner {n : ℕ} (v : Fin n → ↥ScalarTorusL2) (horth : ∀ (i j : Fin n), inner ℝ (v i) (v j) = if i = j then 1 else 0) (c d : Coefficients n) :
          inner ℝ (∑ i : Fin n, c.ofLp i • v i) (∑ j : Fin n, d.ofLp j • v j) = inner ℝ c d
          source
          theorem AVenhance.Infra.Parabolic.FourierGalerkin.ScalarSpace.finiteModeSynthesis_norm {n : ℕ} (v : Fin n → ↥ScalarTorusL2) (horth : ∀ (i j : Fin n), inner ℝ (v i) (v j) = if i = j then 1 else 0) (c : Coefficients n) :
          ‖∑ i : Fin n, c.ofLp i • v i‖ = ‖c‖
          source
          noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.orthonormalProjectionCoefficients {n : ℕ} (v : Fin n → ↥ScalarTorusL2) (x : ↥ScalarTorusL2) :
          Coefficients n

          The coefficient vector of an orthogonal projection onto a finite orthonormal family is contractive.

          Equations
          Instances For
            source
            theorem AVenhance.Infra.Parabolic.FourierGalerkin.orthonormalProjectionCoefficients_norm_le {n : ℕ} (v : Fin n → ↥ScalarTorusL2) (horth : ∀ (i j : Fin n), inner ℝ (v i) (v j) = if i = j then 1 else 0) (x : ↥ScalarTorusL2) :
            ‖orthonormalProjectionCoefficients v x‖ ≤ ‖x‖
            source
            theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierScalarMap_norm (N : ℕ) (c : Coefficients (RealFourierDimension N)) :
            ‖(realFourierScalarMap N) c‖ = ‖c‖

            Synthesis by an orthonormal real Fourier frame is an isometry.

            source
            theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierScalarMap_inner (N : ℕ) (c d : Coefficients (RealFourierDimension N)) :
            inner ℝ ((realFourierScalarMap N) c) ((realFourierScalarMap N) d) = inner ℝ c d

            Synthesis preserves the coefficient-space pairing, including against a different test vector. This identity is the interface used to test the finite ODE by an arbitrary Fourier mode.

            source
            theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_projectionCoefficients_norm_le (N : ℕ) {f : Torus → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
            ‖modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) f‖ ≤ ‖MeasureTheory.MemLp.toLp f hf‖

            The finite Fourier projection coefficients of any torus L² datum are contractive.