Bounded measurable coefficients acting on L² (general elliptic operator)

To pass from the Poisson form ∑ᵢ ⟪∂ᵢu, ∂ᵢv⟫ to the general divergence-form operator L u = -Dⱼ(aᵢⱼ Dᵢu) + bᵢ Dᵢu + c u we need to multiply an L² gradient component by a bounded measurable coefficient and still land in L². This file provides

• mulCoeffL : a bounded measurable scalar f (|f| ≤ M) acting on L²(Ω) as a continuous linear map g ↦ [f · g], with operator-norm bound M;
• mulCoeffL_coeFn : its pointwise a.e. representative x ↦ f x · g x;
• EllipticCoeff : the bundle of a measurable, bounded, uniformly elliptic coefficient matrix a (Evans §6.1.1: ∑ aᵢⱼ ξᵢ ξⱼ ≥ λ |ξ|²).

This mirrors, on the scalar PiLp encoding of Sobolev/Basic.lean, the coefficient action coeffMulLpL that DeGiorgi (WeakFormulation/CoefficientOperator.lean) builds on the vector-valued L²(Ω; E) encoding.

Pointwise multiplication by a bounded measurable coefficient

theorem EllipticPdes.Sobolev.memLp_mul_of_bdd {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {M : ℝ} (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, |f x| ≤ M) (g : L2D Ω) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin d)) => f x * ↑↑g x) 2 (MeasureTheory.volume.restrict Ω)

The pointwise product of a bounded measurable scalar function with an L² class is L².

