haloRegime_count

formal source

  23  | truncation
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem haloRegime_count : Fintype.card HaloRegime = 5 := by decide
  27
  28noncomputable def densityRung (k : ℕ) : ℝ := 1 / phi ^ k
  29
  30theorem density_pos (k : ℕ) : 0 < densityRung k := by
  31  unfold densityRung
  32  exact div_pos one_pos (pow_pos phi_pos k)
  33
  34theorem density_strictDecr (k : ℕ) :
  35    densityRung (k + 1) < densityRung k := by
  36  unfold densityRung
  37  have hpos_k : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  38  have h_growth : phi ^ k < phi ^ (k + 1) := by
  39    rw [pow_succ]
  40    have h1 : 1 < phi := one_lt_phi
  41    nlinarith
  42  exact one_div_lt_one_div_of_lt hpos_k h_growth
  43
  44structure DarkMatterHaloCert where
  45  five_regimes : Fintype.card HaloRegime = 5
  46  density_always_pos : ∀ k, 0 < densityRung k
  47  density_strictly_decreasing : ∀ k, densityRung (k + 1) < densityRung k
  48
  49noncomputable def darkMatterHaloCert : DarkMatterHaloCert where
  50  five_regimes := haloRegime_count
  51  density_always_pos := density_pos
  52  density_strictly_decreasing := density_strictDecr
  53
  54end IndisputableMonolith.Physics.DarkMatterHaloProfileFromRS