ScalarPoissonKernelPerturbation.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

A quantitative small-coefficient inverse on L2, with its actual second-order distributional equation and H2 regularity.

def OAI.PositiveEinsteinFour.Geometry.scalarL2Multiply line 21
Source documentation
Physical multiplication by an essentially bounded coefficient.
```
def scalarL2Multiply (a : Linf) : L2 →L[ℂ] L2 :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2Multiply_norm line 30
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2Multiply_distribution line 33
def OAI.PositiveEinsteinFour.Geometry.scalarL2Perturbation line 40
Source documentation
The lower-order perturbation after composing on the right with Bessel(-2).
```
def scalarL2Perturbation (a : Fin 4 → Fin 4 → Linf) (b : Fin 4 → Linf) : L2 →L[ℂ] L2 :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2Perturbation_apply line 45

theorem OAI.PositiveEinsteinFour.Geometry.scalarL2Perturbation_bound line 53

Source documentation

Sixteen second-order terms and four first-order terms, with exact Fourier factors.

theorem scalarL2Perturbation_bound (a : Fin 4 → Fin 4 → Linf) (b : Fin 4 → Linf)
    (δ : ℝ) (ha : ∀ i j, ‖a i j‖ ≤ δ) (hb : ∀ i, ‖b i‖ ≤ δ) (f : L2) :
    ‖scalarL2Perturbation a b f‖ ≤
      (16 * (2 * Real.pi) ^ 2 * δ + 4 * (2 * Real.pi) * δ) * ‖f‖ := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarL2Perturbation

theorem OAI.PositiveEinsteinFour.Geometry.scalarL2Perturbation_opNorm line 85
def OAI.PositiveEinsteinFour.Geometry.scalarPerturbationEquiv line 94
Source documentation
Neumann inversion of Id + K in the actual Banach space.
```
def scalarPerturbationEquiv (K : L2 →L[ℂ] L2) (hK : ‖K‖ < 1) : L2 ≃L[ℂ] L2 :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarPerturbationEquiv_apply line 97

theorem OAI.PositiveEinsteinFour.Geometry.scalarL2Perturbation_existsUnique line 103

Source documentation

An L2 right-hand side has a unique transformed unknown for small coefficients.

theorem scalarL2Perturbation_existsUnique (a : Fin 4 → Fin 4 → Linf) (b : Fin 4 → Linf)
    (δ : ℝ) (ha : ∀ i j, ‖a i j‖ ≤ δ) (hb : ∀ i, ‖b i‖ ≤ δ)
    (hsmall : 16 * (2 * Real.pi) ^ 2 * δ + 4 * (2 * Real.pi) * δ < 1) (f : L2) :
    ∃! v : L2, v + scalarL2Perturbation a b v = f := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarL2Perturbation

theorem OAI.PositiveEinsteinFour.Geometry.scalarCoefficient_memLp line 118
theorem OAI.PositiveEinsteinFour.Geometry.scalarCoefficient_Linf_bound line 122
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2Perturbation_distribution line 129

theorem OAI.PositiveEinsteinFour.Geometry.scalar_perturbedHelmholtz_solution line 158

Source documentation

Small smooth bounded coefficients give a genuine H2 solution of the perturbed distributional equation. No regularity of a prospective solution is used in this construction.

theorem scalar_perturbedHelmholtz_solution
    (a : Fin 4 → Fin 4 → V → ℂ) (b : Fin 4 → V → ℂ)
    (ha : ∀ i j, (a i j).HasTemperateGrowth) (hb : ∀ i, (b i).HasTemperateGrowth)
    (δ : ℝ) (haBound : ∀ i j x, ‖a i j x‖ ≤ δ) (hbBound : ∀ i x, ‖b i x‖ ≤ δ)
    (hsmall : 16 * (2 * Real.pi) ^ 2 * δ + 4 * (2 * Real.pi) * δ < 1) (f : L2) :
    ∃ u : L2, MemSobolev 2 2 (u : 𝓢'(V, ℂ)) ∧
      normalizedScalarHelmholtz (u : 𝓢'(V, ℂ)) +
        (∑ i : Fin 4, ∑ j : Fin 4, smulLeftCLM ℂ (a i j)
          (scalarCoordinateDerivative i (scalarCoordinateDerivative j (u : 𝓢'(V, ℂ))))) +
        (∑ i : Fin 4, smulLeftCLM ℂ (b i)
          (scalarCoordinateDerivative i (u : 𝓢'(V, ℂ)))) = (f : 𝓢'(V, ℂ)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.normalizedScalarHelmholtz, OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative