OAI/Analysis/ModularTheory/WeightFaithful.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual modular cutoff vectors separate squares in the core. This proves faithfulness of the proposed weight, without presupposing its traciality or semifiniteness.

  1. def OAI.WeakPureInfiniteness.modularWeightCutoffInverse line 18
  2. lemma OAI.WeakPureInfiniteness.modularWeightCutoffInverse_cancel line 28
  3. lemma OAI.WeakPureInfiniteness.modularWeightCutoffInverse_apply line 36
  4. lemma OAI.WeakPureInfiniteness.scalarLp_eq_zero_of_weightCutoffs line 58
  5. theorem OAI.WeakPureInfiniteness.modularCoreCutoffs_faithful_square line 102

    Source documentation

    Faithfulness for squares follows from the concrete cutoff functionals.

    theorem modularCoreCutoffs_faithful_square
    (T : Lp H 2 (volume : Measure ℝ) →L[ℂ] Lp H 2 (volume : Measure ℝ))
    (hT : T ∈ modularCrossedProduct (volume : Measure ℝ) S)
    (hz : ∀ n, modularCoreCutoffFunctional S n (star T * T) = 0) : T = 0 := by
…

    Mentions: OAI.WeakPureInfiniteness.modularCrossedProduct, OAI.WeakPureInfiniteness.modularCoreCutoffFunctional