FluxLimit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passing finite-hole flux estimates to the limit

The rigidity manuscript's finite-hole estimate bounds the flux with an error of sixteen times the remaining mixed-radius sum. Square-summability of the source and target radii makes this error tend to zero along arbitrary finite subsets of the index type, giving eq:limiting-flux.

theorem OAI.CircleDomainRigidity.tendsto_mixed_radius_tail line 22
Source documentation
The mixed-radius tail vanishes as the retained finite family exhausts the holes. The hypotheses ensure that the total mixed-radius sum is the actual convergent series.
```
theorem tendsto_mixed_radius_tail {ι : Type*} {r s : ι → ℝ}
    (hr : Summable (fun j => r j ^ 2)) (hs : Summable (fun j => s j ^ 2)) :
    Tendsto (fun F : Finset ι => ∑' j : {j // j ∉ F}, r j * s j)
      atTop (𝓝 0) := by
…
```

theorem OAI.CircleDomainRigidity.limiting_flux_of_finite_hole_estimates line 42

Source documentation

A uniform finite-hole flux estimate gives the limiting flux bound. The coefficient 16 is the two-direction multiplicity bound appearing immediately before eq:limiting-flux in the rigidity manuscript.

theorem limiting_flux_of_finite_hole_estimates {ι : Type*} {r s : ι → ℝ}
    {A I : ℝ} (hr : Summable (fun j => r j ^ 2))
    (hs : Summable (fun j => s j ^ 2))
    (hfinite : ∀ F : Finset ι, 2 * A ≤ 2 * I +
      2 * Real.pi * (∑ j ∈ F, r j * s j) +
      16 * (∑' j : {j // j ∉ F}, r j * s j)) :
    2 * A ≤ 2 * I + 2 * Real.pi * (∑' j, r j * s j) := by
…