Positive real Fourier Galerkin data for the drift

This module instantiates the abstract finite weak-form ODE by the positive symmetric real Fourier cutoff. The coefficient datum is the quotient-torus representative of the initial datum.

@[instance_reducible]

noncomputable def concreteDataMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

• concreteDataMeasureSpaceUnitAddCircle = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem concreteDataMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem concreteDataProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.spatialVector_norm_eq_euclideanVecNorm (v : Homogenization.Vec 2) : ‖WithLp.toLp 2 v‖ = euclideanVecNorm v

The PiLp 2 norm is the Euclidean norm used by the gradient energy.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.fourierGalerkin_vecDot_eq_frozen (u v : Homogenization.Vec 2) : vecDot u v = Homogenization.vecDot u v

The local Galerkin matrix dot product is the Euclidean vector pairing.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradFin_norm_memLp (N : ℕ) (i : Fin (RealFourierDimension N)) : MeasureTheory.MemLp (fun (x : Torus) => euclideanVecNorm (realFourierModeGradFin N i x)) 2 MeasureTheory.volume

The gradient norm of one positive-cutoff mode belongs to scalar L².

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientMap_coeFn (N : ℕ) (c : Coefficients (RealFourierDimension N)) : (fun (x : Torus) => ↑↑((realFourierGradientMap N) c) x) =ᵐ[MeasureTheory.volume] fun (x : Torus) => WithLp.toLp 2 (∑ i : Fin (RealFourierDimension N), c.ofLp i • realFourierModeGradFin N i x)

The pointwise finite gradient sum is the representative of the L² gradient map.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierScalarMap_coeFn (N : ℕ) (c : Coefficients (RealFourierDimension N)) : (fun (x : Torus) => ↑↑((realFourierScalarMap N) c) x) =ᵐ[MeasureTheory.volume] fun (x : Torus) => modeExpansion (RealFourierDimension N) (realFourierModeFin N) c x

The pointwise finite scalar sum is the representative of the scalar synthesis map.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.l2_norm_sq_eq_integral_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) : ‖f‖ ^ 2 = ∫ (x : Torus), ‖↑↑f x‖ ^ 2

The scalar L² norm squared is the integral of the pointwise squared norm.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientMap_inner_formula (N : ℕ) (c : Coefficients (RealFourierDimension N)) : inner ℝ ((realFourierGradientMap N) c) ((realFourierGradientMap N) c) = ∑ i : Fin (RealFourierDimension N), ∑ j : Fin (RealFourierDimension N), c.ofLp i * c.ofLp j * inner ℝ (realFourierModeGradL2 N i) (realFourierModeGradL2 N j)

The diffusion energy of a finite real Fourier gradient sum is its weak-form pairing.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradL2_inner (N : ℕ) (i j : Fin (RealFourierDimension N)) : inner ℝ (realFourierModeGradL2 N i) (realFourierModeGradL2 N j) = ∫ (x : Torus), vecDot (realFourierModeGradFin N i x) (realFourierModeGradFin N j x)

The L² pairing of two real Fourier gradient modes is the diffusion matrix entry.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.matrixCoefficientCLM_inner_quadratic {n : ℕ} (A : Fin n → Fin n → ℝ) (c : Coefficients n) : inner ℝ c ((matrixCoefficientCLM A) c) = ∑ i : Fin n, ∑ j : Fin n, c.ofLp i * c.ofLp j * A i j

Quadratic pairing of a finite coefficient matrix in the Euclidean coefficient inner product.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientMap_diffusionMatrix (N : ℕ) (c : Coefficients (RealFourierDimension N)) : ‖(realFourierGradientMap N) c‖ ^ 2 = ∑ i : Fin (RealFourierDimension N), ∑ j : Fin (RealFourierDimension N), c.ofLp i * c.ofLp j * ∫ (x : Torus), vecDot (realFourierModeGradFin N j x) (realFourierModeGradFin N i x)

The finite gradient energy equals the quadratic form of the weak diffusion matrix.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierWeakMatrix_quadratic (N : ℕ) (b : ℝ → Torus → Homogenization.Vec 2) (κ t : ℝ) (c : Coefficients (RealFourierDimension N)) : ∑ i : Fin (RealFourierDimension N), ∑ j : Fin (RealFourierDimension N), c.ofLp i * c.ofLp j * weakFormMatrixEntry b κ (realFourierModeFin N) (realFourierModeGradFin N) t i j = (-∑ i : Fin (RealFourierDimension N), ∑ j : Fin (RealFourierDimension N), c.ofLp i * c.ofLp j * ∫ (x : Torus), vecDot (b t x) (realFourierModeGradFin N j x) * realFourierModeFin N i x) - κ * ‖(realFourierGradientMap N) c‖ ^ 2

