OAI/Geometry/EinsteinFour/ScalarPoissonKernelPotential.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PositiveEinsteinFour.Geometry.scalarPotential_multipliers_commute line 22
2. theorem OAI.PositiveEinsteinFour.Geometry.scalar_nested_cutoff_gain_of_potential line 40

   Source documentation

   The potential times u has the needed order from the outer cutoff; it is not required to be smooth before the bootstrap.

   theorem scalar_nested_cutoff_gain_of_potential (c ψ χ : S)
       (hnest : ScalarCutoffNested ψ χ) (n : ℕ) (u : T)
       (hu : MemSobolev ((n + 1 : ℕ) : ℝ) 2 (M χ u))
       (hf : MemSobolev (n : ℝ) 2
         (M ψ (scalarPerturbedOperator a b u - u - M c u))) :
       MemSobolev ((n + 2 : ℕ) : ℝ) 2 (M ψ u) := by
   …

   Mentions: OAI.PositiveEinsteinFour.Geometry.ScalarCutoffNested, OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator

3. theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_cutoff_chain_gain_of_potential line 62
4. theorem OAI.PositiveEinsteinFour.Geometry.scalar_ball_local_sobolev_of_potential line 89

   Source documentation

   Local H1 and a smooth potential-source remainder give every Sobolev order on each smaller compactly supported localization.

   theorem scalar_ball_local_sobolev_of_potential (c : S) (u : T)
       (hH1 : ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
         tsupport (ψ : V → ℂ) ⊆ ball 0 1 → MemSobolev 1 2 (M ψ u))
       (hforce : ∀ n : ℕ, ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
         tsupport (ψ : V → ℂ) ⊆ ball 0 1 →
           MemSobolev (n : ℝ) 2 (M ψ (scalarPerturbedOperator a b u - u - M c u)))
       (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (φ : S)
       (hφc : HasCompactSupport (φ : V → ℂ))
       (hφ : tsupport (φ : V → ℂ) ⊆ closedBall 0 r) :
       ∀ n : ℕ, MemSobolev (n : ℝ) 2 (M φ u) := by
   …

   Mentions: OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator

5. def OAI.PositiveEinsteinFour.Geometry.scalarPotentialInnerBump line 109
6. def OAI.PositiveEinsteinFour.Geometry.scalarPotentialInnerCutoff line 115
7. theorem OAI.PositiveEinsteinFour.Geometry.scalarPotentialInnerCutoff_apply line 120
8. theorem OAI.PositiveEinsteinFour.Geometry.scalarPotentialInnerCutoff_tsupport line 123
9. theorem OAI.PositiveEinsteinFour.Geometry.scalarPotentialInnerCutoff_one line 133
10. theorem OAI.PositiveEinsteinFour.Geometry.scalar_small_elliptic_potential_local_representative line 143

    Source documentation

    No smallness or prior regularity of the potential term times u is assumed. The original L2 solution has a smooth local representative.

    theorem scalar_small_elliptic_potential_local_representative (c : S) (u : L2)
        (hH1 : ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
          tsupport (ψ : V → ℂ) ⊆ ball 0 1 → MemSobolev 1 2 (M ψ (u : T)))
        (hforce : ∀ n : ℕ, ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
          tsupport (ψ : V → ℂ) ⊆ ball 0 1 → MemSobolev (n : ℝ) 2
            (M ψ (scalarPerturbedOperator a b (u : T) - (u : T) - M c (u : T)))) :
        ∃ f : V → ℂ, ContDiff ℝ (⊤ : ℕ∞) f ∧
          (u : V → ℂ) =ᵐ[volume.restrict (ball 0 (1 / 4))] f := by
    …

    Mentions: OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator

11. theorem OAI.PositiveEinsteinFour.Geometry.scalar_small_elliptic_potential_local_real_representative line 162