Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Doubling variables

This file contains the basic functions used in the doubling-of-variables argument for comparison theorems.

For functions u v : R^n -> R and a parameter α, the central expression is

u x - v y - (α / 2) * ∑ i, (x i - y i)^2.

The first-order components of the quadratic penalty are recorded explicitly as α • (x - y) and -α • (x - y).

@[reducible, inline]

abbrev ViscositySolns.DoubledPoint (n : ℕ) : Type

The product space used in the doubling-of-variables argument.

Equations

• ViscositySolns.DoubledPoint n = (ViscositySolns.Point n × ViscositySolns.Point n)

noncomputable def ViscositySolns.quadraticPenalty {n : ℕ} (α : ℝ) (x y : Point n) : ℝ

The coordinate quadratic penalty

(α / 2) * ∑ i, (x i - y i)^2.

This is the differentiable Euclidean quadratic form used in the matrix inequalities. The ambient topology on Point n is still Lean's finite product topology, and the finite-dimensional comparison lemmas in Foundation.lean relate this quadratic form to the norm used in little-oh statements.

Equations

• ViscositySolns.quadraticPenalty α x y = α / 2 * (x - y) ⬝ᵥ (x - y)

noncomputable def ViscositySolns.doubledObjective {n : ℕ} (u v : Point n → ℝ) (α : ℝ) (q : DoubledPoint n) : ℝ

The doubled-variable objective

u x - v y - (α / 2) * ∑ i, (x i - y i)^2.

Equations

• ViscositySolns.doubledObjective u v α q = u q.1 - v q.2 - ViscositySolns.quadraticPenalty α q.1 q.2

def ViscositySolns.quadraticPenaltyGradientLeft {n : ℕ} (α : ℝ) (x y : Point n) : Point n

The derivative of the quadratic penalty with respect to the first variable.

Equations

• ViscositySolns.quadraticPenaltyGradientLeft α x y = α • (x - y)

def ViscositySolns.quadraticPenaltyGradientRight {n : ℕ} (α : ℝ) (x y : Point n) : Point n

The derivative of the quadratic penalty with respect to the second variable.

Equations

• ViscositySolns.quadraticPenaltyGradientRight α x y = -α • (x - y)

def ViscositySolns.quadraticPenaltyHessianLeftLeft {n : ℕ} (α : ℝ) : Hessian n

The Hessian block of the quadratic penalty in the first variable.

Equations

• ViscositySolns.quadraticPenaltyHessianLeftLeft α = α • 1

def ViscositySolns.quadraticPenaltyHessianLeftRight {n : ℕ} (α : ℝ) : Hessian n

The mixed Hessian block of the quadratic penalty.

Equations

• ViscositySolns.quadraticPenaltyHessianLeftRight α = -α • 1

def ViscositySolns.quadraticPenaltyHessianRightRight {n : ℕ} (α : ℝ) : Hessian n

The Hessian block of the quadratic penalty in the second variable.

Equations

• ViscositySolns.quadraticPenaltyHessianRightRight α = α • 1

@[simp]

theorem ViscositySolns.quadraticPenalty_apply {n : ℕ} (α : ℝ) (x y : Point n) : quadraticPenalty α x y = α / 2 * (x - y) ⬝ᵥ (x - y)

@[simp]

theorem ViscositySolns.doubledObjective_apply {n : ℕ} (u v : Point n → ℝ) (α : ℝ) (x y : Point n) : doubledObjective u v α (x, y) = u x - v y - quadraticPenalty α x y

theorem ViscositySolns.quadraticPenalty_self {n : ℕ} (α : ℝ) (x : Point n) : quadraticPenalty α x x = 0

theorem ViscositySolns.quadraticPenalty_nonneg {n : ℕ} {α : ℝ} (hα : 0 ≤ α) (x y : Point n) : 0 ≤ quadraticPenalty α x y

theorem ViscositySolns.norm_weightedDistanceSq_le_quadraticPenalty_mul_two {n : ℕ} {α : ℝ} (hα : 0 ≤ α) (x y : Point n) : α * ‖x - y‖ ^ 2 ≤ 2 * quadraticPenalty α x y

theorem ViscositySolns.comparisonScale_nonneg {n : ℕ} {α : ℝ} (hα : 0 < α) (x y : Point n) : 0 ≤ α * ‖x - y‖ ^ 2 + ‖x - y‖

If α > 0, then 0 ≤ α * ‖x - y‖ ^ 2 + ‖x - y‖.

theorem ViscositySolns.comparisonScale_pos_of_ne {n : ℕ} {α : ℝ} (hα : 0 < α) {x y : Point n} (hxy : x ≠ y) : 0 < α * ‖x - y‖ ^ 2 + ‖x - y‖

If α > 0 and x ≠ y, then 0 < α * ‖x - y‖ ^ 2 + ‖x - y‖.

@[simp]

theorem ViscositySolns.quadraticPenaltyGradientRight_eq_neg_left {n : ℕ} (α : ℝ) (x y : Point n) : quadraticPenaltyGradientRight α x y = -quadraticPenaltyGradientLeft α x y

theorem ViscositySolns.neg_quadraticPenaltyGradientRight_eq_left {n : ℕ} (α : ℝ) (x y : Point n) : -quadraticPenaltyGradientRight α x y = quadraticPenaltyGradientLeft α x y

