OAI/NumberTheory/TotientAsymptotic/PPTFiniteLabels.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

One finite label type for the actual residual comparison partition.

  1. abbrev OAI.TotientAsymptotic.PPTResidualLabel line 12
  2. def OAI.TotientAsymptotic.pptResidualLabel line 15
  3. def OAI.TotientAsymptotic.pptLabelB line 18
  4. def OAI.TotientAsymptotic.pptLabelGrid line 19
  5. def OAI.TotientAsymptotic.pptLabelWindow line 20
  6. def OAI.TotientAsymptotic.pptLabelH line 21
  7. def OAI.TotientAsymptotic.pptLabelA line 22
  8. def OAI.TotientAsymptotic.pptLabelS line 23
  9. def OAI.TotientAsymptotic.pptLabelC line 24
  10. def OAI.TotientAsymptotic.pptLabelWeight line 26
  11. def OAI.TotientAsymptotic.pptResidualLabels line 29
  12. lemma OAI.TotientAsymptotic.ppt_residual_label_mem line 37
  13. lemma OAI.TotientAsymptotic.ppt_residual_labels_mass line 48
  14. theorem OAI.TotientAsymptotic.ppt_selected_labels_mass line 61

    Source documentation

    Any selected subfamily, including the image of the actual residual label map, obeys the same complete weighted entropy estimate.

    theorem ppt_selected_labels_mass {A : ℝ} (hA : 0 ≤ A) :
    ∃ M : ℝ, 0 < M ∧ ∀ᶠ z : ℝ in atTop,
      ∀ (H : ℕ) (δ : ℝ) (I : Finset PPTResidualLabel),
        (H : ℝ) ≤ A*Real.log (B z) → 0 < δ → 1/B z ≤ δ →
        I ⊆ pptResidualLabels (discardPrimeBound (B z)) H δ →
        (∑ l ∈ I, pptLabelWeight l) ≤ Real.exp (M*(Real.log (B z))^2) := by
…

    Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.PPTResidualLabel, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.pptResidualLabels, OAI.TotientAsymptotic.discardPrimeBound, OAI.TotientAsymptotic.pptLabelWeight

  15. def OAI.TotientAsymptotic.pptResidualCell line 76
  16. lemma OAI.TotientAsymptotic.ppt_residual_cells_cover line 81
  17. lemma OAI.TotientAsymptotic.ppt_residual_cells_count_le line 88