Multilinear #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Flow.Multilinear.flowVariation_addDirection3
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(x : Homogenization.Vec 2)
(s t : ℝ)
(hV : IsFlow (linearizedFieldAlongFlow b X x s) V)
(h₁ h₂ : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Flow.Multilinear.flowVariation_smulDirection3
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(x : Homogenization.Vec 2)
(s t c : ℝ)
(hV : IsFlow (linearizedFieldAlongFlow b X x s) V)
(h : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Flow.flowThirdVariation_add_left
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlow b X)
{V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(x : Homogenization.Vec 2)
(s : ℝ)
(hV : IsFlow (linearizedFieldAlongFlow b X x s) V)
(h₁ h₂ k l : Homogenization.Vec 2)
(t : ℝ)
:
flowThirdVariation hb hX x s hV (h₁ + h₂) k l t 0 s = flowThirdVariation hb hX x s hV h₁ k l t 0 s + flowThirdVariation hb hX x s hV h₂ k l t 0 s
The selected third variational solution is additive in the direction that indexes the derivative of the second variation.
theorem
AVenhance.Infra.Flow.flowThirdVariation_add_middle
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlow b X)
{V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(x : Homogenization.Vec 2)
(s : ℝ)
(hV : IsFlow (linearizedFieldAlongFlow b X x s) V)
(h k₁ k₂ l : Homogenization.Vec 2)
(t : ℝ)
:
flowThirdVariation hb hX x s hV h (k₁ + k₂) l t 0 s = flowThirdVariation hb hX x s hV h k₁ l t 0 s + flowThirdVariation hb hX x s hV h k₂ l t 0 s
The selected third variational solution is additive in its middle direction.
theorem
AVenhance.Infra.Flow.flowThirdVariation_add_right
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlow b X)
{V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(x : Homogenization.Vec 2)
(s : ℝ)
(hV : IsFlow (linearizedFieldAlongFlow b X x s) V)
(h k l₁ l₂ : Homogenization.Vec 2)
(t : ℝ)
:
flowThirdVariation hb hX x s hV h k (l₁ + l₂) t 0 s = flowThirdVariation hb hX x s hV h k l₁ t 0 s + flowThirdVariation hb hX x s hV h k l₂ t 0 s
The selected third variational solution is additive in its right direction.
theorem
AVenhance.Infra.Flow.flowThirdVariation_smul_left
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlow b X)
{V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(x : Homogenization.Vec 2)
(s c : ℝ)
(hV : IsFlow (linearizedFieldAlongFlow b X x s) V)
(h k l : Homogenization.Vec 2)
(t : ℝ)
:
The selected third variational solution is homogeneous in the direction that indexes differentiation of the second variation.
theorem
AVenhance.Infra.Flow.flowThirdVariation_smul_middle
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlow b X)
{V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(x : Homogenization.Vec 2)
(s c : ℝ)
(hV : IsFlow (linearizedFieldAlongFlow b X x s) V)
(h k l : Homogenization.Vec 2)
(t : ℝ)
:
The selected third variational solution is homogeneous in its middle direction.
theorem
AVenhance.Infra.Flow.flowThirdVariation_smul_right
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlow b X)
{V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(x : Homogenization.Vec 2)
(s c : ℝ)
(hV : IsFlow (linearizedFieldAlongFlow b X x s) V)
(h k l : Homogenization.Vec 2)
(t : ℝ)
:
The selected third variational solution is homogeneous in its right direction.