TwoCenterProjectionBudget.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A summable source for the actual two-center sharp estimate

def OAI.RegularPointCoordinates.twoCenterProjectionSource line 16
Source documentation
The square root is taken only after the two summable energies are combined. Its square, rather than its square root, is summed.
```
def twoCenterProjectionSource (eta : ℝ) (P Q : ℕ → ℝ) (i : ℕ) : ℝ :=
…
```

theorem OAI.RegularPointCoordinates.twoCenterProjectionSource_budget line 22

Source documentation

The actual defects at the two centers and each radial-fit envelope are dominated by one strictly positive source with a uniform square sum.

theorem twoCenterProjectionSource_budget {eta : ℝ} (heta : 0 < eta)
    {P Q : ℕ → ℝ} (hP : ∀ i, 0 ≤ P i) (hQ : ∀ i, 0 ≤ Q i)
    (hPs : Summable P) (hQs : Summable Q) :
    (∀ i, 0 < twoCenterProjectionSource eta P Q i ∧
      P i + Q i ≤ twoCenterProjectionSource eta P Q i ^ 2 ∧
      pinchingEnvelope (7 / 8) (3 / 4) eta Q i ≤ twoCenterProjectionSource eta P Q i ^ 2) ∧
    Summable (fun i => twoCenterProjectionSource eta P Q i ^ 2) ∧
    (∑' i, twoCenterProjectionSource eta P Q i ^ 2) ≤
      64 * (2 * eta + (∑' i, P i) + ∑' i, Q i) := by
…

Mentions: OAI.RegularPointCoordinates.twoCenterProjectionSource, OAI.RegularPointCoordinates.pinchingEnvelope

theorem OAI.RegularPointCoordinates.actual_two_center_projection_budget line 54

Source documentation

Specialization to the original positive Poisson defects; no new source or summability premise is introduced for sharp projection.

theorem actual_two_center_projection_budget {μ : Measure X} [IsFiniteMeasureOnCompacts μ]
    {hQ : QuadraticCheegerEnergy μ} {n : ℕ} {κ root : ℝ} {p q : X}
    (S1 : DyadicDistanceSources μ hQ n κ p root)
    (S2 : DyadicDistanceSources μ hQ n κ q root) (hκ : 0 ≤ κ)
    {eta : ℝ} (heta : 0 < eta)
    (hP : Summable (normalizedPoissonDefect μ hQ S1))
    (hQsum : Summable (normalizedPoissonDefect μ hQ S2)) :
    let sigma := twoCenterProjectionSource eta
…

Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.normalizedPoissonDefect, OAI.RegularPointCoordinates.sigma, OAI.RegularPointCoordinates.twoCenterProjectionSource