Linear algebra of iterated weak derivatives

The datum of the differentiated equation is a finite sum of signed terms, each a bounded weight against a derivative of the solution. EllipticPdes.Regularity.MulIterated supplies the weight; this file supplies the sum.

The same observation appears at three levels: weak differentiation is linear, so an order-k family of a sum is the entrywise sum of the families, and the triangle inequality turns a bound on each summand into a bound on the sum. The constants add rather than being optimised, which is all the induction of Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65) needs: its constant is quantified before the solution and the datum, and nothing constrains its size.

Main declarations

• HasWeakDerivOn.zero, HasWeakDerivOn.neg, HasWeakDerivOn.sum: linearity of the weak derivative on a region.
• HasIteratedWeakDerivOn.neg, .sub, .sum: the families.
• IteratedL2Bound.add, .neg, .sub, .sum: the bounds.

Linearity of the weak derivative

theorem EllipticPdes.Regularity.HasWeakDerivOn.zero {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {ℓ : Fin d} : HasWeakDerivOn V ℓ 0 0

The zero class has zero weak derivative: both sides of the integration by parts vanish.

theorem EllipticPdes.Regularity.HasWeakDerivOn.neg {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {ℓ : Fin d} {g g' : Sobolev.L2D V} (hg : HasWeakDerivOn V ℓ g g') : HasWeakDerivOn V ℓ (-g) (-g')

A weak derivative of a negation is the negation of the weak derivative.

theorem EllipticPdes.Regularity.HasWeakDerivOn.sum {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {ℓ : Fin d} {ι : Type u_1} {g g' : ι → Sobolev.L2D V} (h : ∀ (i : ι), HasWeakDerivOn V ℓ (g i) (g' i)) (s : Finset ι) : HasWeakDerivOn V ℓ (∑ i ∈ s, g i) (∑ i ∈ s, g' i)

A weak derivative of a finite sum is the sum of the weak derivatives.

Families

noncomputable def EllipticPdes.Regularity.HasIteratedWeakDerivOn.neg {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {g : Sobolev.L2D V} (hg : HasIteratedWeakDerivOn V k g) : HasIteratedWeakDerivOn V k (-g)

The order-k family of a negation, entry by entry.

Equations

• hg.neg = { D := fun (α : List (Fin d)) => -hg.D α, D_nil := ⋯, D_step := ⋯ }

noncomputable def EllipticPdes.Regularity.HasIteratedWeakDerivOn.sub {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {g h : Sobolev.L2D V} (hg : HasIteratedWeakDerivOn V k g) (hh : HasIteratedWeakDerivOn V k h) : HasIteratedWeakDerivOn V k (g - h)

The order-k family of a difference. The datum of the induction step is a signed combination, so subtraction is as basic here as addition.

Equations

• hg.sub hh = (hg.add hh.neg).congr ⋯

noncomputable def EllipticPdes.Regularity.HasIteratedWeakDerivOn.sum {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {ι : Type u_1} [Fintype ι] {g : ι → Sobolev.L2D V} (H : (i : ι) → HasIteratedWeakDerivOn V k (g i)) : HasIteratedWeakDerivOn V k (∑ i : ι, g i)

The order-k family of a finite sum, entry by entry.

Equations

• EllipticPdes.Regularity.HasIteratedWeakDerivOn.sum H = { D := fun (α : List (Fin d)) => ∑ i : ι, (H i).D α, D_nil := ⋯, D_step := ⋯ }

Bounds

theorem EllipticPdes.Regularity.IteratedL2Bound.add {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {C C' : ℝ} {g h : Sobolev.L2D V} {hg : HasIteratedWeakDerivOn V k g} {hh : HasIteratedWeakDerivOn V k h} (hC : IteratedL2Bound hg C) (hC' : IteratedL2Bound hh C') : IteratedL2Bound (hg.add hh) (C + C')

The bound on a sum of two families is the sum of the bounds.

theorem EllipticPdes.Regularity.IteratedL2Bound.neg {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {C : ℝ} {g : Sobolev.L2D V} {hg : HasIteratedWeakDerivOn V k g} (hC : IteratedL2Bound hg C) : IteratedL2Bound hg.neg C

A negation has the same bound.

theorem EllipticPdes.Regularity.IteratedL2Bound.sub {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {C C' : ℝ} {g h : Sobolev.L2D V} {hg : HasIteratedWeakDerivOn V k g} {hh : HasIteratedWeakDerivOn V k h} (hC : IteratedL2Bound hg C) (hC' : IteratedL2Bound hh C') : IteratedL2Bound (hg.sub hh) (C + C')

The bound on a difference of families is the sum of the bounds.

theorem EllipticPdes.Regularity.IteratedL2Bound.sum {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {ι : Type u_1} [Fintype ι] {g : ι → Sobolev.L2D V} {H : (i : ι) → HasIteratedWeakDerivOn V k (g i)} {C : ι → ℝ} (hC : ∀ (i : ι), IteratedL2Bound (H i) (C i)) : IteratedL2Bound (HasIteratedWeakDerivOn.sum H) (∑ i : ι, C i)

The bound on a finite sum of families is the sum of the bounds.