OAI/NumberTheory/TotientAsymptotic/CubeBoundary.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Unit boxes meeting the boundary lie in explicit prefix-slack shells.

  1. lemma OAI.TotientAsymptotic.unitGridCell_coordinate_distance line 13
  2. lemma OAI.TotientAsymptotic.prefixLinear_cube_error line 21
  3. lemma OAI.TotientAsymptotic.prefixBudget_cube_error line 69
  4. theorem OAI.TotientAsymptotic.prefixRegion_cube_boundary line 85

    Source documentation

    If a unit box meets a prefix region but is not contained in it, its interior points are in one of the displayed shells.

    theorem prefixRegion_cube_boundary {N : ℕ} (B C₀ : ℝ) (C : Fin N → ℝ)
    {u v : Fin N → ℝ} (_hu : u ∈ prefixRegion N B C₀ C)
    (hv : v ∉ prefixRegion N B C₀ C) (hdist : ∀ j, |u j-v j| ≤ 1) :
    B-C₀-(∑ j, a (j.val+1)*u j) ≤ (N : ℝ)^2 ∨
      ∃ i, prefixLinear N u i-C i ≤ ((N-i.val : ℕ) : ℝ)^2 := by
…

    Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.prefixRegion, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.prefixLinear