FiniteCutoffPartition.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The quantitative cutoff partition used by Lipschitz replacement

def OAI.PolycyclicRecognition.cutoffMass line 16
Source documentation
Unnormalized radius-two distance cutoffs in the sum norm.
```
def cutoffMass (v : I → X) (x : X) : PiLp 1 (fun _ : I => ℝ) :=
…
```
def OAI.PolycyclicRecognition.cutoffPartition line 19
theorem OAI.PolycyclicRecognition.cutoff_difference_le line 22
theorem OAI.PolycyclicRecognition.norm_cutoffMass_sub_le line 30
Source documentation
Before normalization, at most one distance error is charged per participating center. The application restricts to the finite local support.
```
theorem norm_cutoffMass_sub_le (v : I → X) (x y : X) :
    ‖cutoffMass v x - cutoffMass v y‖ ≤ (Fintype.card I : ℝ) * dist x y := by
…
```
Mentions: OAI.PolycyclicRecognition.cutoffMass
theorem OAI.PolycyclicRecognition.one_le_norm_cutoffMass line 39
Source documentation
The unit-ball cover gives the uniform lower bound on the denominator.
```
theorem one_le_norm_cutoffMass (v : I → X) (x : X)
    (hcover : ∃ i, dist x (v i) ≤ 1) : 1 ≤ ‖cutoffMass v x‖ := by
…
```
Mentions: OAI.PolycyclicRecognition.cutoffMass
theorem OAI.PolycyclicRecognition.norm_cutoffPartition_sub_le line 51
Source documentation
Normalization costs a factor two, uniformly over points whose unit balls contain one of the participating centers.
```
theorem norm_cutoffPartition_sub_le (v : I → X) (x y : X)
    (hx : ∃ i, dist x (v i) ≤ 1) (hy : ∃ i, dist y (v i) ≤ 1) :
    ‖cutoffPartition v x - cutoffPartition v y‖ ≤
      2 * (Fintype.card I : ℝ) * dist x y := by
…
```
Mentions: OAI.PolycyclicRecognition.cutoffPartition
theorem OAI.PolycyclicRecognition.cutoffPartition_probability line 61
Source documentation
These are genuine barycentric coordinates, with nonnegative entries and total mass exactly one.
```
theorem cutoffPartition_probability (v : I → X) (x : X)
    (hcover : ∃ i, dist x (v i) ≤ 1) :
    (∀ i, 0 ≤ cutoffPartition v x i) ∧ (∑ i, cutoffPartition v x i) = 1 := by
…
```
Mentions: OAI.PolycyclicRecognition.cutoffPartition