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

Operator hypotheses for comparison

This file contains operator-level hypotheses that are designed for the doubling-of-variables comparison proof. The exact matrix inequality supplied by Ishii's lemma is kept as a parameter here; the comparison infrastructure will later instantiate that parameter with the block-matrix relation obtained from the maximum principle for semicontinuous functions.

def ViscositySolns.ComparisonModulus (ω : ℝ → ℝ) : Prop

A comparison modulus is a nonnegative real-valued function ω such that ω t -> 0 as t -> 0 with t > 0.

Equations

• ViscositySolns.ComparisonModulus ω = ((∀ (t : ℝ), 0 ≤ t → 0 ≤ ω t) ∧ Filter.Tendsto ω (nhdsWithin 0 (Set.Ioi 0)) (nhds 0))

theorem ViscositySolns.ComparisonModulus.zero : ComparisonModulus fun (_t : ℝ) => 0

The zero function is a comparison modulus.

theorem ViscositySolns.ComparisonModulus.nonneg {ω : ℝ → ℝ} (hω : ComparisonModulus ω) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ ω t

theorem ViscositySolns.ComparisonModulus.tendsto_zero {ω : ℝ → ℝ} (hω : ComparisonModulus ω) : Filter.Tendsto ω (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem ViscositySolns.ComparisonModulus.exists_pos_apply_lt {ω : ℝ → ℝ} (hω : ComparisonModulus ω) {ε : ℝ} (hε : 0 < ε) : ∃ (t : ℝ), 0 < t ∧ ω t < ε

If ω is a comparison modulus and ε > 0, then there exists t > 0 such that ω t < ε.

theorem ViscositySolns.ComparisonModulus.not_forall_pos_le_apply {ω : ℝ → ℝ} (hω : ComparisonModulus ω) {ε : ℝ} (hε : 0 < ε) : ¬∀ (t : ℝ), 0 < t → ε ≤ ω t

No positive number can be bounded above by ω t for every t > 0, when ω is a comparison modulus.

theorem ViscositySolns.ComparisonModulus.not_forall_pos_exists_between_apply {ω : ℝ → ℝ} (hω : ComparisonModulus ω) {ε : ℝ} (hε : 0 < ε) : ¬∀ (t : ℝ), 0 < t → ∃ (g : ℝ), ε ≤ g ∧ g ≤ ω t

Let ω be a comparison modulus and let ε > 0. It is impossible that for every t > 0 there exists a real number g with ε ≤ g ≤ ω t.

theorem ViscositySolns.ComparisonModulus.finset_sup' {ι : Type u_1} [Fintype ι] [Nonempty ι] {ω : ι → ℝ → ℝ} (hω : ∀ (a : ι), ComparisonModulus (ω a)) : ComparisonModulus fun (t : ℝ) => Finset.univ.sup' ⋯ fun (a : ι) => ω a t

Let ω a, for a in a nonempty finite type, be comparison moduli. Then the function

t ↦ max_{a} ω a t

is also a comparison modulus.

theorem ViscositySolns.ComparisonModulus.add {ω η : ℝ → ℝ} (hω : ComparisonModulus ω) (hη : ComparisonModulus η) : ComparisonModulus fun (t : ℝ) => ω t + η t

If ω and η are comparison moduli, then t ↦ ω t + η t is a comparison modulus.

theorem ViscositySolns.ComparisonModulus.const_mul_nonneg {ω : ℝ → ℝ} {a : ℝ} (ha : 0 ≤ a) (hω : ComparisonModulus ω) : ComparisonModulus fun (t : ℝ) => a * ω t

If ω is a comparison modulus and 0 ≤ a, then t ↦ a * ω t is a comparison modulus.

@[reducible, inline]

abbrev ViscositySolns.ComparisonMatrixRelation (n : ℕ) : Type

The type of matrix relations used in comparison hypotheses.

The arguments are the penalty parameter α, the two spatial points x and y, and the two Hessian matrices X and Y produced by the maximum principle.

Equations

• ViscositySolns.ComparisonMatrixRelation n = (ℝ → ViscositySolns.Point n → ViscositySolns.Point n → ViscositySolns.Hessian n → ViscositySolns.Hessian n → Prop)

def ViscositySolns.OperatorComparisonConditionOn {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (matrixRel : ComparisonMatrixRelation n) (F : Operator n) : Prop

Structural continuity condition for comparison on a set of spatial points C and scalar values R.

For every α > 0, every x, y ∈ C, every r ∈ R, and every pair of matrices X, Y satisfying the supplied matrix relation, the difference F y r (α • (x - y)) Y - F x r (α • (x - y)) X is bounded above by a modulus evaluated at α * ‖x - y‖ ^ 2 + ‖x - y‖.

Equations

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

theorem ViscositySolns.OperatorComparisonConditionOn.mono_scalar_set {n : ℕ} {C : Set (Point n)} {R S : Set ℝ} {matrixRel : ComparisonMatrixRelation n} {F : Operator n} (hF : OperatorComparisonConditionOn C S matrixRel F) (hRS : R ⊆ S) : OperatorComparisonConditionOn C R matrixRel F

theorem ViscositySolns.OperatorComparisonConditionOn.mono_spatial_set {n : ℕ} {C D : Set (Point n)} {R : Set ℝ} {matrixRel : ComparisonMatrixRelation n} {F : Operator n} (hF : OperatorComparisonConditionOn D R matrixRel F) (hCD : C ⊆ D) : OperatorComparisonConditionOn C R matrixRel F

theorem ViscositySolns.OperatorComparisonConditionOn.of_norm_bound {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {matrixRel : ComparisonMatrixRelation n} {F : Operator n} {ω : ℝ → ℝ} (hω : ComparisonModulus ω) (hmono : Monotone ω) (hbound : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), matrixRel α x y X Y → F y r (α • (x - y)) Y - F x r (α • (x - y)) X ≤ ω ‖x - y‖) : OperatorComparisonConditionOn C R matrixRel F

Let ω be a comparison modulus which is monotone on real numbers. Suppose that for every α > 0, every x, y ∈ C, every r ∈ R, and every X, Y satisfying matrixRel α x y X Y,

F y r (α • (x - y)) Y - F x r (α • (x - y)) X ≤ ω ‖x - y‖.

Then F satisfies OperatorComparisonConditionOn C R matrixRel, because ‖x - y‖ ≤ α * ‖x - y‖ ^ 2 + ‖x - y‖.

theorem ViscositySolns.OperatorComparisonConditionOn.of_nonpositive_difference {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {matrixRel : ComparisonMatrixRelation n} {F : Operator n} (hF : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), matrixRel α x y X Y → F y r (α • (x - y)) Y - F x r (α • (x - y)) X ≤ 0) : OperatorComparisonConditionOn C R matrixRel F

If the operator difference in the structural comparison condition is always nonpositive, then the structural comparison condition holds with the zero comparison modulus.

theorem ViscositySolns.OperatorComparisonConditionOn.constOperator {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (matrixRel : ComparisonMatrixRelation n) (c : ℝ) : OperatorComparisonConditionOn C R matrixRel (ViscositySolns.constOperator c)

Every constant operator satisfies the structural comparison condition, for any spatial set, scalar set, and matrix relation.

theorem ViscositySolns.OperatorComparisonConditionOn.addOperator {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {matrixRel : ComparisonMatrixRelation n} {F G : Operator n} (hF : OperatorComparisonConditionOn C R matrixRel F) (hG : OperatorComparisonConditionOn C R matrixRel G) : OperatorComparisonConditionOn C R matrixRel (ViscositySolns.addOperator F G)

If two operators satisfy the structural comparison condition on the same set C, scalar set R, and matrix relation, then their pointwise sum satisfies the same condition. The comparison modulus for the sum is the sum of the two comparison moduli.

theorem ViscositySolns.OperatorComparisonConditionOn.smulOperator_nonneg {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {matrixRel : ComparisonMatrixRelation n} {F : Operator n} {a : ℝ} (ha : 0 ≤ a) (hF : OperatorComparisonConditionOn C R matrixRel F) : OperatorComparisonConditionOn C R matrixRel (smulOperator a F)

If an operator satisfies the structural comparison condition on C, R, and matrixRel, then every nonnegative scalar multiple of it satisfies the same condition.

theorem ViscositySolns.OperatorComparisonConditionOn.supOperator_of_common_modulus {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {matrixRel : ComparisonMatrixRelation n} {F : ι → Operator n} {ω : ℝ → ℝ} (hω : ComparisonModulus ω) (hbound : ∀ (a : ι) (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), matrixRel α x y X Y → F a y r (α • (x - y)) Y - F a x r (α • (x - y)) X ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)) : OperatorComparisonConditionOn C R matrixRel (ViscositySolns.supOperator F)

Let F a be a nonempty finite family of operators. Suppose there is a single comparison modulus ω such that, for every index a, every α > 0, every x, y ∈ C, every r ∈ R, and every X, Y satisfying matrixRel α x y X Y,

F a y r (α • (x - y)) Y - F a x r (α • (x - y)) X ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖).

Then the pointwise supremum operator supOperator F satisfies OperatorComparisonConditionOn C R matrixRel.

theorem ViscositySolns.OperatorComparisonConditionOn.infOperator_of_common_modulus {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {matrixRel : ComparisonMatrixRelation n} {F : ι → Operator n} {ω : ℝ → ℝ} (hω : ComparisonModulus ω) (hbound : ∀ (a : ι) (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), matrixRel α x y X Y → F a y r (α • (x - y)) Y - F a x r (α • (x - y)) X ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)) : OperatorComparisonConditionOn C R matrixRel (ViscositySolns.infOperator F)

Let F a be a nonempty finite family of operators. Suppose there is a single comparison modulus ω such that, for every index a, every α > 0, every x, y ∈ C, every r ∈ R, and every X, Y satisfying matrixRel α x y X Y,

F a y r (α • (x - y)) Y - F a x r (α • (x - y)) X ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖).

Then the pointwise infimum operator infOperator F satisfies OperatorComparisonConditionOn C R matrixRel. The proof chooses an index where F a x r (α • (x - y)) X is minimal.

theorem ViscositySolns.OperatorComparisonConditionOn.supOperator {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {matrixRel : ComparisonMatrixRelation n} {F : ι → Operator n} (hF : ∀ (a : ι), OperatorComparisonConditionOn C R matrixRel (F a)) : OperatorComparisonConditionOn C R matrixRel (ViscositySolns.supOperator F)

Let F a be a nonempty finite family of operators. Suppose that for every index a, the operator F a satisfies OperatorComparisonConditionOn C R matrixRel. Then the pointwise supremum operator supOperator F also satisfies OperatorComparisonConditionOn C R matrixRel.

The proof takes the pointwise maximum of the finitely many comparison moduli associated to the branches F a.

theorem ViscositySolns.OperatorComparisonConditionOn.infOperator {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {matrixRel : ComparisonMatrixRelation n} {F : ι → Operator n} (hF : ∀ (a : ι), OperatorComparisonConditionOn C R matrixRel (F a)) : OperatorComparisonConditionOn C R matrixRel (ViscositySolns.infOperator F)

Let F a be a nonempty finite family of operators. Suppose that for every index a, the operator F a satisfies OperatorComparisonConditionOn C R matrixRel. Then the pointwise infimum operator infOperator F also satisfies OperatorComparisonConditionOn C R matrixRel.

The proof takes the pointwise maximum of the finitely many comparison moduli associated to the branches F a.