Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.Amnr.AdvectionTermCounts

Exact spatial and material counts of ordered correction monomials.

source
def AVenhance.Infra.Section4.amnrTermSpatialCount (t : AmnrAdvectionTerm) :
ℕ

Total number of spatial derivatives in an advection term.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def AVenhance.Infra.Section4.amnrTermMaterialCount (t : AmnrAdvectionTerm) :
    ℕ

    Total number of material derivatives in an advection term.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem AVenhance.Infra.Section4.amnrAdvectionDerivativeTerms_counts (d : Option (Fin 2)) (A : List AmnrAdvectionFactor) (w : List (Option (Fin 2))) (t : AmnrAdvectionTerm) (ht : t ∈ amnrAdvectionDerivativeTerms d A w) :
      t.factors.length = A.length ∧ amnrTermSpatialCount t = amnrTermSpatialCount { factors := A, scalarWord := w } + amnrSpatialCount [d] ∧ amnrTermMaterialCount t = amnrTermMaterialCount { factors := A, scalarWord := w } + amnrMaterialCount [d]
      source
      theorem AVenhance.Infra.Section4.amnrChangedAdvectionDerivativeTerms_counts (a t : AmnrAdvectionTerm) (ht : t ∈ amnrChangedAdvectionDerivativeTerms a) :
      amnrTermMaterialCount t + t.factors.length = amnrTermMaterialCount a + a.factors.length + 1 ∧ amnrTermSpatialCount t = amnrTermSpatialCount a + (t.factors.length - a.factors.length) ∧ a.factors.length ≤ t.factors.length

      A coarse derivative adds one material letter; each fast-advection branch instead adds one spatial letter and one velocity factor.

      source
      theorem AVenhance.Infra.Section4.amnrCounts_replicate_none (n : ℕ) :
      amnrSpatialCount (List.replicate n none) = 0 ∧ amnrMaterialCount (List.replicate n none) = n
      source
      theorem AVenhance.Infra.Section4.amnrMaterialErrorTerms_counts (n : ℕ) (t : AmnrAdvectionTerm) (ht : t ∈ amnrMaterialErrorTerms n) :
      1 ≤ t.factors.length ∧ amnrTermSpatialCount t = t.factors.length ∧ amnrTermMaterialCount t + t.factors.length = n

      Every material error has a genuine fast factor. Its total counts are exact, so no highest-level material jet occurs in any correction factor.

      source
      theorem AVenhance.Infra.Section4.amnrAdvectionDerivativeTerms_scalar_spatial (d : Option (Fin 2)) (A : List AmnrAdvectionFactor) (w : List (Option (Fin 2))) (t : AmnrAdvectionTerm) (ht : t ∈ amnrAdvectionDerivativeTerms d A w) :
      amnrSpatialCount w ≤ amnrSpatialCount t.scalarWord

      Differentiating a monomial never removes a spatial scalar derivative.

      source
      theorem AVenhance.Infra.Section4.amnrChangedAdvectionDerivativeTerms_scalar_spatial (a t : AmnrAdvectionTerm) (ht : t ∈ amnrChangedAdvectionDerivativeTerms a) :
      amnrSpatialCount a.scalarWord ≤ amnrSpatialCount t.scalarWord
      source
      theorem AVenhance.Infra.Section4.amnrMaterialErrorTerms_scalar_spatial (n : ℕ) (t : AmnrAdvectionTerm) (ht : t ∈ amnrMaterialErrorTerms n) :
      1 ≤ amnrSpatialCount t.scalarWord

      The scalar in every material correction has a spatial derivative, so centering the coarse velocity loses no correction term.