BergTent.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Explicit finite Berg towers from unused Cuntz generators

The angular profile is a triangular tent. Two unused orthogonal isometries supply its bottom partial isometry. This discharges the support and angular hypotheses of the finite smoothing construction. It does not identify the terminal corners belonging to two different Cuntz rows.

def OAI.WeakPureInfiniteness.bergTent line 19
Source documentation
A tent of height π / 2, centered at L, with endpoints 0 and 2L.
```
def bergTent (L x : ℝ) : ℝ := (Real.pi / (2 * L)) * max (L - |x - L|) 0
```
lemma OAI.WeakPureInfiniteness.bergTent_zero line 21
lemma OAI.WeakPureInfiniteness.bergTent_peak line 24
lemma OAI.WeakPureInfiniteness.bergTent_end line 28
lemma OAI.WeakPureInfiniteness.bergTent_sub_le line 32
lemma OAI.WeakPureInfiniteness.bergTent_nat_step line 47
def OAI.WeakPureInfiniteness.bergSpareCorner line 55
Source documentation
Two unused ranges give a square-zero partial isometry.
```
def bergSpareCorner (r₀ r₁ : E) : E := r₁ * star r₀
```
lemma OAI.WeakPureInfiniteness.bergSpareCorner_source line 57
lemma OAI.WeakPureInfiniteness.bergSpareCorner_target line 65
lemma OAI.WeakPureInfiniteness.bergSpareCorner_partial line 73
lemma OAI.WeakPureInfiniteness.bergSpareCorner_square_zero line 83
lemma OAI.WeakPureInfiniteness.bergSpareCorner_bottom_support line 94
lemma OAI.WeakPureInfiniteness.bergCuntzRow_norm_le_one line 127

lemma OAI.WeakPureInfiniteness.exists_connected_cuntz_berg_tent line 137

Source documentation

With an explicit tent profile, every angle and support hypothesis is supplied by the infinite Cuntz row itself. The transported corner is the Kth iterate of the two unused generator ranges.

lemma exists_connected_cuntz_berg_tent (s : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n K : ℕ) (hK : 0 < K) :
    ∃ (u : unitary E) (b : E), Joined (1 : unitary E) u ∧
      (u : E) * (star b * b) = b ∧
      b = bergCornerIterHom
        (finiteCuntzDiagonalHom (fun i : Fin n => s i)
          (fun i j => by simpa only [Fin.ext_iff] using hs i j)) K
        (bergSpareCorner (s n) (s (n + 1))) ∧
      ∀ i < n, ‖(u : E) * s i - s i * (u : E)‖ ≤ Real.pi / (K : ℝ) := by
…

Mentions: OAI.WeakPureInfiniteness.bergCornerIterHom, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom, OAI.WeakPureInfiniteness.bergSpareCorner