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

Continuity and boundedness hypotheses for operators

This file packages continuity and local boundedness assumptions for fully nonlinear operators through operatorGraphEval, the graph-space evaluation map used by closed-semijet arguments.

def ViscositySolns.OperatorContinuous {n : ℕ} (F : Operator n) : Prop

An operator is continuous when its graph-space evaluation map is continuous.

Equations

• ViscositySolns.OperatorContinuous F = Continuous (ViscositySolns.operatorGraphEval F)

def ViscositySolns.OperatorContinuousOn {n : ℕ} (S : Set ((Point n × ℝ) × Jet n)) (F : Operator n) : Prop

An operator is continuous on a graph-space set when its graph-space evaluation map is continuous there.

Equations

• ViscositySolns.OperatorContinuousOn S F = ContinuousOn (ViscositySolns.operatorGraphEval F) S

def ViscositySolns.OperatorLocallyBounded {n : ℕ} (F : Operator n) : Prop

An operator is locally bounded when its graph-space evaluation is locally bounded.

Equations

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

def ViscositySolns.OperatorLocallyBoundedOn {n : ℕ} (S : Set ((Point n × ℝ) × Jet n)) (F : Operator n) : Prop

An operator is locally bounded on a graph-space set when its graph-space evaluation is locally bounded in the relative topology of that set.

Equations

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

theorem ViscositySolns.OperatorContinuous.continuous {n : ℕ} {F : Operator n} (hF : OperatorContinuous F) : Continuous (operatorGraphEval F)

theorem ViscositySolns.OperatorContinuousOn.continuousOn {n : ℕ} {S : Set ((Point n × ℝ) × Jet n)} {F : Operator n} (hF : OperatorContinuousOn S F) : ContinuousOn (operatorGraphEval F) S

theorem ViscositySolns.OperatorContinuous.operatorContinuousOn {n : ℕ} {S : Set ((Point n × ℝ) × Jet n)} {F : Operator n} (hF : OperatorContinuous F) : OperatorContinuousOn S F

theorem ViscositySolns.OperatorContinuous.isClosed_le_zero {n : ℕ} {F : Operator n} (hF : OperatorContinuous F) : IsClosed {z : (Point n × ℝ) × Jet n | operatorGraphEval F z ≤ 0}

theorem ViscositySolns.OperatorContinuous.isClosed_zero_le {n : ℕ} {F : Operator n} (hF : OperatorContinuous F) : IsClosed {z : (Point n × ℝ) × Jet n | 0 ≤ operatorGraphEval F z}

theorem ViscositySolns.OperatorContinuous.locallyBounded {n : ℕ} {F : Operator n} (hF : OperatorContinuous F) : OperatorLocallyBounded F

theorem ViscositySolns.OperatorContinuousOn.locallyBoundedOn {n : ℕ} {S : Set ((Point n × ℝ) × Jet n)} {F : Operator n} (hF : OperatorContinuousOn S F) : OperatorLocallyBoundedOn S F

theorem ViscositySolns.OperatorContinuous.locallyBoundedOn {n : ℕ} {S : Set ((Point n × ℝ) × Jet n)} {F : Operator n} (hF : OperatorContinuous F) : OperatorLocallyBoundedOn S F

theorem ViscositySolns.OperatorLocallyBounded.locallyBoundedOn {n : ℕ} {S : Set ((Point n × ℝ) × Jet n)} {F : Operator n} (hF : OperatorLocallyBounded F) : OperatorLocallyBoundedOn S F