FiniteLevels.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite scalar levels

The distinct values of a nonnegative function on a finite set, together with zero, give a finite subdivision. Its positive gaps reconstruct every value and every absolute difference by strict superlevel indicators. These are finite sums, including when the only level is zero.

structure OAI.ThompsonNonamenability.FiniteLevelChain line 27
Source documentation
The actual ordered levels of p on K, with zero included.
```
structure FiniteLevelChain (K : Finset G) (p : G → ℝ) where
…
```
def OAI.ThompsonNonamenability.FiniteLevelChain.ofNonneg line 37
Source documentation
Construct the level chain by sorting the actual finite image.
```
noncomputable def ofNonneg (K : Finset G) (p : G → ℝ)
    (hp : ∀ x ∈ K, 0 ≤ p x) : FiniteLevelChain K p := by
…
```
Mentions: OAI.ThompsonNonamenability.FiniteLevelChain
theorem OAI.ThompsonNonamenability.FiniteLevelChain.exists_chain line 65
def OAI.ThompsonNonamenability.FiniteLevelChain.gap line 72
Source documentation
Width of the interval immediately above the indexed level.
```
def gap (i : Fin c.n) : ℝ := c.value i.succ - c.value i.castSucc
```
theorem OAI.ThompsonNonamenability.FiniteLevelChain.gap_pos line 74
theorem OAI.ThompsonNonamenability.FiniteLevelChain.value_nonneg line 78
theorem OAI.ThompsonNonamenability.FiniteLevelChain.value_mem line 82

theorem OAI.ThompsonNonamenability.FiniteLevelChain.telescope line 87

Source documentation

Telescoping below any selected value of a strictly increasing finite list.

private theorem telescope : ∀ (n : ℕ) (f : Fin (n + 1) → ℝ),
    StrictMono f → ∀ k : Fin (n + 1),
      f k - f 0 = ∑ i : Fin n,
        (f i.succ - f i.castSucc) * (if f i.castSucc < f k then 1 else 0) := by
…

theorem OAI.ThompsonNonamenability.FiniteLevelChain.reconstruct line 120

Source documentation

The finite layer decomposition of each value in the actual level set.

theorem reconstruct (a : ℝ) (ha : a ∈ insert 0 (K.image p)) :
    a = ∑ i : Fin c.n, c.gap i *
      (if c.value i.castSucc < a then (1 : ℝ) else 0) := by
…

theorem OAI.ThompsonNonamenability.FiniteLevelChain.abs_sub_eq_sum_of_le line 131

theorem OAI.ThompsonNonamenability.FiniteLevelChain.abs_sub_eq_sum line 162

Source documentation

The finite coarea identity for a scalar absolute difference.

theorem abs_sub_eq_sum (a b : ℝ)
    (ha : a ∈ insert 0 (K.image p)) (hb : b ∈ insert 0 (K.image p)) :
    |a - b| = ∑ i : Fin c.n, c.gap i *
      |(if c.value i.castSucc < a then (1 : ℝ) else 0) -
        (if c.value i.castSucc < b then (1 : ℝ) else 0)| := by
…