OuterApproximation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.RuledApproximation.inter_reciprocal_cthickening line 13
Source documentation
Closed outer neighborhoods recover a closed set even when its frontier has positive measure.
```
lemma inter_reciprocal_cthickening {E : Type*} [MetricSpace E] (K : Set E)
    (hK : IsClosed K) :
    (⋂ n : ℕ, cthickening (1 / ((n : ℝ) + 1)) K) = K := by
…
```

theorem OAI.RuledApproximation.exists_nice_outer_integral line 30

Source documentation

Small open outer neighborhoods, not regularity of the label boundary, justify the weighted lattice count for arbitrary compact label sets.

theorem exists_nice_outer_integral {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasureSpace E] [BorelSpace E]
    [IsFiniteMeasureOnCompacts (volume : Measure E)] [SFinite (volume : Measure E)]
    {K U : Set E} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U)
    {F : E → ℝ} (hF : Continuous F) (hFpos : ∀ x, 0 ≤ F x)
    {eps : ℝ} (heps : 0 < eps) :
    ∃ S : Set E, IsOpen S ∧ Bornology.IsBounded S ∧ K ⊆ S ∧ S ⊆ U ∧
      volume (frontier S) = 0 ∧ (∫ x in S, F x) < (∫ x in K, F x) + eps := by
…

def OAI.RuledApproximation.coordinateGrid line 70
Source documentation
The square lattice in the displayed (possibly nonorthonormal) parameter coordinates.
```
def coordinateGrid (n : ℕ) : Set (Fin 2 → ℝ) :=
…
```
lemma OAI.RuledApproximation.finite_inter_coordinateGrid line 73

theorem OAI.RuledApproximation.finite_weighted_grid_outer line 83

Source documentation

A finite lattice retained around any compact label set has arbitrarily accurate weighted cost. The finite set is the intersection with a fixed regular outer neighborhood, so no assumption on the boundary or positive area of K occurs here.

theorem finite_weighted_grid_outer {K U : Set (Fin 2 → ℝ)}
    (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U)
    {F : (Fin 2 → ℝ) → ℝ} (hF : Continuous F) (hFpos : ∀ x, 0 ≤ F x)
    (R : ℝ) {eps : ℝ} (heps : 0 < eps) :
    ∀ᶠ n : ℕ in atTop, 0 < n ∧ ∃ S : Set (Fin 2 → ℝ), S.Finite ∧
      S ⊆ U ∩ coordinateGrid n ∧
      (∀ b ∈ coordinateGrid n, (∃ p ∈ K, dist b p ≤ R / n) → b ∈ S) ∧
      (∑' b : S, F b) / (n : ℝ) ^ 2 < (∫ p in K, F p) + eps := by
…

Mentions: OAI.RuledApproximation.coordinateGrid