theorem ViscositySolns.continuous_quadraticPenalty {n : ℕ} (α : ℝ) : Continuous fun (q : DoubledPoint n) => quadraticPenalty α q.1 q.2

theorem ViscositySolns.continuous_doubledObjective {n : ℕ} {u v : Point n → ℝ} {α : ℝ} (hu : Continuous u) (hv : Continuous v) : Continuous fun (q : DoubledPoint n) => doubledObjective u v α q

theorem ViscositySolns.upperSemicontinuousOn_doubledObjective {n : ℕ} {K L : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} (hu : UpperSemicontinuousOn u K) (hv : LowerSemicontinuousOn v L) : UpperSemicontinuousOn (fun (q : DoubledPoint n) => doubledObjective u v α q) (K ×ˢ L)

If u is upper semicontinuous on K and v is lower semicontinuous on L, then the function (x, y) ↦ u x - v y - (α / 2) * ∑ i, (x i - y i)^2 is upper semicontinuous on K × L.

theorem ViscositySolns.exists_isMaxOn_doubledObjective_of_isCompact {n : ℕ} {K L : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u K) (hv : LowerSemicontinuousOn v L) : ∃ q ∈ K ×ˢ L, IsMaxOn (fun (z : DoubledPoint n) => doubledObjective u v α z) (K ×ˢ L) q

Let K and L be nonempty compact sets. If u is upper semicontinuous on K and v is lower semicontinuous on L, then there exists (x, y) ∈ K × L such that for every (x', y') ∈ K × L,

u x' - v y' - (α / 2) * ∑ i, (x' i - y' i)^2 ≤ u x - v y - (α / 2) * ∑ i, (x i - y i)^2.

theorem ViscositySolns.value_right_le_left_of_pos_gap_of_isMaxOn_doubledObjective {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} {x y z : Point n} (hα : 0 ≤ α) (hz : z ∈ C) (hgap : v z < u z) (hmax : IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v α q) (C ×ˢ C) (x, y)) : v y ≤ u x

Let u z - v z be positive at some z ∈ C. If (x, y) maximizes

(x', y') ↦ u x' - v y' - (α / 2) * ∑ i, (x' i - y' i)^2

on C × C and α ≥ 0, then v y ≤ u x.

theorem ViscositySolns.quadraticPenalty_le_value_sub_value_of_isMaxOn_doubledObjective {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} {x y : Point n} (hy : y ∈ C) (hmax : IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v α q) (C ×ˢ C) (x, y)) : quadraticPenalty α x y ≤ u x - u y

If (x, y) maximizes the doubled-variable objective on C × C and y ∈ C, then comparison with the diagonal point (y, y) gives

quadraticPenalty α x y ≤ u x - u y.

theorem ViscositySolns.quadraticPenalty_le_value_sub_value_at_diagonal_of_isMaxOn_doubledObjective {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} {x y z : Point n} (hz : z ∈ C) (hmax : IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v α q) (C ×ˢ C) (x, y)) : quadraticPenalty α x y ≤ u x - v y - (u z - v z)

If (x, y) maximizes the doubled-variable objective on C × C and z ∈ C, then comparison with the diagonal point (z, z) gives

quadraticPenalty α x y ≤ u x - v y - (u z - v z).

theorem ViscositySolns.weightedDistanceSq_le_two_value_range_of_isMaxOn_doubledObjective {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {α m M : ℝ} {x y : Point n} (hα : 0 ≤ α) (hy : y ∈ C) (hlo : m ≤ u y) (hhi : u x ≤ M) (hmax : IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v α q) (C ×ˢ C) (x, y)) : α * ‖x - y‖ ^ 2 ≤ 2 * (M - m)

Assume (x, y) maximizes the doubled-variable objective on C × C, y ∈ C, m ≤ u y, and u x ≤ M. Then

α * ‖x - y‖ ^ 2 ≤ 2 * (M - m).

theorem ViscositySolns.weightedDistanceSq_le_two_value_sub_value_at_diagonal_range_of_isMaxOn {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {α m M : ℝ} {x y z : Point n} (hα : 0 ≤ α) (hz : z ∈ C) (hlo : m ≤ v y) (hhi : u x ≤ M) (hmax : IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v α q) (C ×ˢ C) (x, y)) : α * ‖x - y‖ ^ 2 ≤ 2 * (M - m - (u z - v z))

Assume (x, y) maximizes the doubled-variable objective on C × C, z ∈ C, m ≤ v y, and u x ≤ M. Then

α * ‖x - y‖ ^ 2 ≤ 2 * (M - m - (u z - v z)).

theorem ViscositySolns.exists_eventually_isMaxOn_doubledObjective_along_of_isCompact {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} (hα : ∀ᶠ (i : ι) in l, 0 < α i) (hCne : C.Nonempty) (hCcompact : IsCompact C) (hu : UpperSemicontinuousOn u C) (hv : LowerSemicontinuousOn v C) : ∃ (x : ι → Point n) (y : ι → Point n), ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)

Let α i be a family of positive parameters for all i in a set belonging to a filter l. Let C be nonempty and compact. If u is upper semicontinuous on C and v is lower semicontinuous on C, then one can choose functions x i and y i such that, for all i in a set belonging to l, α i > 0, x i ∈ C, y i ∈ C, and (x i, y i) maximizes

(x', y') ↦ u x' - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2

on C × C.