PoissonCommonRegion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Common-region data for actual two-center replacements

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.value_bound line 19
Source documentation
The actual replacement has a global value bound in its natural squared length units; it follows from the positive datum and the proved height.
```
theorem DyadicDistanceReplacements.value_bound {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ) :
    ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (T.replacement i) x| ≤
      max 8 B * (distanceSourceRadius r0 i) ^ 2 := by
…
```
Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.distanceSourceRadius

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.laplacian_on_ball line 44

Source documentation

Equal Laplacians remain equal on a smaller ball around another center.

theorem DyadicDistanceReplacements.laplacian_on_ball {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
    (z : X) {R : ℝ} (hroom : R + dist z p ≤ distanceSourceRadius r0 i) :
    IsConstantLaplacianOn μ hQ (ball z R) (T.replacement i)
      ((n : ℝ) + κ * (4 * distanceSourceRadius r0 i) ^ 2) :=
…

Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.IsConstantLaplacianOn

theorem OAI.RegularPointCoordinates.common_replacement_difference_harmonic line 54

Source documentation

The harmonic difference in the two-center argument is constructed from the actual same-scale replacements and their common constant source.

theorem common_replacement_difference_harmonic
    {n : ℕ} {κ r0 B₁ J₁ C₁ B₂ J₂ C₂ : ℝ} {p₁ p₂ : X}
    {S₁ : DyadicDistanceSources μ hQ n κ p₁ r0}
    {S₂ : DyadicDistanceSources μ hQ n κ p₂ r0}
    (T₁ : DyadicDistanceReplacements μ hQ S₁ B₁ J₁ C₁)
    (T₂ : DyadicDistanceReplacements μ hQ S₂ B₂ J₂ C₂)
    (i : ℕ) (z : X) {R : ℝ}
    (hroom₁ : R + dist z p₁ ≤ distanceSourceRadius r0 i)
    (hroom₂ : R + dist z p₂ ≤ distanceSourceRadius r0 i) :
    IsSobolevHarmonicOn μ hQ (ball z R) (T₂.replacement i - T₁.replacement i) :=
…