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

Finite suprema and infima of operators

This file contains pointwise finite suprema and infima of second-order operators. These constructions are the finite-index versions of the Hamilton-Jacobi-Bellman and Isaacs operators appearing in viscosity theory.

def ViscositySolns.supOperator {n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] (F : α → Operator n) : Operator n

The pointwise supremum of a nonempty finite family of operators.

For each (x, r, p, X), this is the maximum of the finite set of real numbers F a x r p X.

Equations

• ViscositySolns.supOperator F x r p X = Finset.univ.sup' ⋯ fun (a : α) => F a x r p X

def ViscositySolns.infOperator {n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] (F : α → Operator n) : Operator n

The pointwise infimum of a nonempty finite family of operators.

For each (x, r, p, X), this is the minimum of the finite set of real numbers F a x r p X.

Equations

• ViscositySolns.infOperator F x r p X = Finset.univ.inf' ⋯ fun (a : α) => F a x r p X

@[simp]

theorem ViscositySolns.supOperator_apply {n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] (F : α → Operator n) (x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : supOperator F x r p X = Finset.univ.sup' ⋯ fun (a : α) => F a x r p X

@[simp]

theorem ViscositySolns.infOperator_apply {n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] (F : α → Operator n) (x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : infOperator F x r p X = Finset.univ.inf' ⋯ fun (a : α) => F a x r p X

theorem ViscositySolns.DegenerateElliptic.supOperator {n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] {F : α → Operator n} (hF : ∀ (a : α), DegenerateElliptic (F a)) : DegenerateElliptic (ViscositySolns.supOperator F)

theorem ViscositySolns.DegenerateElliptic.infOperator {n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] {F : α → Operator n} (hF : ∀ (a : α), DegenerateElliptic (F a)) : DegenerateElliptic (ViscositySolns.infOperator F)

theorem ViscositySolns.Proper.supOperator {n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] {F : α → Operator n} (hF : ∀ (a : α), Proper (F a)) : Proper (ViscositySolns.supOperator F)

theorem ViscositySolns.Proper.infOperator {n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] {F : α → Operator n} (hF : ∀ (a : α), Proper (F a)) : Proper (ViscositySolns.infOperator F)

theorem ViscositySolns.OperatorContinuous.supOperator {n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] {F : α → Operator n} (hF : ∀ (a : α), OperatorContinuous (F a)) : OperatorContinuous (ViscositySolns.supOperator F)

theorem ViscositySolns.OperatorContinuous.infOperator {n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] {F : α → Operator n} (hF : ∀ (a : α), OperatorContinuous (F a)) : OperatorContinuous (ViscositySolns.infOperator F)