OAI/Geometry/EinsteinFour/ScalarPoissonKernelContinuousEmbedding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite H3 embedding needed for weak positivity. Fourier inversion provides a bounded continuous representative before any positivity or smooth nonlinear chain rule is available.

  1. def OAI.PositiveEinsteinFour.Geometry.h3InverseBounded line 18
  2. theorem OAI.PositiveEinsteinFour.Geometry.h3InverseBounded_apply line 21
  3. theorem OAI.PositiveEinsteinFour.Geometry.h3_inverse_pairing line 25
  4. theorem OAI.PositiveEinsteinFour.Geometry.scalar_H3_boundedContinuous_representative line 43

    Source documentation

    Three L2 Sobolev derivatives in dimension four produce a bounded continuous function representing the same tempered distribution.

    theorem scalar_H3_boundedContinuous_representative (u : ๐“ข'(V, โ„‚))
    (hu : MemSobolev 3 2 u) :
    โˆƒ f : V โ†’แต‡ โ„‚, โˆ€ ฯ† : ๐“ข(V, โ„‚), u ฯ† = โˆซ x : V, ฯ† x * f x := by
โ€ฆ
  5. theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_H3_boundedContinuous_representative line 56

    Source documentation

    The bounded continuous representative agrees almost everywhere with any L2 realization of the original distribution.

    theorem scalar_L2_H3_boundedContinuous_representative
    (u : Lp โ„‚ 2 (volume : Measure V)) (hu : MemSobolev 3 2 (u : ๐“ข'(V, โ„‚))) :
    โˆƒ f : V โ†’แต‡ โ„‚, (u : V โ†’ โ„‚) =แต[volume] f := by
โ€ฆ
  6. theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_H3_continuous_representative line 70
  7. theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_H3_continuous_real_representative line 76