Uniform interior difference-quotient norm bound

The master energy bound of EllipticPdes.Regularity.Interior.EnergyBound is run along a cutoff tower to produce a bound on ‖Dₖ^h (ζ ∂ᵢu)‖ that is uniform in the step h, which is the hypothesis the weak-limit converse consumes to produce the second weak derivative.

Main declarations

• interior_diffQuot_norm_bound: the h-uniform bound on the difference quotient of the cut-off first derivatives.

Uniform difference-quotient norm bound for the limit passage

theorem EllipticPdes.Regularity.interior_diffQuot_norm_bound {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) (hΩm : MeasurableSet Ω) (hA : IsLipCoeff Op.toEllipticCoeff) {V : Set (EuclideanSpace ℝ (Fin d))} (T : CutoffTower Ω V) (k i : Fin d) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∀ (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω), (∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) → ∃ (M : ℝ), 0 ≤ M ∧ (∀ (h : ℝ), h ≠ 0 → ‖(diffQuot k h) ((extendL2 hΩm) ((mulTest ⋯) ((↑u).ofLp i.succ)))‖ ≤ M) ∧ M ≤ Cd * (‖f‖ + ‖(↑u).ofLp 0‖)

Uniform difference-quotient norm bound (Evans §5.8.2 / §6.3.1). For a cutoff tower T and each (k, i), there is a constant Cd such that every weak solution u of L u = f has the whole-space difference quotient of the extension of ζ · ∂ᵢu bounded in L² by M, uniformly over all steps h ≠ 0, with M ≤ Cd (‖f‖ + ‖u₀‖). The step-uniform bound M depends on u and f; Cd is quantified before both, so it depends only on λ, Λ, A₁, d, γ, ‖b‖∞, ‖c‖∞ and the tower. For small h the discrete Leibniz split localises the difference quotient onto the master energy bound (interior_diffQuot_energy_bound) and the first-order energy; for large h the crude operator bound ‖Dₖʰ g‖ ≤ 2‖g‖/|h| closes it. This uniform bound is exactly the hypothesis of the weak-limit converse weakDeriv_of_diffQuot_bounded.