Projection

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Projection.complexFourierPartialSumComplex_sum {ι : Type u_1} {N : ℕ} (s : Finset ι) (F : ι → Torus → ℂ) (hF : ∀ i ∈ s, Continuous (F i)) (x : Torus) : complexFourierPartialSumComplex N (fun (y : Torus) => ∑ i ∈ s, F i y) x = ∑ i ∈ s, complexFourierPartialSumComplex N (F i) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Projection.complexFourierPartialSumComplex_linearCombination {N : ℕ} {k l : Fin 2 → ℤ} (hk : frequencyPair k ∈ symmetricFrequencyBox N) (hl : frequencyPair l ∈ symmetricFrequencyBox N) (c d : ℂ) (x : Torus) : complexFourierPartialSumComplex N (fun (y : Torus) => c * (UnitAddTorus.mFourier k) y + d * (UnitAddTorus.mFourier l) y) x = c * (UnitAddTorus.mFourier k) x + d * (UnitAddTorus.mFourier l) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Projection.frequencyPair_neg (k : Fin 2 → ℤ) : frequencyPair (-k) = -frequencyPair k

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Projection.neg_frequency_mem_box {N : ℕ} {k : Fin 2 → ℤ} (hk : frequencyPair k ∈ symmetricFrequencyBox N) : frequencyPair (-k) ∈ symmetricFrequencyBox N

theorem AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSumComplex_realFourierMode {N : ℕ} (a : RealFourierIndex N) (x : Torus) : complexFourierPartialSumComplex N (fun (y : Torus) => ↑(realFourierMode N a y)) x = ↑(realFourierMode N a x)

Every real sine/cosine mode in the cutoff is fixed by the corresponding complex Fourier sum.

@[irreducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.RealFourierDimension (N : ℕ) : ℕ

The finite real-mode dimension at cutoff N.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.RealFourierDimension N = Fintype.card (AVenhance.Infra.Parabolic.FourierGalerkin.RealFourierIndex N)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierIndexEquivFin (N : ℕ) : RealFourierIndex N ≃ Fin (RealFourierDimension N)

Reindex the concrete real Fourier family by the standard finite type used by the ODE layer.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.realFourierIndexEquivFin N = id (Fintype.equivFin (AVenhance.Infra.Parabolic.FourierGalerkin.RealFourierIndex N))

def AVenhance.Infra.Parabolic.FourierGalerkin.positiveRepresentativeLift {M N : ℕ} (hMN : M ≤ N) (p : ↥(positiveFrequencyRepresentatives M)) : ↥(positiveFrequencyRepresentatives N)

Lift a real Fourier index into a larger symmetric cutoff.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.positiveRepresentativeLift hMN p = ⟨↑p, ⋯⟩

theorem AVenhance.Infra.Parabolic.FourierGalerkin.representativeFrequency_lift {M N : ℕ} (hMN : M ≤ N) (p : ↥(positiveFrequencyRepresentatives M)) : representativeFrequency (positiveRepresentativeLift hMN p) = representativeFrequency p

The representative frequency is unchanged by lifting a positive representative.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierIndexLift {M N : ℕ} (hMN : M ≤ N) : RealFourierIndex M → RealFourierIndex N

Lift a real Fourier index into a larger symmetric cutoff.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierIndexLift_injective {M N : ℕ} (hMN : M ≤ N) : Function.Injective (realFourierIndexLift hMN)

Lifting real indices to a larger cutoff is injective.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_lift {M N : ℕ} (hMN : M ≤ N) (a : RealFourierIndex M) : realFourierMode N (realFourierIndexLift hMN a) = realFourierMode M a

The lift preserves every real mode.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbient_lift {M N : ℕ} (hMN : M ≤ N) (a : RealFourierIndex M) : realFourierModeAmbient N (realFourierIndexLift hMN a) = realFourierModeAmbient M a

The lift preserves the smooth ambient real mode.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbientGrad_lift {M N : ℕ} (hMN : M ≤ N) (a : RealFourierIndex M) : realFourierModeAmbientGrad N (realFourierIndexLift hMN a) = realFourierModeAmbientGrad M a

The lift also preserves the ambient periodic gradient mode.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin (N : ℕ) : Fin (RealFourierDimension N) → Torus → ℝ

The scalar Fourier mode family with Fin indices.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradFin (N : ℕ) : Fin (RealFourierDimension N) → Torus → Homogenization.Vec 2

The gradient family with the matching Fin indices.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierIndexLiftFin {M N : ℕ} (hMN : M ≤ N) : Fin (RealFourierDimension M) → Fin (RealFourierDimension N)

The Fin-indexed injection induced by a nested real Fourier cutoff.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_lift {M N : ℕ} (hMN : M ≤ N) (i : Fin (RealFourierDimension M)) : realFourierModeFin N (realFourierIndexLiftFin hMN i) = realFourierModeFin M i

The scalar mode is unchanged by the Fin-indexed cutoff injection.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_orthonormal (N : ℕ) (i j : Fin (RealFourierDimension N)) : ∫ (x : Torus), realFourierModeFin N i x * realFourierModeFin N j x = if i = j then 1 else 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_continuous (N : ℕ) (i : Fin (RealFourierDimension N)) : Continuous (realFourierModeFin N i)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_eq_periodicToTorus (N : ℕ) (i : Fin (RealFourierDimension N)) : realFourierModeFin N i = Torus.periodicToTorus (realFourierModeAmbient N ((realFourierIndexEquivFin N).symm i))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradFin_eq_periodicToTorus (N : ℕ) (i : Fin (RealFourierDimension N)) : realFourierModeGradFin N i = Torus.periodicToTorus (realFourierModeAmbientGrad N ((realFourierIndexEquivFin N).symm i))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradFin_lift {M N : ℕ} (hMN : M ≤ N) (i : Fin (RealFourierDimension M)) : realFourierModeGradFin N (realFourierIndexLiftFin hMN i) = realFourierModeGradFin M i

The gradient mode is unchanged by the Fin-indexed cutoff injection.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSumComplex_modeExpansion {N : ℕ} (c : Coefficients (RealFourierDimension N)) (x : Torus) : complexFourierPartialSumComplex N (fun (y : Torus) => ↑(modeExpansion (RealFourierDimension N) (realFourierModeFin N) c y)) x = ↑(modeExpansion (RealFourierDimension N) (realFourierModeFin N) c x)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierProjection_modeExpansion (N : ℕ) (c : Coefficients (RealFourierDimension N)) : realFourierProjection N (modeExpansion (RealFourierDimension N) (realFourierModeFin N) c) = modeExpansion (RealFourierDimension N) (realFourierModeFin N) c

Every finite coefficient expansion of the cutoff's real modes is fixed by its real projection.