Bounded-domain instances of the Σ-spectrum results

SpectrumSigma.lean proves Existence III and the boundedness of the resolvent for the FULL operator (nonzero bⁱ, arbitrary sign of c) on any Ω, under the single hypothesis that the compact part opK is a compact operator. On a bounded measurable domain that hypothesis is a theorem (embL2_isCompact + opK_isCompact), so each result holds with no analytic hypotheses at all. These are the paper-facing statements.

theorem EllipticPdes.Sobolev.FullEllipticOp.existence_three_of_bounded {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) : ∃ (S : Set ℝ), S.Countable ∧ (∀ (C : ℝ), (S ∩ Set.Iic C).Finite) ∧ ∀ (lam : ℝ), lam ∉ S ↔ ∀ (f : L2D Ω), ∃! u : ↥(H01 Ω), ∀ (v : ↥(H01 Ω)), ((Op.fullBilin Ω) u) v = lam * inner ℝ ((↑u).ofLp 0) ((↑v).ofLp 0) + ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑((↑v).ofLp 0) x

Existence III on a bounded measurable domain.

theorem EllipticPdes.Sobolev.FullEllipticOp.notMem_sigmaSet_iff_solvable_of_bounded {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (lam : ℝ) : lam ∉ Op.sigmaSet Ω ↔ ∀ (f : ↥(H01 Ω) →L[ℝ] ℝ), ∃! u : ↥(H01 Ω), ∀ (v : ↥(H01 Ω)), ((Op.fullBilin Ω) u) v = lam * ((zerothForm Ω) u) v + f v

The Σ-membership characterisation on a bounded measurable domain.

theorem EllipticPdes.Sobolev.FullEllipticOp.sigmaSet_inter_Iic_finite_of_bounded {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (C : ℝ) : (Op.sigmaSet Ω ∩ Set.Iic C).Finite

Bounded-above slices of Σ are finite, on a bounded measurable domain.

theorem EllipticPdes.Sobolev.FullEllipticOp.resolvent_bound_of_bounded {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) {lam : ℝ} (hlam : lam ∉ Op.sigmaSet Ω) : ∃ (C : ℝ), 0 < C ∧ ∀ (f : L2D Ω) (u : ↥(H01 Ω)), (∀ (v : ↥(H01 Ω)), ((Op.fullBilin Ω) u) v = lam * inner ℝ ((↑u).ofLp 0) ((↑v).ofLp 0) + ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑((↑v).ofLp 0) x) → ‖(↑u).ofLp 0‖ ≤ C * ‖f‖

Resolvent bound on a bounded measurable domain.