OAI/InformationTheory/QuantumCircuit/Localization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QAC.UniformLocalization line 15

    Source documentation

    The uniform estimate, with the eventual quantifier outside all circuit data.

    def UniformLocalization (d : ℕ) (s t : ℝ) : Prop :=
…
  2. lemma OAI.QAC.uniform_zero line 19
  3. lemma OAI.QAC.uniform_large line 32
  4. lemma OAI.QAC.uniform_low_propagation line 40
  5. lemma OAI.QAC.uniform_small_support line 56
  6. lemma OAI.QAC.uniform_backward line 88
  7. theorem OAI.QAC.uniform_localization line 126

    Source documentation

    Uniform localization, proved by depth and finite scale induction.

    theorem uniform_localization : ∀ d s t, 0 ≤ s → s < t → UniformLocalization d s t := by
…

    Mentions: OAI.QAC.UniformLocalization

  8. theorem OAI.QAC.localization line 137

    Source documentation

    Uniform product-projection localization in the Euclidean operator norm.

    theorem localization : LocalizationStatement := by
…

    Mentions: OAI.QAC.LocalizationStatement