Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.Terms.Assembly

Finite HDot⁻¹ assembly for the nine named Section 5 terms and R46. The exact residual identity is an explicit upstream input. Time measurability of prefix norms is also kept explicit, while spatial L² closure is proved.

source
noncomputable def AVenhance.Infra.Section5.section5Term {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (i : ℕ) :
ℝ → Homogenization.Vec 2 → ℝ

The ten source terms in the order used by nineTerms, followed by R46. Out-of-range indices return zero for convenient finite-prefix notation.

Equations
Instances For
    source
    noncomputable def AVenhance.Infra.Section5.section5Prefix {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (n : ℕ) :
    ℝ → Homogenization.Vec 2 → ℝ

    The pointwise sum of the first n named terms.

    Equations
    Instances For
      source
      theorem AVenhance.Infra.Section5.section5Prefix_succ {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (n : ℕ) :
      section5Prefix I hΦ m κm T d e (n + 1) = fun (t : ℝ) (x : Homogenization.Vec 2) => section5Prefix I hΦ m κm T d e n t x + section5Term I hΦ m κm T d e n t x
      source
      theorem AVenhance.Infra.Section5.section5Prefix_memL2 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (htermL2 : ∀ i < 10, ∀ t ∈ Set.Ioo 0 1, Homogenization.MemL2On unitCube (section5Term I hΦ m κm T d e i t)) (n : ℕ) (hn : n ≤ 10) (t : ℝ) (ht : t ∈ Set.Ioo 0 1) :
      Homogenization.MemL2On unitCube (section5Prefix I hΦ m κm T d e n t)

      Every finite prefix is spatially L² when its component terms are.

      source
      theorem AVenhance.Infra.Section5.section5Prefix_ten_eq_terms {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) :
      section5Prefix I hΦ m κm T d e 10 = fun (t : ℝ) (x : Homogenization.Vec 2) => nineTerms I hΦ m κm T d e t x + R46 I hΦ m κm T t x

      The ten-term prefix is exactly the residual sum nineTerms + R46.

      source
      theorem AVenhance.Infra.Section5.timeHMinusOneNorm_section5Prefix_le_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (htermL2 : ∀ i < 10, ∀ t ∈ Set.Ioo 0 1, Homogenization.MemL2On unitCube (section5Term I hΦ m κm T d e i t)) (htermMeas : ∀ i < 10, AEMeasurable (fun (t : ℝ) => hMinusOneNorm (section5Term I hΦ m κm T d e i t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) (hprefixMeas : ∀ (n : ℕ), 1 ≤ n → n < 10 → AEMeasurable (fun (t : ℝ) => hMinusOneNorm (section5Prefix I hΦ m κm T d e n t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) (n : ℕ) (hnpos : 1 ≤ n) (hn : n ≤ 10) :
      timeHMinusOneNorm (section5Prefix I hΦ m κm T d e n) ≤ ∑ i ∈ Finset.range n, timeHMinusOneNorm (section5Term I hΦ m κm T d e i)

      Triangle inequality for the first n terms in the exact BigBound time norm. Inputs are component L² regularity and time measurability of the terms and partial-prefix negative norms.