OAI/Geometry/EinsteinFour/ScalarPoissonKernelMultiplier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth compactly supported coefficients preserve every nonnegative integer Sobolev order. The proof uses the actual distributional product rule and the coordinate-derivative characterization.

  1. theorem OAI.PositiveEinsteinFour.Geometry.scalar_schwartz_coordinate_product line 18
  2. theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative_multiplier line 34

    Source documentation

    Leibniz's rule for the actual tempered-distribution coordinate derivative.

    theorem scalarCoordinateDerivative_multiplier (a : 𝓢(V, ℂ)) (u : 𝓢'(V, ℂ))
    (i : Fin 4) :
    scalarCoordinateDerivative i (smulLeftCLM ℂ a u) =
      smulLeftCLM ℂ (∂_{EuclideanSpace.basisFun (Fin 4) ℝ i} a : 𝓢(V, ℂ)) u +
        smulLeftCLM ℂ a (scalarCoordinateDerivative i u) := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative

  3. theorem OAI.PositiveEinsteinFour.Geometry.scalar_memSobolev_zero_multiplier line 48
  4. theorem OAI.PositiveEinsteinFour.Geometry.scalar_memSobolev_schwartz_multiplier line 58

    Source documentation

    Every Schwartz coefficient preserves each integer Sobolev space.

    theorem scalar_memSobolev_schwartz_multiplier (n : ℕ) (a : 𝓢(V, ℂ))
    (u : 𝓢'(V, ℂ)) (hu : MemSobolev (n : ℝ) 2 u) :
    MemSobolev (n : ℝ) 2 (smulLeftCLM ℂ a u) := by
…
  5. theorem OAI.PositiveEinsteinFour.Geometry.scalar_memSobolev_compact_multiplier line 81

    Source documentation

    The compactly supported smooth coefficient form used for local cutoffs.

    theorem scalar_memSobolev_compact_multiplier (n : ℕ) (a : V → ℂ)
    (ha : ContDiff ℝ (⊤ : ℕ∞) a) (hc : HasCompactSupport a)
    (u : 𝓢'(V, ℂ)) (hu : MemSobolev (n : ℝ) 2 u) :
    MemSobolev (n : ℝ) 2 (smulLeftCLM ℂ a u) :=
…