Growth

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Flow.Growth.gronwallBound_zero_scale_third (L a c d : ℝ) : gronwallBound 0 L (c * a) d = c * gronwallBound 0 L a d

noncomputable def AVenhance.Infra.Flow.flowThirdVariationGrowthConstant (M C₂ C₃ s t : ℝ) : ℝ

The uniform growth constant for the third variation on [s,t].

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Flow.flowThirdVariation_bound_all_times_of_le {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 t : ℝ) (hst : s ≤ t) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (M C₂ C₃ : ℝ) (hM₀ : 0 ≤ M) (hM : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖jointSpatialFDeriv b t x‖ ≤ M) (hC₂₀ : 0 ≤ C₂) (hC₂ : ∀ (t : ℝ) (x h k : Homogenization.Vec 2), ‖spatialSecondDerivativeEval b t x h k‖ ≤ C₂ * ‖h‖ * ‖k‖) (hC₃₀ : 0 ≤ C₃) (hC₃ : ∀ (t : ℝ) (x h k l : Homogenization.Vec 2), ‖spatialThirdDerivativeEval b t x h k l‖ ≤ C₃ * ‖h‖ * ‖k‖ * ‖l‖) : ∃ (K : ℝ), 0 ≤ K ∧ K = flowThirdVariationGrowthConstant M C₂ C₃ s t ∧ ∀ (h k l : Homogenization.Vec 2), ∀ q ∈ Set.Icc s t, ‖flowThirdVariation hb hX x s hV h k l q 0 s‖ ≤ K * ‖h‖ * ‖k‖ * ‖l‖

The third variation has a uniform trilinear growth bound on forward compact time intervals.

theorem AVenhance.Infra.Flow.exists_flowThirdVariationContinuousLinear_left_of_le {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 t : ℝ) (hst : s ≤ t) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (k l : Homogenization.Vec 2) : ∃ (L : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2), ∀ (h : Homogenization.Vec 2), L h = flowThirdVariation hb hX x s hV h k l t 0 s

On a forward compact time interval, fixing the second and third directions makes the third variation a continuous linear map in its differentiating direction.

theorem AVenhance.Infra.Flow.exists_flowThirdVariationContinuousTrilinear_of_le {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 t : ℝ) (hst : s ≤ t) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) : ∃ (B : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2), ∀ (h k l : Homogenization.Vec 2), ((B h) k) l = flowThirdVariation hb hX x s hV h k l t 0 s

On a forward compact time interval, the third variation is represented by a continuous trilinear map in all three directions.