SeparatedGeometry.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded geometry of the separated union

Uniform component ball bounds pass to the union. All cross-component pairs in a fixed distance range lie in a finite prefix, which also supplies the finite exceptional set in the transfer argument.

def OAI.CoarseAssembly.componentPrefix line 20
theorem OAI.CoarseAssembly.mem_componentPrefix line 24
theorem OAI.CoarseAssembly.finite_cross_pairs line 30

theorem OAI.CoarseAssembly.separated_uniform_finite_balls line 42

Source documentation

The bounded-geometry hypothesis needed by the Roe transfer is preserved by this separated union.

theorem separated_uniform_finite_balls (o : ∀ i, V i)
    (hcomp : ∀ R : ℝ, 0 ≤ R → ∃ N : ℕ, ∀ i (x : V i), ∃ b : Finset (V i),
      (∀ y, y ∈ b ↔ dist x y ≤ R) ∧ b.card ≤ N) :
    @UniformFiniteBalls (Sigma V) (separatedMetric o).toPseudoMetricSpace := by
…

Mentions: OAI.CoarseAssembly.UniformFiniteBalls, OAI.CoarseAssembly.separatedMetric

theorem OAI.CoarseAssembly.separated_uniform_discrete line 80
Source documentation
Unit separation in each component gives unit separation in the union.
```
theorem separated_uniform_discrete (o : ∀ i, V i)
    (hcomp : ∀ i (x y : V i), x ≠ y → 1 ≤ dist x y)
    (x y : Sigma V) (hxy : x ≠ y) : 1 ≤ separatedDist o x y := by
…
```
Mentions: OAI.CoarseAssembly.separatedDist