OAI/NumberTheory/TwoPoint/Bounds/PerfectIntervalFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Choose numerical intervals for the constructed perfect blocks, preserving all budgets.

  1. def OAI.TwoPointCorrelations.intervalPositions line 9
  2. theorem OAI.TwoPointCorrelations.choose_interval_family line 12
  3. theorem OAI.TwoPointCorrelations.perfectChunkLength_eq_sum line 32
  4. theorem OAI.TwoPointCorrelations.shortPerfectColumnChunks_interval_family line 48

    Source documentation

    The actual short-block partition admits numerical interval parameters. Their total length is at most the original length; every selected position retains its original perfect flag. Empty terminal blocks cost zero.

    theorem shortPerfectColumnChunks_interval_family (N s : ℕ) (perfect : ℕ → Bool) :
    ∃ intervals : List (ℕ × ℕ),
      intervals.map intervalPositions =
        ((shortPerfectColumnChunks s ((List.range N).map (fun i => (i, perfect i)))).filterMap
          (Sum.elim some (fun _ => none))) ∧
      intervals.length = perfectChunkCount
        (shortPerfectColumnChunks s ((List.range N).map (fun i => (i, perfect i)))) ∧
      (intervals.map Prod.snd).sum ≤ N ∧
      ∀ b ∈ intervals, b.1 + b.2 ≤ N ∧ ∀ i ∈ intervalPositions b, perfect i = true := by
…

    Mentions: OAI.TwoPointCorrelations.intervalPositions, OAI.TwoPointCorrelations.shortPerfectColumnChunks, OAI.TwoPointCorrelations.perfectChunkCount