GraphFiberOperators.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Controlled transport along the base graph

The three depth cases give actual contractions on the finite scalar Hilbert spaces. Their nonzero coefficients are supported on edges of the constructed fibered graph, not on an assumed transport relation.

theorem OAI.CoarseAssembly.isometry_norm_le_one line 19

theorem OAI.CoarseAssembly.exists_depth_operator line 28

Source documentation

Transport between adjacent depths, with its exact reduced support.

theorem exists_depth_operator (t : ℤ_[2]ˣ) (k l : ℕ) (a : ℤ)
    (hkl : |(k : ℤ) - (l : ℤ)| ≤ 1) :
    ∃ O : lp (fun _ : Quotient k => ℂ) 2 →L[ℂ] lp (fun _ : Quotient l => ℂ) 2,
      ‖O‖ ≤ 1 ∧ O (fiberConstant (Quotient k) (1 : ℂ)) =
        fiberConstant (Quotient l) 1 ∧
      ∀ q z, O (lp.single 2 q 1) z ≠ 0 →
        ∀ m (hm : m ≤ k) (hl : m ≤ l),
          quotientMap hl z = quotientMap hm q * holonomy t m ^ a := by
…

Mentions: OAI.CoarseAssembly.fiberConstant

theorem OAI.CoarseAssembly.exists_base_edge_operator line 71

Source documentation

Each base edge has a contraction preserving constants, whose matrix coefficients are supported on actual edges upstairs.

theorem exists_base_edge_operator (S : Finset ArithmeticGroup) (t : ℤ_[2]ˣ)
    {j : ℕ} {u v : Disc j} (huv : (discGraph j).Adj u v) :
    ∃ O : lp (fun _ : Quotient (discDepth j u) => ℂ) 2 →L[ℂ]
        lp (fun _ : Quotient (discDepth j v) => ℂ) 2,
      ‖O‖ ≤ 1 ∧ O (fiberConstant (Quotient (discDepth j u)) (1 : ℂ)) =
        fiberConstant (Quotient (discDepth j v)) 1 ∧
      ∀ q z, ¬(fiberedGraph S t j).Adj ⟨u, q⟩ ⟨v, z⟩ →
        O (lp.single 2 q 1) z = 0 := by
…

Mentions: OAI.CoarseAssembly.Disc, OAI.CoarseAssembly.discGraph, OAI.CoarseAssembly.discDepth, OAI.CoarseAssembly.fiberConstant, OAI.CoarseAssembly.fiberedGraph