PathFiberOperators.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Composing the concrete fiber transports

Every base walk gives a contraction preserving normalized constants. A nonzero matrix coefficient comes with an actual lifted walk of the same length, which is the propagation estimate needed by the transfer criterion.

theorem OAI.CoarseAssembly.scalarFiber_expansion line 24
theorem OAI.CoarseAssembly.scalarFiber_apply_sum line 33
theorem OAI.CoarseAssembly.scalarFiber_comp_nonzero line 42

theorem OAI.CoarseAssembly.exists_base_walk_operator line 61

Source documentation

The concrete edge maps compose without any loss in the propagation bound. This includes the length-zero identity case.

theorem exists_base_walk_operator (S : Finset ArithmeticGroup) (t : ℤ_[2]ˣ)
    {j : ℕ} {u v : Disc j} (p : (discGraph j).Walk 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, O (lp.single 2 q 1) z ≠ 0 →
        ∃ w : (fiberedGraph S t j).Walk ⟨u, q⟩ ⟨v, z⟩, w.length = p.length := by
…

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

theorem OAI.CoarseAssembly.exists_bounded_base_operator line 97

Source documentation

A shortest base walk provides the desired controlled contraction for any prescribed finite graph-distance bound.

theorem exists_bounded_base_operator (S : Finset ArithmeticGroup) (t : ℤ_[2]ˣ)
    {j : ℕ} {u v : Disc j} {R : ℕ} (hR : (discGraph j).edist u v ≤ R) :
    ∃ 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, R < (fiberedGraph S t j).edist ⟨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