The quadratic weak-form matrix splits into the direct drift form and the gradient energy.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientMap_norm_sq (N : ℕ) (c : Coefficients (RealFourierDimension N)) : ‖(realFourierGradientMap N) c‖ ^ 2 = ∫ (x : Torus), euclideanVecNorm (∑ i : Fin (RealFourierDimension N), c.ofLp i • realFourierModeGradFin N i x) ^ 2

The L² norm of a finite real Fourier gradient sum is its integral gradient energy.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientExpansion_norm_memLp (N : ℕ) (c : Coefficients (RealFourierDimension N)) : MeasureTheory.MemLp (fun (x : Torus) => euclideanVecNorm (∑ i : Fin (RealFourierDimension N), c.ofLp i • realFourierModeGradFin N i x)) 2 MeasureTheory.volume

The finite pointwise real Fourier gradient sum belongs to scalar L² after taking its Euclidean norm.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierScalarExpansion_memLp (N : ℕ) (c : Coefficients (RealFourierDimension N)) : MeasureTheory.MemLp (modeExpansion (RealFourierDimension N) (realFourierModeFin N) c) 2 MeasureTheory.volume

The finite pointwise real Fourier scalar sum belongs to scalar L².

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientExpansion_l2Factor (N : ℕ) (c : Coefficients (RealFourierDimension N)) : (∫ (x : Torus), euclideanVecNorm (∑ i : Fin (RealFourierDimension N), c.ofLp i • realFourierModeGradFin N i x) ^ 2) ^ (1 / 2) = ‖(realFourierGradientMap N) c‖

The gradient factor of the finite Fourier sum is its vector L² norm.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierScalarExpansion_l2Factor (N : ℕ) (c : Coefficients (RealFourierDimension N)) : (∫ (x : Torus), ‖modeExpansion (RealFourierDimension N) (realFourierModeFin N) c x‖ ^ 2) ^ (1 / 2) = ‖c‖

The scalar factor of the finite Fourier sum is the coefficient norm.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFinL2Factor (N : ℕ) (i : Fin (RealFourierDimension N)) : ℝ

The square-integral factor of a normalized scalar Fourier mode.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradFinL2Factor (N : ℕ) (i : Fin (RealFourierDimension N)) : ℝ

The square-integral factor of a real Fourier gradient mode.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeFin_l2Factor_eq_one (N : ℕ) (i : Fin (RealFourierDimension N)) : realFourierModeFinL2Factor N i = 1

Every real mode has scalar L² factor one.

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

The finite cutoff has an explicit bound for all individual gradient-mode factors.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradFin_l2Factor_nonneg (N : ℕ) (i : Fin (RealFourierDimension N)) : 0 ≤ realFourierModeGradFinL2Factor N i

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierCutoffGradientBound_nonneg (N : ℕ) : 0 ≤ realFourierCutoffGradientBound N

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradFin_l2Factor_le_cutoff (N : ℕ) (i : Fin (RealFourierDimension N)) : realFourierModeGradFinL2Factor N i ≤ realFourierCutoffGradientBound N

theorem AVenhance.Infra.Parabolic.FourierGalerkin.vecDot_abs_le_euclidean (u v : Homogenization.Vec 2) : |Homogenization.vecDot u v| ≤ euclideanVecNorm u * euclideanVecNorm v

Cauchy--Schwarz for the two-vector dot product in its Euclidean norm.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradFin_diffusion_abs_bound_by_factors (N : ℕ) (i j : Fin (RealFourierDimension N)) : |∫ (x : Torus), vecDot (realFourierModeGradFin N j x) (realFourierModeGradFin N i x)| ≤ realFourierModeGradFinL2Factor N j * realFourierModeGradFinL2Factor N i

The diffusion pairing is bounded by the product of the two gradient-mode factors.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradFin_diffusion_abs_bound (N : ℕ) (i j : Fin (RealFourierDimension N)) : |∫ (x : Torus), vecDot (realFourierModeGradFin N j x) (realFourierModeGradFin N i x)| ≤ realFourierCutoffGradientBound N ^ 2

