Pointwise weak gradients on a set

The Lᵖ-scale, pointwise-function analogue of HasWeakDerivOn: a function u has weak gradient g = (gₖ) on B when the integration by parts identity is satisfied against every smooth test function supported in B. This is the interface the Morrey embedding consumes; it is stated for functions (not Lp classes) and for a full gradient tuple so that a general exponent p > d is expressible, which the L²-only HasWeakDerivOn cannot do.

theorem EllipticPdes.Embedding.integrableOn_mul_bounded {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} {w h : EuclideanSpace ℝ (Fin d) → ℝ} (hw : MeasureTheory.IntegrableOn w B MeasureTheory.volume) (hc : Continuous h) {C : ℝ} (hC : ∀ (x : EuclideanSpace ℝ (Fin d)), ‖h x‖ ≤ C) : MeasureTheory.IntegrableOn (fun (x : EuclideanSpace ℝ (Fin d)) => w x * h x) B MeasureTheory.volume

Integrability against a bounded factor. An integrable class stays integrable when multiplied by a bounded measurable one, which is how every test function and every cutoff of this development enters an integral.

def EllipticPdes.Embedding.HasWeakGradOn {d : ℕ} (B : Set (EuclideanSpace ℝ (Fin d))) (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) : Prop

g is the pointwise weak gradient of u on B: integration by parts holds against every smooth compactly supported test function whose support lies in B. This mirrors EllipticPdes.Regularity.HasWeakDerivOn component-wise but for pointwise functions u, gₖ : EuclideanSpace ℝ (Fin d) → ℝ.

Equations

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

theorem EllipticPdes.Embedding.HasWeakGradOn.const_mul {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (c : ℝ) (h : HasWeakGradOn B u g) : HasWeakGradOn B (fun (x : EuclideanSpace ℝ (Fin d)) => c * u x) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => c * g k x

Scalar multiple of a weak gradient. A constant multiple of a class with a weak gradient has the same multiple of the gradient.

theorem EllipticPdes.Embedding.HasWeakGradOn.add {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} {u v : EuclideanSpace ℝ (Fin d) → ℝ} {g h : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.IntegrableOn u B MeasureTheory.volume) (hv : MeasureTheory.IntegrableOn v B MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.IntegrableOn (g k) B MeasureTheory.volume) (hh : ∀ (k : Fin d), MeasureTheory.IntegrableOn (h k) B MeasureTheory.volume) (hU : HasWeakGradOn B u g) (hV : HasWeakGradOn B v h) : HasWeakGradOn B (fun (x : EuclideanSpace ℝ (Fin d)) => u x + v x) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => g k x + h k x

Additivity of a weak gradient. Two classes with weak gradients on the same set add, and so do their gradients. The finite sum of local pieces the extension operator glues is built by iterating this.

theorem EllipticPdes.Embedding.hasWeakGradOn_zero {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} : HasWeakGradOn B (fun (x : EuclideanSpace ℝ (Fin d)) => 0) fun (x : Fin d) (x_1 : EuclideanSpace ℝ (Fin d)) => 0

Zero as its own weak gradient.

theorem EllipticPdes.Embedding.hasWeakGradOn_finsetSum {d : ℕ} {ι : Type u_1} (s : Finset ι) {B : Set (EuclideanSpace ℝ (Fin d))} {U : ι → EuclideanSpace ℝ (Fin d) → ℝ} {G : ι → Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hU : ∀ i ∈ s, MeasureTheory.IntegrableOn (U i) B MeasureTheory.volume) (hG : ∀ i ∈ s, ∀ (k : Fin d), MeasureTheory.IntegrableOn (G i k) B MeasureTheory.volume) (h : ∀ i ∈ s, HasWeakGradOn B (U i) (G i)) : HasWeakGradOn B (fun (y : EuclideanSpace ℝ (Fin d)) => ∑ i ∈ s, U i y) fun (k : Fin d) (y : EuclideanSpace ℝ (Fin d)) => ∑ i ∈ s, G i k y

Finite sum of classes with weak gradients, whose gradient is the sum. This is what glues the local pieces of the extension operator.

noncomputable def EllipticPdes.Embedding.morreyExponent (d : ℕ) (p : ℝ) : NNReal

The Morrey/Hölder exponent γ = 1 - d/p, as a ℝ≥0 (faithful when p > d).

Equations

• EllipticPdes.Embedding.morreyExponent d p = (1 - ↑d / p).toNNReal

theorem EllipticPdes.Embedding.coe_morreyExponent {d : ℕ} {p : ℝ} (hp : ↑d < p) (hd : 0 < d) : ↑(morreyExponent d p) = 1 - ↑d / p

When p > d, the Morrey exponent coerces back to 1 - d/p.