Gradient Estimates

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.FaaDiBruno.transportSolution_spatialGradient_hasDerivAt_alongFlow {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s t : ℝ) : HasDerivAt (fun (r : ℝ) => spatialDerivativeCLM (Function.uncurry Y) r (X r x s)) (spatialDerivativeCLM (Function.uncurry g) t (X t x s) - spatialDerivativeCLM (Function.uncurry Y) t (X t x s) ∘SL spatialDerivativeCLM (Function.uncurry b) t (X t x s)) t

Along a flow characteristic, the spatial derivative of a smooth transport solution solves the differentiated transport equation as a linear-map ODE.

theorem AVenhance.FaaDiBruno.transportSolution_spatialGradient_norm_le_forward {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hLip : ∃ (L : ℝ), ∀ (r : ℝ) (x z : Homogenization.Vec 2), ‖b r x - b r z‖ ≤ L * ‖x - z‖) {Lf Lg : ℝ} (hbD : ∀ (r : ℝ) (x : Homogenization.Vec 2), ‖spatialDerivativeCLM (Function.uncurry b) r x‖ ≤ Lf) (hgD : ∀ (r : ℝ) (x : Homogenization.Vec 2), ‖spatialDerivativeCLM (Function.uncurry g) r x‖ ≤ Lg) {t : ℝ} (ht : 0 ≤ t) (y : Homogenization.Vec 2) : ‖spatialDerivativeCLM (Function.uncurry Y) t y‖ ≤ gronwallBound 0 Lf Lg t

Grönwall bound for the differentiated transport solution along the characteristic ending at an arbitrary point at time t.

theorem AVenhance.FaaDiBruno.transportSolution_spatialGradient_norm_le_backward {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hLip : ∃ (L : ℝ), ∀ (r : ℝ) (x z : Homogenization.Vec 2), ‖b r x - b r z‖ ≤ L * ‖x - z‖) {Lf Lg : ℝ} (hbD : ∀ (r : ℝ) (x : Homogenization.Vec 2), ‖spatialDerivativeCLM (Function.uncurry b) r x‖ ≤ Lf) (hgD : ∀ (r : ℝ) (x : Homogenization.Vec 2), ‖spatialDerivativeCLM (Function.uncurry g) r x‖ ≤ Lg) {t : ℝ} (ht : t ≤ 0) (y : Homogenization.Vec 2) : ‖spatialDerivativeCLM (Function.uncurry Y) t y‖ ≤ gronwallBound 0 Lf Lg (-t)

The same endpoint derivative estimate for a characteristic traversed backward from time zero.

theorem AVenhance.FaaDiBruno.GradientEstimates.gronwallBound_zero_le_two_mul_of_small {K ε t : ℝ} (hK : 0 < K) (hε : 0 ≤ ε) (ht : 0 ≤ t) (hsmall : K * t ≤ 1) : gronwallBound 0 K ε t ≤ 2 * ε * t

theorem AVenhance.FaaDiBruno.GradientEstimates.exists_spatial_lipschitz_of_fderiv_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) {L : ℝ} (hL : 0 ≤ L) (hD : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖fderiv ℝ (b t) x‖ ≤ L) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ K * ‖x - y‖

theorem AVenhance.FaaDiBruno.GradientEstimates.transportField_spatialDerivative_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) {C R : ℝ} (hR : 0 < R) (hC : 0 ≤ C) (hB : ∀ (t : ℝ), snorm (b t) 1 R ≤ ENNReal.ofReal C) (t : ℝ) (x : Homogenization.Vec 2) : ‖spatialDerivativeCLM (Function.uncurry b) t x‖ ≤ 2 * C * R / 4

The source seminorm at order one supplies the pointwise spatial derivative bound used by the characteristic estimate.

theorem AVenhance.FaaDiBruno.transportSolution_snorm_one_equalRadius {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {C_f C_g R : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hB : ∀ (t : ℝ), snorm (b t) 1 R ≤ ENNReal.ofReal C_f) (hG : ∀ (t : ℝ), snorm (g t) 1 R ≤ ENNReal.ofReal C_g) {t : ℝ} (hT : |t| ≤ 1 / (8 * C_f * R)) : snorm (Y t) 1 (R * (1 + 8 * |t| * C_f * R)) ≤ ENNReal.ofReal (16 * C_g * |t|)

Equal-radius, order-one transport estimate for either sign of time.