IndisputableMonolith.VoxelWalks

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace VoxelWalks
   5
   6noncomputable section
   7open Real
   8
   9def phi : ℝ := (1 + Real.sqrt 5) / 2
  10
  11def A2 (P γ : ℝ) : ℝ := P * (phi) ^ (-(2 * γ))
  12
  13def sigmaCore (n : ℕ) (a2 : ℝ) : ℝ :=
  14  let num := (3 : ℝ) ^ n * (a2) ^ n
  15  let den := 2 * (1 - 2 * a2) ^ (2 * n - 1)
  16  num / den
  17
  18@[simp] lemma sigmaCore_n0 (a2 : ℝ) : sigmaCore 0 a2 = 1 / 2 := by
  19  unfold sigmaCore
  20  simp
  21
  22def fEye (n : ℕ) : ℝ := (1 / 2 : ℝ) ^ n
  23def fHalfVoxel (n : ℕ) : ℝ := ((23 : ℝ) / 24) ^ n
  24def fFace (n : ℕ) : ℝ := ((11 : ℝ) / 12) ^ n
  25
  26def sigmaN (n : ℕ) (a2 : ℝ)
  27  (useEye : Bool := true) (useHalfVoxel : Bool := true) (useFace : Bool := false) : ℝ :=
  28  let core := sigmaCore n a2
  29  let eye := if useEye then fEye n else 1
  30  let hv  := if useHalfVoxel then fHalfVoxel n else 1
  31  let face := if useFace then fFace n else 1
  32  core * eye * hv * face
  33
  34def A2_QED : ℝ := A2 ((1 : ℝ) / 18) ((2 : ℝ) / 3)
  35def A2_QCD : ℝ := A2 ((2 : ℝ) / 9) ((2 : ℝ) / 3)
  36
  37def convergent (a2 : ℝ) : Prop := 1 - 2 * a2 > 0
  38
  39lemma sigmaN_QED_expand (n : ℕ) :
  40  sigmaN n A2_QED true true false =
  41    sigmaCore n A2_QED * ((1 / 2 : ℝ) ^ n) * (((23 : ℝ) / 24) ^ n) := by
  42  unfold sigmaN fEye fHalfVoxel fFace
  43  simp
  44
  45lemma sigmaN_QCD_expand (n : ℕ) :
  46  sigmaN n A2_QCD true true false =
  47    sigmaCore n A2_QCD * ((1 / 2 : ℝ) ^ n) * (((23 : ℝ) / 24) ^ n) := by
  48  unfold sigmaN fEye fHalfVoxel fFace
  49  simp
  50
  51end
  52
  53end VoxelWalks
  54end IndisputableMonolith
  55