noncomputable def EllipticPdes.Sobolev.mulCoeffCls {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {M : ℝ} (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, |f x| ≤ M) (g : L2D Ω) : L2D Ω

The L² class of f · g for a bounded measurable f.

Equations

• EllipticPdes.Sobolev.mulCoeffCls hf hM g = MeasureTheory.MemLp.toLp (fun (x : EuclideanSpace ℝ (Fin d)) => f x * ↑↑g x) ⋯

theorem EllipticPdes.Sobolev.mulCoeffCls_coeFn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {M : ℝ} (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, |f x| ≤ M) (g : L2D Ω) : ↑↑(mulCoeffCls hf hM g) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => f x * ↑↑g x

The class mulCoeffCls hf hM g has pointwise representative x ↦ f x · g x a.e.

noncomputable def EllipticPdes.Sobolev.mulCoeffLM {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {M : ℝ} (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, |f x| ≤ M) : L2D Ω →ₗ[ℝ] L2D Ω

A bounded measurable scalar f acting on L²(Ω) by pointwise multiplication, as a (bare) linear map g ↦ [f · g].

Equations

• EllipticPdes.Sobolev.mulCoeffLM hf hM = { toFun := EllipticPdes.Sobolev.mulCoeffCls hf hM, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EllipticPdes.Sobolev.mulCoeffL {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {M : ℝ} (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, |f x| ≤ M) : L2D Ω →L[ℝ] L2D Ω

A bounded measurable scalar f (|f| ≤ M) acting on L²(Ω) by pointwise multiplication, as a continuous linear map with operator norm ≤ M.

Equations

• EllipticPdes.Sobolev.mulCoeffL hf hM = (EllipticPdes.Sobolev.mulCoeffLM hf hM).mkContinuous M ⋯

@[simp]

theorem EllipticPdes.Sobolev.mulCoeffL_apply {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {M : ℝ} (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, |f x| ≤ M) (g : L2D Ω) : (mulCoeffL hf hM) g = mulCoeffCls hf hM g

Simp lemma: mulCoeffL hf hM g = mulCoeffCls hf hM g.

theorem EllipticPdes.Sobolev.mulCoeffL_coeFn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {M : ℝ} (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, |f x| ≤ M) (g : L2D Ω) : ↑↑((mulCoeffL hf hM) g) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => f x * ↑↑g x

The pointwise a.e. representative of the coefficient action.

theorem EllipticPdes.Sobolev.norm_mulCoeffL_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {M : ℝ} (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, |f x| ≤ M) (g : L2D Ω) : ‖(mulCoeffL hf hM) g‖ ≤ M * ‖g‖

Operator-norm bound for the coefficient action: ‖[f · g]‖ ≤ M ‖g‖.

theorem EllipticPdes.Sobolev.inner_mulCoeffL_eq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {M : ℝ} (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, |f x| ≤ M) (g h : L2D Ω) : inner ℝ ((mulCoeffL hf hM) g) h = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, f x * ↑↑g x * ↑↑h x

The inner product of the coefficient action against h is the integral of the triple product ∫_Ω f · g · h.

Uniformly elliptic coefficient matrices (Evans §6.1.1)

structure EllipticPdes.Sobolev.EllipticCoeff (d : ℕ) : Type

A measurable, bounded coefficient matrix a that is uniformly elliptic with ellipticity constant lam > 0 and sup bound Λ: ∑ᵢⱼ aᵢⱼ(x) ξᵢ ξⱼ ≥ lam · |ξ|² and |aᵢⱼ(x)| ≤ Λ for almost every x (Evans §6.1.1 states ellipticity pointwise for a.e. x ∈ U; the bundle has a measurable representative on ℝᵈ with the bounds holding volume-a.e., which restricts to a.e. on every domain Ω). This is exactly the data the divergence-form operator Lu = -Dⱼ(aᵢⱼ Dᵢu) needs for the energy estimate.

No symmetry is assumed, where Evans §6.1.1 assumes aᵢⱼ = aⱼᵢ throughout and Gilbarg-Trudinger ch. 8 assumes it for the principal part. Neither field above sees the antisymmetric part of a x: elliptic constrains the quadratic form ξ ↦ ∑ᵢⱼ aᵢⱼ ξᵢ ξⱼ, which the antisymmetric part annihilates, and bdd constrains the entries one at a time.

Symmetry is asked for at one place in the development, as the explicit hypothesis hAsymm : ∀ᵐ x ∂(volume.restrict Ω), ∀ i j, a x i j = a x j i of bilin_symm and of the spectral theorems above it (symmetric_fullElliptic_spectral and its bounded-set form). It enters there because the spectral theorem for compact self-adjoint operators asks the bilinear form to be symmetric, and bilin is symmetric exactly when a is (with the drift vanishing). Every other result of the library is proved for an arbitrary a: Gårding, existence and uniqueness, Fredholm, the resolvent bound, and the whole interior-regularity chain. With a non-symmetric the formal adjoint L* v = -Dᵢ(aᵢⱼ Dⱼv) - bⁱ Dᵢv + (c - Dᵢbⁱ)v has principal part built from the transpose, which is the transpose problem the Fredholm solvability criterion states.

• a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ

  The coefficient matrix entries.

• lam : ℝ

  Ellipticity constant.

• Λ : ℝ

  Uniform sup bound on the entries.

• lam_pos : 0 < self.lam

  The ellipticity constant is strictly positive.

• Λ_nonneg : 0 ≤ self.Λ

  The sup bound is nonnegative.

• measurable (i j : Fin d) : Measurable fun (x : EuclideanSpace ℝ (Fin d)) => self.a x i j

  Every entry of the matrix is measurable.

• bdd (i j : Fin d) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |self.a x i j| ≤ self.Λ

  Every entry is bounded by Λ almost everywhere.

• elliptic : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), ∀ (ξ : Fin d → ℝ), self.lam * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, self.a x i j * ξ i * ξ j

  The quadratic form of a x dominates lam · |ξ|² for almost every x.

noncomputable def EllipticPdes.Sobolev.EllipticCoeff.actL {d : ℕ} (A : EllipticCoeff d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (i j : Fin d) : L2D Ω →L[ℝ] L2D Ω

The (i, j) coefficient acting on L²(Ω).

Equations

• A.actL i j = EllipticPdes.Sobolev.mulCoeffL ⋯ ⋯

@[simp]

theorem EllipticPdes.Sobolev.EllipticCoeff.actL_coeFn {d : ℕ} (A : EllipticCoeff d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (i j : Fin d) (g : L2D Ω) : ↑↑((A.actL i j) g) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => A.a x i j * ↑↑g x

Simp lemma: A.actL i j g has pointwise representative x ↦ A.a x i j · g x a.e.

theorem EllipticPdes.Sobolev.EllipticCoeff.inner_actL_eq {d : ℕ} (A : EllipticCoeff d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (i j : Fin d) (g h : L2D Ω) : inner ℝ ((A.actL i j) g) h = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, A.a x i j * ↑↑g x * ↑↑h x

⟪A.actL i j g, h⟫ = ∫_Ω A.a x i j · g x · h x.

theorem EllipticPdes.Sobolev.EllipticCoeff.norm_actL_le {d : ℕ} (A : EllipticCoeff d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (i j : Fin d) (g : L2D Ω) : ‖(A.actL i j) g‖ ≤ A.Λ * ‖g‖

Operator-norm bound: ‖A.actL i j g‖ ≤ Λ · ‖g‖.