OAI/Geometry/EinsteinFour/ScalarPoissonKernelAdjointEstimate.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Quantitative bounded extension of the actual transposed operator after Bessel regularization. Coefficient bounds imply the dense-range condition used for distributional uniqueness.

  1. def OAI.PositiveEinsteinFour.Geometry.scalarSchwartzMultiplyL2 line 22

    Source documentation

    Multiplication by a Schwartz coefficient, as a physical L2 operator.

    def scalarSchwartzMultiplyL2 (a : S) : L2 →L[ℂ] L2 :=
…
  2. theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_product_distribution line 25
  3. theorem OAI.PositiveEinsteinFour.Geometry.scalarL2_eq_schwartz line 34
  4. theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzMultiplyL2_distribution line 41
  5. theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzMultiplyL2_toLp line 49
  6. theorem OAI.PositiveEinsteinFour.Geometry.scalar_derivative_schwartz_distribution line 54
  7. theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL2_schwartz_distribution line 58
  8. theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL2_toLp line 64
  9. theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselSecondL2_schwartz_distribution line 69
  10. theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselSecondL2_toLp line 76
  11. theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzHelmholtz_distribution line 81
  12. theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzHelmholtz_bessel_toLp line 89
  13. def OAI.PositiveEinsteinFour.Geometry.scalarAdjointSecondPiece line 99
  14. def OAI.PositiveEinsteinFour.Geometry.scalarAdjointFirstPiece line 105
  15. def OAI.PositiveEinsteinFour.Geometry.scalarAdjointSecondL2Term line 108
  16. def OAI.PositiveEinsteinFour.Geometry.scalarAdjointFirstL2Term line 114
  17. def OAI.PositiveEinsteinFour.Geometry.scalarAdjointL2Perturbation line 118
  18. theorem OAI.PositiveEinsteinFour.Geometry.scalarAdjointSecondL2Term_toLp line 122
  19. theorem OAI.PositiveEinsteinFour.Geometry.scalarAdjointFirstL2Term_toLp line 130
  20. theorem OAI.PositiveEinsteinFour.Geometry.scalarAdjointL2Perturbation_toLp line 139

    Source documentation

    The bounded L2 perturbation is exactly the regularized formal transpose.

    theorem scalarAdjointL2Perturbation_toLp (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S) (φ : S) :
    (scalarSchwartzTranspose a b (scalarSchwartzBesselInverse φ)).toLp 2 volume =
      φ.toLp 2 volume + scalarAdjointL2Perturbation a b (φ.toLp 2 volume) := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.scalarSchwartzTranspose, OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselInverse, OAI.PositiveEinsteinFour.Geometry.scalarAdjointL2Perturbation

  21. theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzMultiplyL2_bound line 168
  22. theorem OAI.PositiveEinsteinFour.Geometry.scalarAdjointSecondL2Term_bound line 173
  23. theorem OAI.PositiveEinsteinFour.Geometry.scalarAdjointFirstL2Term_bound line 202
  24. theorem OAI.PositiveEinsteinFour.Geometry.scalarAdjointL2Perturbation_bound line 218

    Source documentation

    Uniform control of coefficient derivatives makes the formal transpose an explicit small perturbation.

    theorem scalarAdjointL2Perturbation_bound (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S)
    (δ : ℝ) (hδ : 0 ≤ δ)
    (ha : ∀ i j, ‖(a i j).toLp ∞ (volume : Measure V)‖ ≤ δ)
    (ha1 : ∀ i j k, ‖(D k (a i j)).toLp ∞ (volume : Measure V)‖ ≤ δ)
    (ha2 : ∀ i j k l, ‖(D k (D l (a i j))).toLp ∞ (volume : Measure V)‖ ≤ δ)
    (hb : ∀ i, ‖(b i).toLp ∞ (volume : Measure V)‖ ≤ δ)
    (hb1 : ∀ i k, ‖(D k (b i)).toLp ∞ (volume : Measure V)‖ ≤ δ) :
    ∀ f : L2, ‖scalarAdjointL2Perturbation a b f‖ ≤
      ((16 * (2 * Real.pi) ^ 2 + 36 * (2 * Real.pi) + 20) * δ) * ‖f‖ := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.scalarAdjointL2Perturbation

  25. theorem OAI.PositiveEinsteinFour.Geometry.scalarAdjointL2Perturbation_opNorm line 247
  26. theorem OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator_kernel_small line 261

    Source documentation

    An actual L2 distributional kernel element vanishes under explicit smallness of the coefficient jets through order two.

    theorem scalarPerturbedOperator_kernel_small (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S)
    (δ : ℝ) (hδ : 0 ≤ δ)
    (ha : ∀ i j, ‖(a i j).toLp ∞ (volume : Measure V)‖ ≤ δ)
    (ha1 : ∀ i j k, ‖(D k (a i j)).toLp ∞ (volume : Measure V)‖ ≤ δ)
    (ha2 : ∀ i j k l, ‖(D k (D l (a i j))).toLp ∞ (volume : Measure V)‖ ≤ δ)
    (hb : ∀ i, ‖(b i).toLp ∞ (volume : Measure V)‖ ≤ δ)
    (hb1 : ∀ i k, ‖(D k (b i)).toLp ∞ (volume : Measure V)‖ ≤ δ)
    (hsmall : (16 * (2 * Real.pi) ^ 2 + 36 * (2 * Real.pi) + 20) * δ < 1)
    (u : L2) (hu : scalarPerturbedOperator a b (u : 𝓢'(V, ℂ)) = 0) : u = 0 := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator