Spatial second derivatives at a local maximum and the barrier maximum principle for bounded solutions on the whole plane.

def AVenhance.Infra.Section3.ParabolicMaximum.coordinateLine (x : Homogenization.Vec 2) (i : Fin 2) : ℝ → Homogenization.Vec 2

Line through a point in one coordinate direction for the parabolic maximum argument.

Equations

• AVenhance.Infra.Section3.ParabolicMaximum.coordinateLine x i s = x + s • Homogenization.basisVec i

theorem AVenhance.Infra.Section3.ParabolicMaximum.coordinateLine_hasDerivAt (x : Homogenization.Vec 2) (i : Fin 2) (s : ℝ) : HasDerivAt (coordinateLine x i) (Homogenization.basisVec i) s

theorem AVenhance.Infra.Section3.spaceLap_nonpos_of_isLocalMax {f : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (hf : ContDiff ℝ 2 f) (hmax : IsLocalMax f x) : spaceLap f x ≤ 0

At a spatial local maximum of a C² function, every diagonal second partial derivative and hence its Laplacian is nonpositive.

theorem AVenhance.Infra.Section3.spaceTime_local_max_derivative_facts {f : ℝ × Homogenization.Vec 2 → ℝ} {t : ℝ} {x : Homogenization.Vec 2} (hf : ContDiff ℝ 2 f) (hmax : IsLocalMax f (t, x)) : deriv (fun (s : ℝ) => f (s, x)) t = 0 ∧ (∀ (i : Fin 2), spaceGrad (fun (y : Homogenization.Vec 2) => f (t, y)) x i = 0) ∧ spaceLap (fun (y : Homogenization.Vec 2) => f (t, y)) x ≤ 0

At a joint local maximum of a C² space-time function, the time derivative is zero, the spatial gradient vanishes, and the Laplacian is nonpositive.

theorem AVenhance.Infra.Section3.spaceGrad_sub {f g : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (i : Fin 2) (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : spaceGrad (fun (y : Homogenization.Vec 2) => f y - g y) x i = spaceGrad f x i - spaceGrad g x i

Coordinate derivative is linear under subtraction of differentiable functions.

theorem AVenhance.Infra.Section3.spaceLap_sub {f g : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 2 g) : spaceLap (fun (y : Homogenization.Vec 2) => f y - g y) x = spaceLap f x - spaceLap g x

Laplacian is linear under subtraction of C² functions.

def AVenhance.Infra.Section3.parabolicRadialSq (x : Homogenization.Vec 2) : ℝ

The quadratic coercive function used to localize a bounded parabolic maximum on the whole plane.

Equations

• AVenhance.Infra.Section3.parabolicRadialSq x = x 0 ^ 2 + x 1 ^ 2

theorem AVenhance.Infra.Section3.ParabolicMaximum.parabolicRadialSq_line_deriv (x : Homogenization.Vec 2) (i : Fin 2) : HasDerivAt (fun (s : ℝ) => parabolicRadialSq (coordinateLine x i s)) (2 * x i) 0

theorem AVenhance.Infra.Section3.spaceGrad_parabolicRadialSq (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad parabolicRadialSq x i = 2 * x i

Coordinate derivatives of the coercive quadratic on Vec 2.

theorem AVenhance.Infra.Section3.spaceGrad_scaledCoordinate (c : ℝ) (j i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => c * y j) x i = if i = j then c else 0

theorem AVenhance.Infra.Section3.spaceGrad_constantRadialSq (c : ℝ) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => c * (1 + parabolicRadialSq y)) x i = c * (2 * x i)

Spatial gradient of a constant multiple of the quadratic barrier.

theorem AVenhance.Infra.Section3.spaceLap_constantRadialSq (c : ℝ) (x : Homogenization.Vec 2) : spaceLap (fun (y : Homogenization.Vec 2) => c * (1 + parabolicRadialSq y)) x = 4 * c

Spatial Laplacian of a constant multiple of the quadratic barrier.

noncomputable def AVenhance.Infra.Section3.parabolicBarrier (ε A s : ℝ) (p : ℝ × Homogenization.Vec 2) : ℝ

Exponential quadratic barrier for the bounded whole-plane maximum principle.

Equations

• AVenhance.Infra.Section3.parabolicBarrier ε A s p = ε * (1 + AVenhance.Infra.Section3.parabolicRadialSq p.2) * Real.exp (A * (p.1 - s))

theorem AVenhance.Infra.Section3.parabolicBarrier_time_deriv (ε A s t : ℝ) (x : Homogenization.Vec 2) : deriv (fun (r : ℝ) => parabolicBarrier ε A s (r, x)) t = ε * A * Real.exp (A * (t - s)) * (1 + parabolicRadialSq x)

Time derivative of the exponential quadratic barrier.