Documentation

Atlas.DifferentialAnalysis.code.DiffOpSobolev

Non-degeneracy of the Schwartz pairing: if a Schwartz function ψ pairs to zero against every Schwartz function via the canonical Schwartz-to-tempered-distribution embedding, then ψ = 0.

theorem DiffOpSobolev.hall_implies_eq (n : ) (ι : SchwartzMap (EuclideanSpace (Fin n)) →L[] TemperedDistribution (EuclideanSpace (Fin n)) ) ( : ι = SchwartzMap.toTemperedDistributionCLM (EuclideanSpace (Fin n)) MeasureTheory.volume) (u : TemperedDistribution (EuclideanSpace (Fin n)) ) (f₀ : SchwartzMap (EuclideanSpace (Fin n)) ) (S' : Finset (SchwartzMap (EuclideanSpace (Fin n)) )) (hf₀ : φS', (ι f₀) φ = u φ) (ψ : SchwartzMap (EuclideanSpace (Fin n)) ) (hall : ∀ (g : SchwartzMap (EuclideanSpace (Fin n)) ), (∀ φS', (ι g) φ = 0)(ι g) ψ = 0) :
(ι f₀) ψ = u ψ

Key inductive step for weak density: if f₀ already matches the distribution u on a finite set S' and any ψ annihilated by tests vanishing on S' is also annihilated by ι g, then ι f₀ ψ = u ψ.

Given any tempered distribution u and any finite set S of test functions, there exists a Schwartz function f whose Schwartz-distribution image agrees with u on every element of S.

The canonical embedding of Schwartz functions into tempered distributions has dense range with respect to the weak (pointwise) topology on distributions.

A tempered distribution u lies in the Sobolev space H^m if it is represented by integration against an element of SobolevSpace n m.

Instances For

    Action of a constant-coefficient differential operator P(D) on a distribution represented by a Sobolev H^s function: the result is represented by an H^{s-k} function, when the polynomial has degree at most k ≤ s.

    A constant-coefficient differential operator P(D) of degree k maps the Sobolev class H^s into H^{s-k} (Melrose, Section 10, Prop 10.2).

    def DiffOpSobolev.tailMultiIndexSum {n : } (α : Fin n) (k : ) :

    Sum of the components of a multi-index α over coordinates ≥ k.

    Instances For
      theorem DiffOpSobolev.tailMultiIndexSum_zero {n : } (α : Fin n) :
      tailMultiIndexSum α 0 = i : Fin n, α i

      The tail sum from index 0 equals the total sum of the multi-index.

      theorem DiffOpSobolev.tailMultiIndexSum_ge {n : } (α : Fin n) (k : ) (hk : n k) :

      If k ≥ n, the tail sum ∑_{i ≥ k} α i is empty and hence 0.

      theorem DiffOpSobolev.tailMultiIndexSum_succ {n : } (α : Fin n) (k : ) (hk : k < n) :

      Recurrence for the tail sum: peel off the term at index k.

      @[irreducible]

      Auxiliary recursion computing the multi-index iterated partial derivative on SobolevSpace n m' by processing coordinates starting at index k.

      Instances For
        noncomputable def DiffOpSobolev.multiIndexMonomial (n : ) (α : Fin n) :

        The monomial x^α := ∏ x_i^{α_i} viewed as a multivariate polynomial.

        Instances For
          theorem DiffOpSobolev.multiIndexDeriv_memHs (n : ) {m : } (α : Fin n) (u : TemperedDistribution (EuclideanSpace (Fin n)) ) (hu : SobolevSpace.MemHs n m u) :
          SobolevSpace.MemHs n (m - (∑ i : Fin n, α i)) (SobolevSpace.iteratedDistribDeriv n α u)

          Iterated distributional derivatives of order α map H^m to H^{m - |α|}.

          Iteratively multiplying by Fourier variables equals smul-left multiplication by the symbol of the monomial x^α, when acting on a distribution.

          theorem DiffOpSobolev.sobolev_witness_ae_unique (n : ) {s : } (g₁ g₂ : EuclideanSpace (Fin n)) (hg₁ : MeasureTheory.MemLp g₁ 2 MeasureTheory.volume) (hg₂ : MeasureTheory.MemLp g₂ 2 MeasureTheory.volume) (hint : ∀ (φ : SchwartzMap (EuclideanSpace (Fin n)) ), (ξ : EuclideanSpace (Fin n)), (↑(SobolevSpace.sobolevWeight n s ξ))⁻¹ * g₁ ξ * φ ξ = (ξ : EuclideanSpace (Fin n)), (↑(SobolevSpace.sobolevWeight n s ξ))⁻¹ * g₂ ξ * φ ξ) :

          Almost-everywhere uniqueness of the Sobolev L^2 witness: two L^2 functions that pair identically against all Schwartz functions via the weighted integral are equal a.e.

          Distributional derivative in the j-th direction maps Sobolev H^s witnesses to H^{s-1} witnesses, with the resulting L^2 representative bounded pointwise by (2π) ‖g‖.

          Iterated k-fold partial derivative in the j-th direction maps Sobolev H^s witnesses to H^{s-k} witnesses with L^2 representative bounded by (2π)^k ‖g‖.

          theorem DiffOpSobolev.memHs_foldr_with_bound (n : ) {s : } (l : List (Fin n)) (α : Fin n) (u : TemperedDistribution (EuclideanSpace (Fin n)) ) (g : EuclideanSpace (Fin n)) (hg_mem : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hg_eq : ∀ (φ : SchwartzMap (EuclideanSpace (Fin n)) ), (FourierTransform.fourier u) φ = (ξ : EuclideanSpace (Fin n)), (↑(SobolevSpace.sobolevWeight n s ξ))⁻¹ * g ξ * φ ξ) :
          ∃ (g_new : EuclideanSpace (Fin n)), MeasureTheory.MemLp g_new 2 MeasureTheory.volume (∀ (φ : SchwartzMap (EuclideanSpace (Fin n)) ), (FourierTransform.fourier (List.foldr (fun (i : Fin n) (acc : TemperedDistribution (EuclideanSpace (Fin n)) ) => SobolevSpace.iteratedPartialDerivDistrib n i (α i) acc) u l)) φ = (ξ : EuclideanSpace (Fin n)), (↑(SobolevSpace.sobolevWeight n (s - (List.map (fun (j : Fin n) => α j) l).sum) ξ))⁻¹ * g_new ξ * φ ξ) ∀ (ξ : EuclideanSpace (Fin n)), g_new ξ (2 * Real.pi) ^ (List.map (fun (j : Fin n) => α j) l).sum * g ξ

          Sequentially applying the iterated partial derivatives D_i^{α_i} along a list l of coordinates preserves the Sobolev structure with an L^2 witness bounded by (2π)^{Σ α} ‖g‖.

          theorem DiffOpSobolev.iteratedDistribDeriv_witness_ae_bound (n : ) {m : } (α : Fin n) (u : TemperedDistribution (EuclideanSpace (Fin n)) ) (g : EuclideanSpace (Fin n)) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hug : ∀ (φ : SchwartzMap (EuclideanSpace (Fin n)) ), (FourierTransform.fourier u) φ = (ξ : EuclideanSpace (Fin n)), (↑(SobolevSpace.sobolevWeight n m ξ))⁻¹ * g ξ * φ ξ) {g' : EuclideanSpace (Fin n)} (hg'_mem : MeasureTheory.MemLp g' 2 MeasureTheory.volume) (hg'_eq : ∀ (φ : SchwartzMap (EuclideanSpace (Fin n)) ), (FourierTransform.fourier (SobolevSpace.iteratedDistribDeriv n α u)) φ = (ξ : EuclideanSpace (Fin n)), (↑(SobolevSpace.sobolevWeight n (m - (∑ i : Fin n, α i)) ξ))⁻¹ * g' ξ * φ ξ) :
          ∀ᵐ (ξ : EuclideanSpace (Fin n)), g' ξ ((2 * Real.pi) ^ i : Fin n, α i) * g ξ

          Almost-everywhere pointwise bound: any L^2 witness g' for the iterated distributional derivative D^α u satisfies ‖g' ξ‖ ≤ (2π)^{|α|} ‖g ξ‖ for the witness g of u.

          Quantitative Sobolev bound: the L^2 witness of D^α u has norm at most (2π)^{|α|} times the norm of the witness of u.

          Continuity of the multi-index derivative D^α : H^m → H^{m - |α|} with an explicit positive operator-norm constant C = (2π)^{|α|}.

          Combined statement: D^α maps H^m to H^{m - |α|} and is bounded as a linear operator with explicit constant (2π)^{|α|}. This corresponds to Melrose Prop 10.2.