Measurability and bounds for the transport pairing against a test function

The hypotheses on the drift b (jointly measurable, bounded, periodic, divergence free) are packaged as DriftHyp. For a test function φ, the pairing b·∇φ is measurable and bounded on the space-time cell, so it is square integrable there.

structure AVenhance.Infra.FullTheorem.TransportLimit.DriftHyp (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

The standing hypotheses on the drift.

• meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))
• bdd : ∃ (B : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ B
• per (t : ℝ) : t ∈ Set.Icc 0 1 → IsZ2Periodic (b t)
• div : IsDivFree b

theorem AVenhance.Infra.FullTheorem.TransportLimit.timeCube_measurableSet' : MeasurableSet timeCube

instance AVenhance.Infra.FullTheorem.TransportLimit.transportFiniteUnitCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

instance AVenhance.Infra.FullTheorem.TransportLimit.transportFiniteTimeCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.FullTheorem.TransportLimit.timeCube_subset_Icc : timeCube ⊆ Set.Icc 0 1 ×ˢ Set.univ

theorem AVenhance.Infra.FullTheorem.TransportLimit.DriftHyp.meas_timeCube {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (h : DriftHyp b) : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.FullTheorem.TransportLimit.DriftHyp.bound_timeCube {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (h : DriftHyp b) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ p ∈ timeCube, ‖b p.1 p.2‖ ≤ B

Pointwise bound on the drift over the space-time cell.

theorem AVenhance.Infra.FullTheorem.TransportLimit.spaceGrad_spacetime_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) : Continuous fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (φ p.1) p.2

theorem AVenhance.Infra.FullTheorem.TransportLimit.grad_bound {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsTestFunction φ) : ∃ (Cg : Fin 2 → ℝ), ∀ (i : Fin 2), 0 ≤ Cg i ∧ ∀ p ∈ timeCube, |spaceGrad (φ p.1) p.2 i| ≤ Cg i

Coordinatewise bound for the spatial gradient of a test function on the cell.

theorem AVenhance.Infra.FullTheorem.TransportLimit.transport_grad_term {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (h : DriftHyp b) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsTestFunction φ) : ∃ (Gb : ℝ), MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (b p.1 p.2) (spaceGrad (φ p.1) p.2)) (MeasureTheory.volume.restrict timeCube) ∧ ∀ p ∈ timeCube, |Homogenization.vecDot (b p.1 p.2) (spaceGrad (φ p.1) p.2)| ≤ Gb

The pairing b·∇φ is measurable and bounded on the space-time cell.

theorem AVenhance.Infra.FullTheorem.TransportLimit.memLp_two_of_bdd_timeCube {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict timeCube)) {C : ℝ} (hC : ∀ p ∈ timeCube, |F p| ≤ C) : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict timeCube)

A measurable function bounded on the space-time cell is square integrable there.

theorem AVenhance.Infra.FullTheorem.TransportLimit.integrable_mul_bdd_timeCube {F G : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict timeCube)) (hG : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict timeCube)) {C : ℝ} (hC : ∀ p ∈ timeCube, |G p| ≤ C) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => F p * G p) (MeasureTheory.volume.restrict timeCube)

The product of a square-integrable function with a bounded measurable one is integrable.