Space-time transfer for the tiny source contract

If a nonnegative function f of time is dominated on (0,1) by a nonnegative combination of the slice energies ‖V_j(t)‖²_{L²} of fields continuous on [0,1] × ℝ², then its lower integral over (0,1) is dominated by the same combination of the space-time energies. The fields used are the gradients of the spatial words applied to the last increment T_{N*} - T_{N*-1}.

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

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

theorem AVenhance.Infra.Section5.Contracts.sc_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

theorem AVenhance.Infra.Section5.Contracts.sc_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)

theorem AVenhance.Infra.Section5.Contracts.sc_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)

theorem AVenhance.Infra.Section5.Contracts.sc_lintegral_le_of_slices {ι : Type u_1} (S : Finset ι) {V : ι → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {c : ι → ℝ} (hc : ∀ j ∈ S, 0 ≤ c j) (hV : ∀ j ∈ S, ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V j p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)) {f : ℝ → ENNReal} (hf : ∀ t ∈ Set.Ioo 0 1, f t ≤ ENNReal.ofReal (∑ j ∈ S, c j * gradNormSq (V j t))) : ∫⁻ (t : ℝ) in Set.Ioo 0 1, f t ≤ ENNReal.ofReal (∑ j ∈ S, c j * spaceTimeGradNormSq (V j))

Generic transfer. A slicewise domination of f by ∑ c_j ‖V_j(t)‖² gives the same domination of the lower integral of f by ∑ c_j ‖V_j‖²_{L²((0,1)×𝕋²)}.

noncomputable def AVenhance.Infra.Section5.Contracts.scWordGrad (u : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The gradient field of the word w applied to the time slices of u.

Equations

• AVenhance.Infra.Section5.Contracts.scWordGrad u w t x = AVenhance.spaceGrad (AVenhance.Infra.Section4.iterateSpatialWord w (u t)) x

theorem AVenhance.Infra.Section5.Contracts.sc_wordGrad_continuousOn {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (i : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => scWordGrad u w p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)

Gradients of spatial words of a function jointly C^∞ on the closed half space are continuous on [0,1] × ℝ².

theorem AVenhance.Infra.Section5.Contracts.sc_increment_contDiff {β : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hN : 1 ≤ Nstar β) (hTa : ContDiff ℝ (↑⊤) (T (Nstar β) t)) (hTb : ContDiff ℝ (↑⊤) (T (Nstar β - 1) t)) : ContDiff ℝ (↑⊤) (Section4.iterateIncrement T (Nstar β) t)

theorem AVenhance.Infra.Section5.Contracts.sc_wordEnergy_continuous {v : Homogenization.Vec 2 → ℝ} (hv : ContDiff ℝ (↑⊤) v) (w : List (Fin 2)) : Continuous fun (x : Homogenization.Vec 2) => Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord w v) x)

theorem AVenhance.Infra.Section5.Contracts.sc_slice_energy_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm κprev : ℝ} (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hN : 1 ≤ Nstar β) (hTa : ContDiff ℝ (↑⊤) (T (Nstar β) t)) (hTb : ContDiff ℝ (↑⊤) (T (Nstar β - 1) t)) (hAs : ContDiff ℝ (↑⊤) (scCoeff I hΦ m κm κprev t)) (hnd : Continuous (tinyNondivergencePart I hΦ m κm (iterateError I hΦ m κm κprev T) t)) {b cχ D r : ℝ} (hb : ∀ (x : Homogenization.Vec 2) (j k : Fin 2), |scCoeff I hΦ m κm κprev t x j k| ≤ b) (hχ : ∀ (k : ℤ) (x : Homogenization.Vec 2) (j : Fin 2), |I.chiTilde hΦ m κm k t x j| ≤ cχ) (hD : 0 ≤ D) (hr : 1 ≤ r) (hAj : ∀ (x : Homogenization.Vec 2) (p : List (Fin 2)), p.length ≤ 2 → ∀ (j k : Fin 2), |Section4.iterateMatrixWord (scCoeff I hΦ m κm κprev t) p x j k| ≤ D * ↑p.length.factorial * r ^ p.length) : 4 * gradNormSq (iterateError I hΦ m κm κprev T t) + 2 * (2 * Real.pi)⁻¹ ^ 2 * l2NormSq (tinyNondivergencePart I hΦ m κm (iterateError I hΦ m κm κprev T) t) ≤ (16 * b ^ 2 + 2 * (2 * Real.pi)⁻¹ ^ 2 * (5184 * cχ ^ 2 * (14336 * D ^ 2 * r ^ 4))) * ∑ w ∈ scWords2, gradNormSq (scWordGrad (Section4.iterateIncrement T (Nstar β)) w t)

Slicewise energy domination. At a fixed time, the weighted sum of the energy of the error e_{m-1} and of the nondivergence part of tiny is bounded by the energies of the gradients of the words of length ≤ 2 of the last increment.