The diffusion pairing of any two cutoff modes is bounded by the square of the cutoff gradient bound.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenDrift_torus_slice_aestronglyMeasurable (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), MeasureTheory.AEStronglyMeasurable (Torus.periodicToTorus (b t)) MeasureTheory.volume

The product-measurable drift has a.e. strongly measurable torus slices.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenDrift_realModeEntry_integrable_ae (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (i j : Fin (RealFourierDimension N)), MeasureTheory.Integrable (fun (x : Torus) => vecDot (Torus.periodicToTorus (b t) x) (realFourierModeGradFin N j x) * realFourierModeFin N i x) MeasureTheory.volume

Every real-mode drift matrix integrand is spatially integrable for almost every time.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierDriftExpansion_pointwise (N : ℕ) (b : Torus → Homogenization.Vec 2) (c : Coefficients (RealFourierDimension N)) : (fun (x : Torus) => Homogenization.vecDot (b x) (∑ j : Fin (RealFourierDimension N), c.ofLp j • realFourierModeGradFin N j x) * modeExpansion (RealFourierDimension N) (realFourierModeFin N) c x) = fun (x : Torus) => ∑ i : Fin (RealFourierDimension N), ∑ j : Fin (RealFourierDimension N), c.ofLp i * c.ofLp j * (Homogenization.vecDot (b x) (realFourierModeGradFin N j x) * realFourierModeFin N i x)

Pointwise bilinearity of the drift form under the two finite real Fourier syntheses.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierDriftExpansion_integral (N : ℕ) (b : ℝ → Torus → Homogenization.Vec 2) (t : ℝ) (c : Coefficients (RealFourierDimension N)) (hentries : ∀ (i j : Fin (RealFourierDimension N)), MeasureTheory.Integrable (fun (x : Torus) => Homogenization.vecDot (b t x) (realFourierModeGradFin N j x) * realFourierModeFin N i x) MeasureTheory.volume) : ∫ (x : Torus), Homogenization.vecDot (b t x) (∑ j : Fin (RealFourierDimension N), c.ofLp j • realFourierModeGradFin N j x) * modeExpansion (RealFourierDimension N) (realFourierModeFin N) c x = ∑ i : Fin (RealFourierDimension N), ∑ j : Fin (RealFourierDimension N), c.ofLp i * c.ofLp j * ∫ (x : Torus), Homogenization.vecDot (b t x) (realFourierModeGradFin N j x) * realFourierModeFin N i x

Under the a.e. slice integrability supplied by product measurability, the finite drift integral expands as the quadratic sum of weak matrix entries.

@[irreducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffGradientMap (N : ℕ) : Coefficients (RealFourierDimension N) →L[ℝ] ↥SpatialGradientL2

The quadratic drift form obtained by expanding a positive-cutoff real Fourier sum.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffGradientMap N = AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientMap N

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierDriftForm (N : ℕ) (drift : ℝ → Torus → Homogenization.Vec 2) (t : ℝ) (c : Coefficients (RealFourierDimension N)) : ℝ

Quadratic contribution of the drift to the real Fourier Galerkin energy.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffDriftConstant (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) : ℝ

The explicit dot-product constant associated with the drift bound.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffDriftConstant b hb_bdd = √2 * Classical.choose hb_bdd

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffDriftForm_bound (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) : 0 ≤ positiveCutoffDriftConstant b hb_bdd ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (c : Coefficients (RealFourierDimension N)), |realFourierDriftForm N (fun (s : ℝ) => Torus.periodicToTorus (b s)) t c| ≤ positiveCutoffDriftConstant b hb_bdd * ‖(positiveCutoffGradientMap N) c‖ * ‖c‖

The bounded drift controls the concrete finite Fourier drift form.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffDriftConstant_spec (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) : 0 ≤ positiveCutoffDriftConstant b hb_bdd ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (c : Coefficients (RealFourierDimension N)), |realFourierDriftForm N (fun (s : ℝ) => Torus.periodicToTorus (b s)) t c| ≤ positiveCutoffDriftConstant b hb_bdd * ‖(positiveCutoffGradientMap N) c‖ * ‖c‖

The chosen drift constant satisfies the bound proved from the hypotheses.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffWeakFormEntry_bound (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (κ : ℝ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ t ∈ Set.Icc 0 1, ∀ (i j : Fin (RealFourierDimension N)), |weakFormMatrixEntry (fun (s : ℝ) (x : Torus) => Torus.periodicToTorus (b s) x) κ (realFourierModeFin N) (realFourierModeGradFin N) t i j| ≤ K

A uniform matrix-entry bound for the positive real Fourier frame.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffMatrixConstant (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (κ : ℝ) : ℝ

A chosen entry bound for the positive-cutoff weak matrix.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffMatrixConstant N b hb_bdd κ = Classical.choose ⋯

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffMatrixConstant_spec (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (κ : ℝ) : 0 ≤ positiveCutoffMatrixConstant N b hb_bdd κ ∧ ∀ t ∈ Set.Icc 0 1, ∀ (i j : Fin (RealFourierDimension N)), |weakFormMatrixEntry (fun (s : ℝ) (x : Torus) => Torus.periodicToTorus (b s) x) κ (realFourierModeFin N) (realFourierModeGradFin N) t i j| ≤ positiveCutoffMatrixConstant N b hb_bdd κ

The chosen matrix bound applies to every entry on the physical time interval.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffWeakForm_energy_identity (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ t : ℝ) (ht : t ∈ Set.Icc 0 1) (c : Coefficients (RealFourierDimension N)) : 2 * inner ℝ c ((frozenWeakFormCoefficient b κ (realFourierModeFin N) (realFourierModeGradFin N) t) c) = -2 * realFourierDriftForm N (fun (s : ℝ) => Torus.periodicToTorus (b s)) t c - 2 * κ * ‖(positiveCutoffGradientMap N) c‖ ^ 2

The finite coefficient energy identity for the concrete positive Fourier weak matrix.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffWeakForm_energy_ae (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (c : Coefficients (RealFourierDimension N)), 2 * inner ℝ c ((frozenWeakFormCoefficient b κ (realFourierModeFin N) (realFourierModeGradFin N) t) c) = -2 * realFourierDriftForm N (fun (s : ℝ) => Torus.periodicToTorus (b s)) t c - 2 * κ * ‖(positiveCutoffGradientMap N) c‖ ^ 2

The pointwise coefficient energy identity holds for a.e. physical time.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffCoefficient_aestronglyMeasurable (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (b t)) (κ : ℝ) : MeasureTheory.AEStronglyMeasurable (frozenWeakFormCoefficient b κ (realFourierModeFin N) (realFourierModeGradFin N)) MeasureTheory.volume

The measurable-drift theorem applies to the concrete real Fourier frame.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffCoefficient_matrixSpec (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (c : Coefficients (RealFourierDimension N)) (i : Fin (RealFourierDimension N)), ((frozenWeakFormCoefficient b κ (realFourierModeFin N) (realFourierModeGradFin N) t) c).ofLp i = ∑ j : Fin (RealFourierDimension N), weakFormMatrixEntry (fun (s : ℝ) (x : Torus) => Torus.periodicToTorus (b s) x) κ (realFourierModeFin N) (realFourierModeGradFin N) t i j * c.ofLp j

The concrete cutoff coefficient agrees a.e. with its weak-form matrix.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffCoefficient_norm_le (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (κ t : ℝ) : ‖frozenWeakFormCoefficient b κ (realFourierModeFin N) (realFourierModeGradFin N) t‖ ≤ ↑(RealFourierDimension N) ^ 2 * positiveCutoffMatrixConstant N b hb_bdd κ

The matrix bound gives the global operator bound required by the finite ODE.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffInitial_projection (N : ℕ) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀_L2 : Homogenization.MemL2On unitCube θ₀) (x : Torus) : modeExpansion (RealFourierDimension N) (realFourierModeFin N) (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) (Torus.periodicToTorus θ₀)) x = realFourierProjection N (Torus.periodicToTorus θ₀) x

Projection of the initial datum has the finite real Fourier expansion in its own coefficient vector.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffGalerkinData (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (b t)) (κ : ℝ) (hκ : 0 < κ) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀_L2 : Homogenization.MemL2On unitCube θ₀) : WeakFormGalerkinData (RealFourierDimension N) ↥SpatialGradientL2

Concrete positive-cutoff Galerkin data built from the measurable, bounded, periodic drift and the L² initial datum.

Equations

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