PinchingEnvelope.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Construction of the summable pinching envelope

The positive floor and the two geometric convolutions in pi:definition-E are constructed here from a nonnegative summable Poisson-defect sequence. No summability of square roots is assumed.

def OAI.RegularPointCoordinates.forwardDefect line 21
def OAI.RegularPointCoordinates.symmetricDefect line 24
def OAI.RegularPointCoordinates.pinchingEnvelope line 27
theorem OAI.RegularPointCoordinates.forwardDefect_nonneg line 30
theorem OAI.RegularPointCoordinates.le_forwardDefect line 36
theorem OAI.RegularPointCoordinates.forwardDefect_budget line 45
theorem OAI.RegularPointCoordinates.geometric_distance_sum_le line 68
Source documentation
A geometric kernel on the nonnegative integers has a uniform row sum bound, also at rows next to the endpoint.
```
theorem geometric_distance_sum_le {ρ : ℝ} (hρ : 0 ≤ ρ) (hρ1 : ρ < 1)
    (i : ℕ) (s : Finset ℕ) :
    (∑ j ∈ s, ρ ^ Nat.dist i j) ≤ 2 * (1 - ρ)⁻¹ := by
…
```
theorem OAI.RegularPointCoordinates.geometric_distance_summable line 111
theorem OAI.RegularPointCoordinates.geometric_distance_tsum_le line 115
theorem OAI.RegularPointCoordinates.symmetricDefect_budget line 119
theorem OAI.RegularPointCoordinates.symmetricDefect_nonneg line 148
theorem OAI.RegularPointCoordinates.symmetricDefect_row_summable line 153
theorem OAI.RegularPointCoordinates.term_le_symmetricDefect line 160
theorem OAI.RegularPointCoordinates.le_symmetricDefect line 166

theorem OAI.RegularPointCoordinates.pinchingEnvelope_spec line 175

Source documentation

The two convolutions produce exactly the summability and positive floor needed when choosing patch centers. The total is uniform whenever the original Poisson-defect budget is uniform.

theorem pinchingEnvelope_spec {ρ σ η : ℝ}
    (hρ : 0 < ρ) (hρ1 : ρ < 1) (hσ : 0 ≤ σ) (hσ1 : σ < 1) (hη : 0 < η)
    {P : ℕ → ℝ} (hP : ∀ i, 0 ≤ P i) (hPs : Summable P) :
    Summable (pinchingEnvelope ρ σ η P) ∧
      (∑' i, pinchingEnvelope ρ σ η P i) ≤
        (2 * (1 - ρ)⁻¹) * (1 - σ)⁻¹ * (η + ∑' i, P i) ∧
      ∀ i, P i ≤ pinchingEnvelope ρ σ η P i ∧
        η * ρ ^ i ≤ pinchingEnvelope ρ σ η P i ∧
        0 < pinchingEnvelope ρ σ η P i := by
…

Mentions: OAI.RegularPointCoordinates.pinchingEnvelope