Measurable drift Galerkin entries

This module transports the ambient drift hypotheses to the time-dependent entries of a finite periodic weak-form matrix. The mode and gradient representatives are supplied explicitly; the real Fourier frame can then use this bridge without changing the weak-form convention.

@[instance_reducible]

noncomputable def frozenMatrixMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem frozenMatrixMeasureIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem frozenMatrixProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenMatrix.frozenWeakEntry_drift_eq_unitCube (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (ht : t ∈ Set.Icc 0 1) (hbper : ∀ s ∈ Set.Icc 0 1, IsZ2Periodic (b s)) (grad : Homogenization.Vec 2 → Homogenization.Vec 2) (weight : Homogenization.Vec 2 → ℝ) (hgradper : Torus.IsZdPeriodic grad) (hweightper : Torus.IsZdPeriodic weight) : ∫ (x : Torus), vecDot (Torus.periodicToTorus (b t) x) (Torus.periodicToTorus grad x) * Torus.periodicToTorus weight x = ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (b t x) (grad x) * weight x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenWeakFormMatrixEntry_time_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)) (κ : ℝ) (mode : Fin n → Torus → ℝ) (modeGrad : Fin n → Torus → Fin 2 → ℝ) (modeAmbient : Fin n → Homogenization.Vec 2 → ℝ) (modeGradAmbient : Fin n → Homogenization.Vec 2 → Fin 2 → ℝ) (hmode : ∀ (i : Fin n), mode i = Torus.periodicToTorus (modeAmbient i)) (hgrad : ∀ (i : Fin n), modeGrad i = Torus.periodicToTorus (modeGradAmbient i)) (hmode_meas : ∀ (i : Fin n), MeasureTheory.AEStronglyMeasurable (modeAmbient i) (MeasureTheory.volume.restrict unitCube)) (hgrad_meas : ∀ (i : Fin n), MeasureTheory.AEStronglyMeasurable (modeGradAmbient i) (MeasureTheory.volume.restrict unitCube)) (hmode_per : ∀ (i : Fin n), Torus.IsZdPeriodic (modeAmbient i)) (hgrad_per : ∀ (i : Fin n) (j : Fin 2), Torus.IsZdPeriodic fun (x : Homogenization.Vec 2) => modeGradAmbient i x j) (i j : Fin n) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => weakFormMatrixEntry (fun (s : ℝ) (x : Torus) => Torus.periodicToTorus (b s) x) κ mode modeGrad t i j) (MeasureTheory.volume.restrict (Set.Icc 0 1))

Under the measurable and periodic drift assumptions, each weak-form matrix entry is a.e. strongly measurable in time. Only the drift part varies with time; the diffusion part is a fixed scalar integral. The torus integral is identified with the open-cell integral using periodicity of the modes and the drift.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.frozenWeakFormCoefficient {n : ℕ} (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) (mode : Fin n → Torus → ℝ) (modeGrad : Fin n → Torus → Fin 2 → ℝ) : ℝ → Coefficients n →L[ℝ] Coefficients n

The weak-form coefficient matrix on the physical time interval, extended by zero to the whole line for the measurable-coefficient ODE interface.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenWeakFormCoefficient_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)) (κ : ℝ) (mode : Fin n → Torus → ℝ) (modeGrad : Fin n → Torus → Fin 2 → ℝ) (modeAmbient : Fin n → Homogenization.Vec 2 → ℝ) (modeGradAmbient : Fin n → Homogenization.Vec 2 → Fin 2 → ℝ) (hmode : ∀ (i : Fin n), mode i = Torus.periodicToTorus (modeAmbient i)) (hgrad : ∀ (i : Fin n), modeGrad i = Torus.periodicToTorus (modeGradAmbient i)) (hmode_meas : ∀ (i : Fin n), MeasureTheory.AEStronglyMeasurable (modeAmbient i) (MeasureTheory.volume.restrict unitCube)) (hgrad_meas : ∀ (i : Fin n), MeasureTheory.AEStronglyMeasurable (modeGradAmbient i) (MeasureTheory.volume.restrict unitCube)) (hmode_per : ∀ (i : Fin n), Torus.IsZdPeriodic (modeAmbient i)) (hgrad_per : ∀ (i : Fin n) (j : Fin 2), Torus.IsZdPeriodic fun (x : Homogenization.Vec 2) => modeGradAmbient i x j) : MeasureTheory.AEStronglyMeasurable (frozenWeakFormCoefficient b κ mode modeGrad) MeasureTheory.volume

Product measurability of the drift induces a globally a.e. strongly measurable Galerkin coefficient after extending the physical-time matrix by zero.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenWeakFormCoefficient_norm_le_of_entries {n : ℕ} (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) (mode : Fin n → Torus → ℝ) (modeGrad : Fin n → Torus → Fin 2 → ℝ) {K : ℝ} (hK : 0 ≤ K) (hentry : ∀ t ∈ Set.Icc 0 1, ∀ (i j : Fin n), |weakFormMatrixEntry (fun (s : ℝ) (x : Torus) => Torus.periodicToTorus (b s) x) κ mode modeGrad t i j| ≤ K) (t : ℝ) : ‖frozenWeakFormCoefficient b κ mode modeGrad t‖ ≤ ↑n ^ 2 * K

A uniform bound on all physical-time matrix entries gives the global operator bound required by the measurable linear ODE interface. The zero extension makes the outside-interval case immediate.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenWeakFormMatrixEntry_abs_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) (κ : ℝ) (mode : Fin n → Torus → ℝ) (modeGrad : Fin n → Torus → Fin 2 → ℝ) {G U D : ℝ} (hG : 0 ≤ G) (hU : 0 ≤ U) (hD : 0 ≤ D) (hgrad_memLp : ∀ (j : Fin n), MeasureTheory.MemLp (fun (x : Torus) => euclideanVecNorm (modeGrad j x)) 2 MeasureTheory.volume) (hmode_memLp : ∀ (i : Fin n), MeasureTheory.MemLp (mode i) 2 MeasureTheory.volume) (hgrad_factor : ∀ (j : Fin n), 0 ≤ (∫ (x : Torus), euclideanVecNorm (modeGrad j x) ^ 2) ^ (1 / 2) ∧ (∫ (x : Torus), euclideanVecNorm (modeGrad j x) ^ 2) ^ (1 / 2) ≤ G) (hmode_factor : ∀ (i : Fin n), 0 ≤ (∫ (x : Torus), ‖mode i x‖ ^ 2) ^ (1 / 2) ∧ (∫ (x : Torus), ‖mode i x‖ ^ 2) ^ (1 / 2) ≤ U) (hdiffusion_bound : ∀ (i j : Fin n), |∫ (x : Torus), vecDot (modeGrad j x) (modeGrad i x)| ≤ D) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ t ∈ Set.Icc 0 1, ∀ (i j : Fin n), |weakFormMatrixEntry (fun (s : ℝ) (x : Torus) => Torus.periodicToTorus (b s) x) κ mode modeGrad t i j| ≤ K

A finite mode family with explicit L² gradient/function bounds has uniformly bounded weak-form entries. The drift part uses only the measurable bounded drift estimate; the diffusion term is controlled by the supplied finite-family gradient pairing bound.