ScalarPoissonKernelFiniteEmbedding.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The finite regularity embedding needed before positivity is known: in four dimensions H⁴ has a C¹ representative. The proof constructs that representative by Fourier inversion and controls its first moment.

def OAI.PositiveEinsteinFour.Geometry.scalarC1Reciprocal line 18
theorem OAI.PositiveEinsteinFour.Geometry.scalarC1Reciprocal_temperate line 21
theorem OAI.PositiveEinsteinFour.Geometry.scalarC1Reciprocal_norm line 25
theorem OAI.PositiveEinsteinFour.Geometry.scalarC1Reciprocal_bound line 32
theorem OAI.PositiveEinsteinFour.Geometry.scalarC1Reciprocal_first_bound line 39
theorem OAI.PositiveEinsteinFour.Geometry.scalarC1Reciprocal_memLp line 47

theorem OAI.PositiveEinsteinFour.Geometry.scalar_H4_fourier_first_moment line 54

Source documentation

H⁴ supplies an L¹ Fourier representative with integrable first moment.

theorem scalar_H4_fourier_first_moment (u : 𝓢'(V, ℂ)) (hu : MemSobolev 4 2 u) :
    ∃ v : Lp ℂ 1 (volume : Measure V),
      𝓕 u = (v : 𝓢'(V, ℂ)) ∧ Integrable (fun x : V => ‖x‖ * ‖v x‖) := by
…

theorem OAI.PositiveEinsteinFour.Geometry.scalarC1_inverse_pairing line 93
theorem OAI.PositiveEinsteinFour.Geometry.scalar_H4_C1_representative line 110
Source documentation
The C¹ representative is obtained without assuming positivity or any higher regularity of a nonlinear source.
```
theorem scalar_H4_C1_representative (u : 𝓢'(V, ℂ)) (hu : MemSobolev 4 2 u) :
    ∃ f : V → ℂ, ContDiff ℝ 1 f ∧
      ∀ φ : 𝓢(V, ℂ), u φ = ∫ x : V, φ x * f x := by
…
```

theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_H4_C1_representative line 135

Source documentation

In particular the C¹ function agrees almost everywhere with an L² representative of the distribution.

theorem scalar_L2_H4_C1_representative (u : Lp ℂ 2 (volume : Measure V))
    (hu : MemSobolev 4 2 (u : 𝓢'(V, ℂ))) :
    ∃ f : V → ℂ, ContDiff ℝ 1 f ∧ (u : V → ℂ) =ᵐ[volume] f := by
…

theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_H4_C1_real_representative line 149