OAI/Geometry/EinsteinFour/ScalarPoissonKernelSobolev.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Arbitrarily high scalar Sobolev regularity produces a smooth function. The representative is constructed by inverse Fourier integration, rather than assumed as an elliptic regularity input.

  1. def OAI.PositiveEinsteinFour.Geometry.sobolevReciprocal line 20
  2. theorem OAI.PositiveEinsteinFour.Geometry.sobolevReciprocal_temperate line 24
  3. theorem OAI.PositiveEinsteinFour.Geometry.sobolevReciprocal_norm line 30
  4. theorem OAI.PositiveEinsteinFour.Geometry.sobolevReciprocal_memLp line 36
  5. theorem OAI.PositiveEinsteinFour.Geometry.scalar_fourier_weight_memL1 line 45
  6. theorem OAI.PositiveEinsteinFour.Geometry.scalar_sobolev_fourier_moments line 70

    Source documentation

    Every polynomial moment of the Fourier representative is integrable.

    theorem scalar_sobolev_fourier_moments (u : ๐“ข'(E, โ„‚))
    (hu : โˆ€ n : โ„•, MemSobolev (n : โ„) 2 u)
    (v : Lp โ„‚ 1 (volume : Measure E)) (hv : ๐“• u = (v : ๐“ข'(E, โ„‚)))
    (n : โ„•) : Integrable (fun x : E => โ€–xโ€– ^ n * โ€–v xโ€–) := by
โ€ฆ
  7. theorem OAI.PositiveEinsteinFour.Geometry.inverse_fourier_pairing line 114
  8. theorem OAI.PositiveEinsteinFour.Geometry.scalar_sobolev_smooth_representative line 133

    Source documentation

    Arbitrarily high L2 Sobolev regularity gives an actual smooth representative, with equality against every Schwartz test function.

    theorem scalar_sobolev_smooth_representative (u : ๐“ข'(E, โ„‚))
    (hu : โˆ€ n : โ„•, MemSobolev (n : โ„) 2 u) :
    โˆƒ f : E โ†’ โ„‚, ContDiff โ„ (โŠค : โ„•โˆž) f โˆง
      โˆ€ ฯ† : ๐“ข(E, โ„‚), u ฯ† = โˆซ x : E, ฯ† x * f x := by
โ€ฆ
  9. theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_sobolev_smooth_representative line 154

    Source documentation

    For an L2 function, the constructed smooth function agrees almost everywhere with the original representative.

    theorem scalar_L2_sobolev_smooth_representative (u : Lp โ„‚ 2 (volume : Measure E))
    (hu : โˆ€ n : โ„•, MemSobolev (n : โ„) 2 (u : ๐“ข'(E, โ„‚))) :
    โˆƒ f : E โ†’ โ„‚, ContDiff โ„ (โŠค : โ„•โˆž) f โˆง (u : E โ†’ โ„‚) =แต[volume] f := by
โ€ฆ
  10. theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_sobolev_smooth_real_representative line 170

    Source documentation

    The real part inherits a smooth representative without requiring a complex-valued formulation from a geometric caller.

    theorem scalar_L2_sobolev_smooth_real_representative
    (u : Lp โ„‚ 2 (volume : Measure E))
    (hu : โˆ€ n : โ„•, MemSobolev (n : โ„) 2 (u : ๐“ข'(E, โ„‚))) :
    โˆƒ f : E โ†’ โ„, ContDiff โ„ (โŠค : โ„•โˆž) f โˆง
      (fun x : E => (u x).re) =แต[volume] f := by
โ€ฆ