BlockOperators.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform block operators on Hilbert sums

The averaging operators used in the transfer act separately on finite fibers. A uniform norm bound, rather than finiteness of the set of fibers, makes their direct sum a bounded operator. The resulting operator admits the uniform approximation needed for the fiber projection.

theorem OAI.CoarseAssembly.blockLinear_norm_le line 28
theorem OAI.CoarseAssembly.blockOperator_apply line 41
theorem OAI.CoarseAssembly.blockOperator_norm_le line 45
theorem OAI.CoarseAssembly.blockIsometry_apply line 49

theorem OAI.CoarseAssembly.blockOperator_dist_le line 54

Source documentation

Uniform fiberwise norm error bounds the operator error on the whole Hilbert sum. This is the norm estimate for the amplified Kazhdan projection.

theorem blockOperator_dist_le (A B : ∀ i, E i →L[ℂ] F i)
    (C D ε : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D) (hε : 0 ≤ ε)
    (hA : ∀ i, ‖A i‖ ≤ C) (hB : ∀ i, ‖B i‖ ≤ D)
    (hAB : ∀ i, ‖A i - B i‖ ≤ ε) :
    ‖blockOperator A C hC hA - blockOperator B D hD hB‖ ≤ ε := by
…

Mentions: OAI.CoarseAssembly.blockOperator

theorem OAI.CoarseAssembly.power_mul_fixed line 66
theorem OAI.CoarseAssembly.projection_error_power line 74
Source documentation
Removing a fixed projection converts averaging powers into powers on its complementary subspace. This identity needs no spectral theorem.
```
theorem projection_error_power {R : Type*} [Ring R] (M P : R)
    (hPP : P * P = P) (hMP : M * P = P) (hPM : P * M = P) (n : ℕ) :
    (M - P) ^ (n + 1) = M ^ (n + 1) - P := by
…
```
theorem OAI.CoarseAssembly.averaging_power_norm_le line 83

theorem OAI.CoarseAssembly.averaging_blocks_tendsto line 93

Source documentation

The uniform spectral-gap consequence needed by the transfer. The published input is the strict contraction bound on M i - P i; norm convergence of the direct sum is proved here.

theorem averaging_blocks_tendsto (M P : ∀ i, E i →L[ℂ] E i)
    (c : ℝ) (hc : 0 ≤ c) (hc1 : c < 1)
    (hM : ∀ i, ‖M i‖ ≤ 1) (hP : ∀ i, ‖P i‖ ≤ 1)
    (hPP : ∀ i, P i * P i = P i) (hMP : ∀ i, M i * P i = P i)
    (hPM : ∀ i, P i * M i = P i) (hgap : ∀ i, ‖M i - P i‖ ≤ c) :
    Tendsto
      (fun n : ℕ => blockOperator (fun i => M i ^ (n + 1)) 1 (by norm_num)
        (averaging_power_norm_le M hM n))
      atTop (nhds (blockOperator P 1 (by norm_num) hP)) := by
…

Mentions: OAI.CoarseAssembly.blockOperator, OAI.CoarseAssembly.averaging_power_norm_le