Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Flow.HigherVariation3.Multilinear

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) :
V t (h₁ + h₂) s = V t h₁ s + V t h₂ s
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 : ℝ) :
flowThirdVariation hb hX x s hV (c • h) k l t 0 s = c • flowThirdVariation hb hX x s hV h k l t 0 s

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 : ℝ) :
flowThirdVariation hb hX x s hV h (c • k) l t 0 s = c • flowThirdVariation hb hX x s hV h k l t 0 s

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 : ℝ) :
flowThirdVariation hb hX x s hV h k (c • l) t 0 s = c • flowThirdVariation hb hX x s hV h k l t 0 s

The selected third variational solution is homogeneous in its right direction.