Drift estimates from the boundedness hypothesis

The weak-wellposedness root assumes a pointwise bound on the ambient drift. Since Vec 2 uses the product sup norm while the spatial gradient energy is Euclidean, the dimension-two bridge below records the harmless factor sqrt 2. No divergence-free assumption is used.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenDrift_aestronglyMeasurable_cell (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))) : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ unitCube))

The product-measurability hypothesis restricts to the physical space-time cell.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.aestronglyMeasurable_timeIntegral_of_cell {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ unitCube))) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, f (t, x)) (MeasureTheory.volume.restrict (Set.Icc 0 1))

Fubini turns cellwise a.e. strong measurability into a measurable time-dependent spatial integral. The domain measure is exactly the product of restricted time and space measures.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenDrift_weightedCell_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))) (grad : Homogenization.Vec 2 → Homogenization.Vec 2) (hgrad : MeasureTheory.AEStronglyMeasurable grad (MeasureTheory.volume.restrict unitCube)) (weight : Homogenization.Vec 2 → ℝ) (hweight : MeasureTheory.AEStronglyMeasurable weight (MeasureTheory.volume.restrict unitCube)) : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (b p.1 p.2) (grad p.2) * weight p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ unitCube))

Multiplying the drift by a spatial vector field and scalar test mode preserves a.e. strong measurability on the space-time cell.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenDrift_weakEntry_time_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))) (grad : Homogenization.Vec 2 → Homogenization.Vec 2) (hgrad : MeasureTheory.AEStronglyMeasurable grad (MeasureTheory.volume.restrict unitCube)) (weight : Homogenization.Vec 2 → ℝ) (hweight : MeasureTheory.AEStronglyMeasurable weight (MeasureTheory.volume.restrict unitCube)) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (b t x) (grad x) * weight x) (MeasureTheory.volume.restrict (Set.Icc 0 1))

Each drift weak-form matrix entry against spatially measurable modes is measurable in time. This is the time-coefficient measurability bridge from the product hypothesis.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.euclideanVecNorm (v : Homogenization.Vec 2) : ℝ

The Euclidean norm associated with the squared vector norm used by the carriers.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.euclideanVecNorm v = √(Homogenization.vecNormSq v)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.euclideanVecNorm_nonneg (v : Homogenization.Vec 2) : 0 ≤ euclideanVecNorm v

theorem AVenhance.Infra.Parabolic.FourierGalerkin.euclideanVecNorm_sq (v : Homogenization.Vec 2) : euclideanVecNorm v ^ 2 = Homogenization.vecNormSq v

theorem AVenhance.Infra.Parabolic.FourierGalerkin.vecDot_le_of_supNorm_le {b v : Homogenization.Vec 2} {C : ℝ} (hC : 0 ≤ C) (hb : ‖b‖ ≤ C) : |Homogenization.vecDot b v| ≤ √2 * C * euclideanVecNorm v

The pointwise bound controls the Euclidean dot product, with the conversion from the product sup norm to the Euclidean norm made explicit.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenDrift_vecDot_bound (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ t ∈ Set.Icc 0 1, ∀ (x v : Homogenization.Vec 2), |Homogenization.vecDot (b t x) v| ≤ B * euclideanVecNorm v

A bounded drift gives a dimension-explicit bound on every spatial dot product.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.driftIntegral_bound_of_L2 {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f g u : α → ℝ) (B : ℝ) (hB : 0 ≤ B) (hpoint : ∀ᵐ (x : α) ∂μ, |f x| ≤ B * (|g x| * |u x|)) (hg : MeasureTheory.MemLp g 2 μ) (hu : MeasureTheory.MemLp u 2 μ) (hf : MeasureTheory.Integrable f μ) : |∫ (x : α), f x ∂μ| ≤ B * (∫ (x : α), ‖g x‖ ^ 2 ∂μ) ^ (1 / 2) * (∫ (x : α), ‖u x‖ ^ 2 ∂μ) ^ (1 / 2)

Hölder controls the space-time-cell drift form from the two scalar L² bounds.

The vector estimate is supplied separately by frozenDrift_vecDot_bound; this lemma is the integral step used to obtain the drift_bound field of a Galerkin system.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.driftIntegral_bound_of_L2_or_not {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f g u : α → ℝ) (B : ℝ) (hB : 0 ≤ B) (hpoint : ∀ᵐ (x : α) ∂μ, |f x| ≤ B * (|g x| * |u x|)) (hg : MeasureTheory.MemLp g 2 μ) (hu : MeasureTheory.MemLp u 2 μ) : |∫ (x : α), f x ∂μ| ≤ B * (∫ (x : α), ‖g x‖ ^ 2 ∂μ) ^ (1 / 2) * (∫ (x : α), ‖u x‖ ^ 2 ∂μ) ^ (1 / 2)

The same L² drift estimate holds without a measurability premise on the integrand: if the Bochner integral is undefined, Mathlib's integral convention assigns it zero. This form is useful for pointwise matrix bounds when the product-measurability hypothesis controls slices only for almost every time.