OAI/NumberTheory/JointDickman/Counting/BlockEndpointLoss.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The endpoint cost of averaging the actual graph over finite blocks

  1. theorem OAI.JointDickman.kernelLagCorrelation_zero line 11
  2. theorem OAI.JointDickman.graph_without_short_nonzero line 15
  3. def OAI.JointDickman.blockWeightedGraphEnergy line 32

    Source documentation

    The coefficient is precisely the fraction of origins retaining both endpoints.

    noncomputable def blockWeightedGraphEnergy (B L : ℕ) (τ C : ℝ)
    (T N H M : ℕ) (F : ℕ → ℂ) : ℝ :=
…
  4. theorem OAI.JointDickman.block_endpoint_loss_le line 37
  5. theorem OAI.JointDickman.arithmetic_block_endpoint_bound line 67