OAI/Analysis/KadisonKastler/TwoRatioParameters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The two fixed product-state parameters

The manuscript uses exp (-1) and exp (-sqrt 2). Their logarithms generate an incommensurable pair of modular frequencies. No parameter depends on an algebra, representation, or requested perturbation bound.

  1. def OAI.KadisonKastler.fixedProductLambda line 20
  2. def OAI.KadisonKastler.fixedProductMu line 22
  3. theorem OAI.KadisonKastler.fixedProductLambda_pos line 24
  4. theorem OAI.KadisonKastler.fixedProductMu_pos line 26
  5. theorem OAI.KadisonKastler.fixedProductLambda_lt_one line 28
  6. theorem OAI.KadisonKastler.fixedProductMu_lt_one line 31
  7. theorem OAI.KadisonKastler.fixedProduct_log_ratio_irrational line 35
  8. theorem OAI.KadisonKastler.fixedProduct_frequency_ratio_irrational line 42

    Source documentation

    The normalization by 2π comes from Mathlib's Fourier convention; it leaves the irrational frequency ratio unchanged.

    theorem fixedProduct_frequency_ratio_irrational :
    Irrational ((Real.log fixedProductLambda / (2 * Real.pi)) /
      (Real.log fixedProductMu / (2 * Real.pi))) := by
…

    Mentions: OAI.KadisonKastler.fixedProductLambda, OAI.KadisonKastler.fixedProductMu