OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/GappedSeparation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Quantitative gaps for one- and two-symbol filled radix cylinders.

  1. def OAI.ForcedComputation.Radix.Separated line 13
  2. theorem OAI.ForcedComputation.Radix.Separated.symm line 16
  3. theorem OAI.ForcedComputation.Radix.cylinder_separated line 21
  4. theorem OAI.ForcedComputation.Radix.cylinder_subset_unit line 33
  5. theorem OAI.ForcedComputation.Radix.nested_subset_cylinder line 39
  6. theorem OAI.ForcedComputation.Radix.nested_same_separated line 45
  7. theorem OAI.ForcedComputation.Radix.nested_different_separated line 57
  8. def OAI.ForcedComputation.Radix.rationalBase line 68
  9. def OAI.ForcedComputation.Radix.rationalDigit line 70
  10. theorem OAI.ForcedComputation.Radix.rationalBase_ge_one line 72
  11. theorem OAI.ForcedComputation.Radix.rationalDigit_bounds line 76
  12. theorem OAI.ForcedComputation.Radix.rationalDigit_gap line 83
  13. theorem OAI.ForcedComputation.Radix.twoSymbol_separated line 105

    Source documentation

    Distinct two-symbol words have a gap at least one inverse square base.

    theorem twoSymbol_separated {N : ℕ} (a b d e : Fin N) (hne : (a, d) ≠ (b, e)) :
    Separated (1 / (rationalBase N : ℝ) ^ 2)
      (push (rationalBase N) (rationalDigit a) ''
        cylinder (rationalBase N) (rationalDigit d))
      (push (rationalBase N) (rationalDigit b) ''
        cylinder (rationalBase N) (rationalDigit e)) := by
…

    Mentions: OAI.ForcedComputation.Radix.Separated, OAI.ForcedComputation.Radix.rationalBase, OAI.ForcedComputation.Radix.push, OAI.ForcedComputation.Radix.rationalDigit, OAI.ForcedComputation.Radix.cylinder