Measurability of t ↦ ‖F t‖_{HDot⁻¹} via a countable family of tests

The hMinusOneNorm is a supremum over an uncountable family of smooth periodic tests. On L²(unitCube) it is already computed by a countable family of admissible tests: the classes of the admissible tests in Lp ℝ 2 (volume.restrict unitCube) form a separable subset of a second-countable space, and φ ↦ ∫ g φ is the (continuous) L² inner product with g.

Consequently, if the slices F t are L² and every continuous pairing t ↦ ∫ F t φ is measurable, so is t ↦ ‖F t‖_{HDot⁻¹} (aemeasurable_hMinusOneNorm); and this applies to jointly continuous F on (0,1) × ℝ² (aemeasurable_hMinusOneNorm_of_continuousOn).

Continuous functions are L² on the cube

theorem AVenhance.Infra.Section5.Integration.memL2On_unitCube_of_continuous {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : Homogenization.MemL2On unitCube f

Continuous functions are L² on the unit cube.

A countable family of tests

@[reducible, inline]

abbrev AVenhance.Infra.Section5.Integration.HMinusTest : Type

The admissible-test subtype of the definition of hMinusOneNorm.

Equations

• AVenhance.Infra.Section5.Integration.HMinusTest = { φ : Homogenization.Vec 2 → ℝ // ContDiff ℝ (↑⊤) φ ∧ AVenhance.IsZ2Periodic φ ∧ AVenhance.gradNormSq (AVenhance.spaceGrad φ) ≤ 1 }

noncomputable def AVenhance.Infra.Section5.Integration.HMinusTest.toLp (φ : HMinusTest) : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict unitCube))

The L²(unitCube) class of an admissible test.

Equations

• φ.toLp = MeasureTheory.MemLp.toLp ↑φ ⋯

theorem AVenhance.Infra.Section5.Integration.integral_mul_eq_inner {g φ : Homogenization.Vec 2 → ℝ} (hg : Homogenization.MemL2On unitCube g) (hφ : Homogenization.MemL2On unitCube φ) : ∫ (x : Homogenization.Vec 2) in unitCube, g x * φ x = inner ℝ (MeasureTheory.MemLp.toLp g hg) (MeasureTheory.MemLp.toLp φ hφ)

The pairing ∫ g φ of an L² function with a continuous function is an L² inner product.

theorem AVenhance.Infra.Section5.Integration.continuous_ofReal_abs_inner (w : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict unitCube))) : Continuous fun (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict unitCube))) => ENNReal.ofReal |inner ℝ w u|

Continuity of u ↦ ofReal |⟪g, u⟫| on L².

theorem AVenhance.Infra.Section5.Integration.secondCountable_L2_unitCube : SecondCountableTopology ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict unitCube))

L² of the cube is second countable.

def AVenhance.Infra.Section5.Integration.zeroHMinusTest : HMinusTest

The zero function is an admissible test.

Equations

• AVenhance.Infra.Section5.Integration.zeroHMinusTest = ⟨fun (x : Homogenization.Vec 2) => 0, AVenhance.Infra.Section5.Integration.zeroHMinusTest._proof_2⟩

theorem AVenhance.Infra.Section5.Integration.exists_countable_hMinusOneNorm_tests : ∃ (φ : ℕ → Homogenization.Vec 2 → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑⊤) (φ n) ∧ IsZ2Periodic (φ n) ∧ gradNormSq (spaceGrad (φ n)) ≤ 1) ∧ ∀ (g : Homogenization.Vec 2 → ℝ), Homogenization.MemL2On unitCube g → hMinusOneNorm g = ⨆ (n : ℕ), ENNReal.ofReal |∫ (x : Homogenization.Vec 2) in unitCube, g x * φ n x|

A fixed countable family of admissible HDot⁻¹ tests computing the norm of every L² function.

Measurability in time

theorem AVenhance.Infra.Section5.Integration.aemeasurable_hMinusOneNorm {F : ℝ → Homogenization.Vec 2 → ℝ} (hL2 : ∀ t ∈ Set.Ioo 0 1, Homogenization.MemL2On unitCube (F t)) (hpair : ∀ (φ : Homogenization.Vec 2 → ℝ), Continuous φ → AEMeasurable (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, F t x * φ x) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) : AEMeasurable (fun (t : ℝ) => hMinusOneNorm (F t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

The HDot⁻¹ norm of L² slices is a.e. measurable once all continuous pairings are.

theorem AVenhance.Infra.Section5.Integration.continuous_slice_of_continuousOn {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ioo 0 1 ×ˢ Set.univ)) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : Continuous (F t)

Slices of a function jointly continuous on (0,1) × ℝ² are continuous.

theorem AVenhance.Infra.Section5.Integration.memL2On_of_continuousOn_slice {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ioo 0 1 ×ˢ Set.univ)) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : Homogenization.MemL2On unitCube (F t)

Slices of a jointly continuous function are L² on the cube.

theorem AVenhance.Infra.Section5.Integration.continuousOn_pairing_of_continuousOn {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ioo 0 1 ×ˢ Set.univ)) {φ : Homogenization.Vec 2 → ℝ} (hφ : Continuous φ) : ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, F t x * φ x) (Set.Ioo 0 1)

The pairing of a jointly continuous function with a continuous test is continuous in time.

theorem AVenhance.Infra.Section5.Integration.aemeasurable_hMinusOneNorm_of_continuousOn {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ioo 0 1 ×ˢ Set.univ)) : AEMeasurable (fun (t : ℝ) => hMinusOneNorm (F t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

The HDot⁻¹ norm is a.e. measurable in time for functions jointly continuous on (0,1) × ℝ².