Space-time L² transfer for the flux source contracts

Generic measure-theoretic step: if the pointwise squared norm of a flux is dominated by a finite nonnegative combination of squared norms of fields V j that are continuous on [0,1] × ℝ², then the time-L²-of-space-L² norm of the flux (the left side of the *SourceContracts) is bounded by the square root of the same combination of the space-time L² norms of the V j.

Only the slices F t, t ∈ (0,1), of the flux are required to be continuous: the flux itself needs no joint regularity.

noncomputable def AVenhance.Infra.Section5.Contracts.saTimeL2 (F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ENNReal

The left side of the Twistie3SourceContract, Normie1SourceContract, Normie2SourceContract.

Equations

• AVenhance.Infra.Section5.Contracts.saTimeL2 F = (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(AVenhance.gradNormSq (F t)) ^ 2) ^ (1 / 2)

theorem AVenhance.Infra.Section5.Contracts.sa_gradNormSq_nonneg (F : Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ gradNormSq F

theorem AVenhance.Infra.Section5.Contracts.sa_lintegrand_eq (F : Homogenization.Vec 2 → Homogenization.Vec 2) : ENNReal.ofReal √(gradNormSq F) ^ 2 = ENNReal.ofReal (gradNormSq F)

theorem AVenhance.Infra.Section5.Contracts.sa_continuousOn_vecNormSq {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {s : Set (ℝ × Homogenization.Vec 2)} (hV : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V p.1 p.2 i) s) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (V p.1 p.2)) s

Joint continuity of the components gives continuity of the squared norm.

theorem AVenhance.Infra.Section5.Contracts.sa_sliceEnergy_continuousOn {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hV : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)) : ContinuousOn (fun (t : ℝ) => gradNormSq (V t)) (Set.Icc 0 1)

The slice energy of a field continuous on [0,1] × ℝ² is continuous in time.

theorem AVenhance.Infra.Section5.Contracts.sa_spaceTime_eq_integral {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hV : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)) : spaceTimeGradNormSq V = ∫ (t : ℝ) in Set.Ioo 0 1, gradNormSq (V t)

Fubini: the space-time norm is the time integral of the slice energies.

theorem AVenhance.Infra.Section5.Contracts.sa_slice_integrableOn {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hV : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => Homogenization.vecNormSq (V t x)) unitCube MeasureTheory.volume

theorem AVenhance.Infra.Section5.Contracts.saTimeL2_le {F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {V : Fin 3 → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {c : Fin 3 → ℝ} (hc : ∀ (j : Fin 3), 0 ≤ c j) (hV : ∀ (j : Fin 3) (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V j p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)) (hFc : ∀ t ∈ Set.Ioo 0 1, Continuous (F t)) (hpt : ∀ t ∈ Set.Ioo 0 1, ∀ (x : Homogenization.Vec 2), Homogenization.vecNormSq (F t x) ≤ ∑ j : Fin 3, c j * Homogenization.vecNormSq (V j t x)) : saTimeL2 F ≤ ENNReal.ofReal √(∑ j : Fin 3, c j * spaceTimeGradNormSq (V j))

Generic space-time transfer.

theorem AVenhance.Infra.Section5.Contracts.sa_spaceTimeGradNormSq_nonneg (V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ spaceTimeGradNormSq V

theorem AVenhance.Infra.Section5.Contracts.saTimeL2_le_of_pointwise {F V₀ V₁ V₂ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {k₀ k₁ k₂ : ℝ} (hk₀ : 0 ≤ k₀) (hk₁ : 0 ≤ k₁) (hk₂ : 0 ≤ k₂) (h₀ : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V₀ p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)) (h₁ : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V₁ p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)) (h₂ : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V₂ p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)) (hFc : ∀ t ∈ Set.Ioo 0 1, Continuous (F t)) (hpt : ∀ t ∈ Set.Ioo 0 1, ∀ (x : Homogenization.Vec 2), Homogenization.vecNormSq (F t x) ≤ k₀ ^ 2 * Homogenization.vecNormSq (V₀ t x) + k₁ ^ 2 * Homogenization.vecNormSq (V₁ t x) + k₂ ^ 2 * Homogenization.vecNormSq (V₂ t x)) : saTimeL2 F ≤ ENNReal.ofReal (k₀ * √(spaceTimeGradNormSq V₀) + k₁ * √(spaceTimeGradNormSq V₁) + k₂ * √(spaceTimeGradNormSq V₂))

Three-field form of the space-time transfer.