Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.LeftToShow.Defs

Objects of the §5.3 additive energy estimate e.left.to.show #

Source: enhance.tex 8271–8882. The matrix field F(t,x) = ∑_{k∈2ℤ+1} ξ_{m,k}(t) (I + ∇Χ_{m,k}) ∘ X⁻¹_{m-1,l_k}(t,x) (8298–8302), the leading term F ∇T_{m-1} of e.leadingord, the space average ⟨FᵗF⟩(t) of e.ergodic.break.up, and the material gradient D_{t,m-1} ∇T_{m-1} of e.barf.cascade.

Conventions: gradMatrix Χ x has entry (i,j) = ∂_{x_i} χ_{e_j} (e.gradcorrmatrix), so the leading term is the matrix–vector product F.mulVec (∇T).

source
noncomputable def AVenhance.Infra.Section5.LeftToShow.leadingMatrix {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm t : ℝ) (x : Homogenization.Vec 2) :
Matrix (Fin 2) (Fin 2) ℝ

F(t,x) := ∑_{k∈2ℤ+1} ξ_{m,k}(t) (I + ∇Χ_{m,k}(t,·)) ∘ X⁻¹_{m-1,l_k}(t,x) (source 8298–8302), with κm = κ_m the diffusivity of the correctors. For each t only finitely many summands are nonzero (xiMK_odd_support_finite).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def AVenhance.Infra.Section5.LeftToShow.leadingGrad {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) :
    Homogenization.Vec 2

    The leading-order gradient F ∇T_{m-1} of e.leadingord / e.left.to.show.

    Equations
    Instances For
      source
      noncomputable def AVenhance.Infra.Section5.LeftToShow.leadingGramAvg {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm t : ℝ) :
      Matrix (Fin 2) (Fin 2) ℝ

      The space average ⟨FᵗF⟩(t) of e.ergodic.break.up / e.bracket.FF.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def AVenhance.Infra.Section5.LeftToShow.materialGrad (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) :
        Homogenization.Vec 2

        The material gradient D_t ∇T = (∂_t + b·∇)∇T, componentwise (e.D.t.m.def, e.barf.cascade with b = b_{m-1}).

        Equations
        Instances For