OAI/Geometry/EinsteinFour/ScalarPoissonKernelLocalRepresentative.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Local smooth representatives of the original L2 function. The cutoff is one on a smaller ball, so Fourier regularization returns the given solution there, not just a solution of a related equation.

  1. def OAI.PositiveEinsteinFour.Geometry.scalarCutoffL2 line 23
  2. theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffL2_distribution line 26
  3. theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffL2_ae line 32
  4. theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_cutoff_smooth_on line 41

    Source documentation

    All Sobolev orders for an inner localization give a smooth function agreeing with the original L2 function wherever the cutoff is one.

    theorem scalar_L2_cutoff_smooth_on (u : L2) (φ : S) (B : Set V)
    (hB : MeasurableSet B) (hone : ∀ x ∈ B, φ x = 1)
    (hreg : ∀ n : ℕ, MemSobolev (n : ℝ) 2 (M φ (u : T))) :
    ∃ f : V → ℂ, ContDiff ℝ (⊤ : ℕ∞) f ∧
      (u : V → ℂ) =ᵐ[volume.restrict B] f := by
…
  5. def OAI.PositiveEinsteinFour.Geometry.scalarInnerBump line 61
  6. def OAI.PositiveEinsteinFour.Geometry.scalarInnerCutoff line 67
  7. theorem OAI.PositiveEinsteinFour.Geometry.scalarInnerCutoff_apply line 72
  8. theorem OAI.PositiveEinsteinFour.Geometry.scalarInnerCutoff_tsupport line 75
  9. theorem OAI.PositiveEinsteinFour.Geometry.scalarInnerCutoff_one line 84
  10. theorem OAI.PositiveEinsteinFour.Geometry.scalar_small_elliptic_local_representative line 92

    Source documentation

    A small smooth elliptic perturbation has a smooth representative on a fixed smaller ball. Hypotheses are local H1 and a regular remainder P u-u.

    theorem scalar_small_elliptic_local_representative
    (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S) (δ : ℝ) (hδ : 0 ≤ δ)
    (ha : ∀ i j x, ‖a i j x‖ ≤ δ)
    (ha1 : ∀ i j k x, ‖D k (a i j) x‖ ≤ δ)
    (ha2 : ∀ i j k l x, ‖D k (D l (a i j)) x‖ ≤ δ)
    (hb : ∀ i x, ‖b i x‖ ≤ δ)
    (hb1 : ∀ i k x, ‖D k (b i) x‖ ≤ δ)
    (hsmall : (16 * (2 * Real.pi) ^ 2 + 36 * (2 * Real.pi) + 20) * δ < 1)
    (u : L2)
    (hH1 : ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
      tsupport (ψ : V → ℂ) ⊆ ball 0 1 → MemSobolev 1 2 (M ψ (u : T)))
    (hforce : ∀ n : ℕ, ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
…
  11. theorem OAI.PositiveEinsteinFour.Geometry.scalar_small_elliptic_local_real_representative line 121

    Source documentation

    Real-valued geometric callers take the real part of the constructed representative, preserving smoothness and equality almost everywhere.

    theorem scalar_small_elliptic_local_real_representative
    (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S) (δ : ℝ) (hδ : 0 ≤ δ)
    (ha : ∀ i j x, ‖a i j x‖ ≤ δ)
    (ha1 : ∀ i j k x, ‖D k (a i j) x‖ ≤ δ)
    (ha2 : ∀ i j k l x, ‖D k (D l (a i j)) x‖ ≤ δ)
    (hb : ∀ i x, ‖b i x‖ ≤ δ)
    (hb1 : ∀ i k x, ‖D k (b i) x‖ ≤ δ)
    (hsmall : (16 * (2 * Real.pi) ^ 2 + 36 * (2 * Real.pi) + 20) * δ < 1)
    (u : L2)
    (hH1 : ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
      tsupport (ψ : V → ℂ) ⊆ ball 0 1 → MemSobolev 1 2 (M ψ (u : T)))
    (hforce : ∀ n : ℕ, ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
…