OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticLineIntegration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual line integrals as bounded functions of the cleared polynomial tests

  1. def OAI.Ostmann.internalLineScalar line 12
  2. theorem OAI.Ostmann.internalLineScalar_nonneg line 15
  3. theorem OAI.Ostmann.internalLineScalar_le_one line 20
  4. def OAI.Ostmann.internalLineFlagWeight line 28
  5. theorem OAI.Ostmann.internalLineFlagWeight_nonneg line 32
  6. theorem OAI.Ostmann.internalLineFlagWeight_le_one line 39
  7. def OAI.Ostmann.internalLineProbability line 47

    Source documentation

    The normalized count before the giant variables are integrated out.

    noncomputable def internalLineProbability {J : Type*} {p : ℕ} [Fact p.Prime]
    (external : Bool) (a b : J → ZMod p) : ℝ :=
…
  8. theorem OAI.Ostmann.internalLineProbability_nonneg line 56
  9. theorem OAI.Ostmann.external_lineSystem_integral_eq_flags line 61
  10. theorem OAI.Ostmann.unit_lineSystem_integral_eq_flags line 75
  11. theorem OAI.Ostmann.internalLineProbability_eq_flags line 91