OAI/NumberTheory/Ostmann/Arithmetic/InternalLineProbability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact rank and feasibility tests for repeated internal-prime occurrences

Section 8, equation arith-line-probabilities: the simultaneous linear tests have probability zero in rank two, and exactly 1/(p-1) or 1/p in the respective feasible rank-one cases. A distinguished nonzero occurrence is sufficient; no independence of the repeated tests is assumed.

  1. def OAI.Ostmann.lineRankOne line 18
  2. def OAI.Ostmann.externalLineFeasible line 21
  3. def OAI.Ostmann.unitLineFeasible line 24
  4. theorem OAI.Ostmann.lineSystem_iff line 27
  5. theorem OAI.Ostmann.unit_lineSystem_iff line 44
  6. theorem OAI.Ostmann.external_lineSystem_probability line 58
  7. theorem OAI.Ostmann.unit_lineSystem_probability line 80