GridSummability.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Vanishing terminal-count bounds for finite transfer

In the Koebe manuscript's finite-transfer estimate eq:transfer-terminal-mean, the scaled expected terminal count is bounded by a finite-cardinality term and finitely many series of clipped oscillation products. Square-summability of the oscillations makes these products summable, and dominated convergence makes the bound tend to zero as the grid spacing tends to zero through positive values.

theorem OAI.CircleDomainRigidity.FiniteTransfer.min_mul_min_norm_le line 24

Source documentation

Clipping two nonnegative oscillations at a nonnegative grid spacing preserves the summable mixed-product majorant.

theorem min_mul_min_norm_le {ι : Type*} {a b : ι → ℝ} {h : ℝ}
    (ha : ∀ s, 0 ≤ a s) (hb : ∀ s, 0 ≤ b s) (hh : 0 ≤ h) (s : ι) :
    ‖min h (a s) * min h (b s)‖ ≤ a s * b s := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.summable_min_mul_min line 33

Source documentation

Each clipped-product series is summable at every nonnegative spacing.

theorem summable_min_mul_min {ι : Type*} {a b : ι → ℝ} {h : ℝ}
    (ha : ∀ s, 0 ≤ a s) (hb : ∀ s, 0 ≤ b s)
    (ha2 : Summable (fun s => a s ^ 2)) (hb2 : Summable (fun s => b s ^ 2))
    (hh : 0 ≤ h) : Summable (fun s => min h (a s) * min h (b s)) :=
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.tendsto_tsum_min_mul_min_zero line 42

Source documentation

Dominated convergence for the clipped oscillation products in the terminal-count estimate.

theorem tendsto_tsum_min_mul_min_zero {ι : Type*} {a b : ι → ℝ}
    (ha : ∀ s, 0 ≤ a s) (hb : ∀ s, 0 ≤ b s)
    (ha2 : Summable (fun s => a s ^ 2)) (hb2 : Summable (fun s => b s ^ 2)) :
    Tendsto (fun h : ℝ => ∑' s, min h (a s) * min h (b s))
      (𝓝[>] 0) (𝓝 0) := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.terminal_mean_bound_tendsto_zero line 69

Source documentation

The complete finite-family bound in eq:transfer-terminal-mean vanishes with the positive grid spacing. P can be the finite family of coordinate pairs i < j, and F the prescribed finite terminal set.

theorem terminal_mean_bound_tendsto_zero {κ τ ι : Type*}
    (F : Finset κ) (P : Finset τ) (a b : τ → ι → ℝ)
    (ha : ∀ p ∈ P, ∀ s, 0 ≤ a p s) (hb : ∀ p ∈ P, ∀ s, 0 ≤ b p s)
    (ha2 : ∀ p ∈ P, Summable (fun s => a p s ^ 2))
    (hb2 : ∀ p ∈ P, Summable (fun s => b p s ^ 2)) :
    Tendsto (fun h : ℝ => h ^ 2 * (F.card : ℝ) +
      ∑ p ∈ P, ∑' s, min h (a p s) * min h (b p s)) (𝓝[>] 0) (𝓝 0) := by
…