OAI/NumberTheory/CubicMoment/Angular/AngularSquarefreeIdentity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The exact square-divisor Möbius identity on primary elements. This is the arithmetic inversion used by the low-height angular model.

  1. def OAI.CubicFirstMoment.primarySquarePrimeFactors line 12
  2. lemma OAI.CubicFirstMoment.primary_subset_square_dvd line 15
  3. lemma OAI.CubicFirstMoment.primarySquarePrimeFactors_empty_iff line 29
  4. lemma OAI.CubicFirstMoment.primary_square_divisors_image line 47
  5. lemma OAI.CubicFirstMoment.sum_powerset_sign line 77
  6. theorem OAI.CubicFirstMoment.primary_square_moebius_inversion line 88

    Source documentation

    Every square divisor is included, so the actual truncated coefficient equals the squarefree indicator; no error term occurs.

    theorem primary_square_moebius_inversion (C : Finset Eisenstein)
    (hC : ∀ c ∈ C, primary c ∧ Squarefree c) {a : Eisenstein} (ha : primary a)
    (hcomplete : ∀ c, primary c → Squarefree c → c^2 ∣ a → c ∈ C) :
    (∑ c ∈ C, if c^2 ∣ a then (idealMoebius c:ℝ) else 0) =
      (idealMoebius a:ℝ)^2 := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealMoebius

  7. lemma OAI.CubicFirstMoment.squarefreeDivisorTruncation_complete line 111
  8. theorem OAI.CubicFirstMoment.primary_square_moebius_truncation line 120