entrainmentConfidence_zero

formal source

  61/-- Confidence at φ-rung `k` (relative to baseline 1): `1 / φ^k`. -/
  62def entrainmentConfidence (k : ℕ) : ℝ := 1 / phi ^ k
  63
  64theorem entrainmentConfidence_zero : entrainmentConfidence 0 = 1 := by
  65  unfold entrainmentConfidence; simp
  66
  67theorem entrainmentConfidence_pos (k : ℕ) : 0 < entrainmentConfidence k :=
  68  div_pos one_pos (pow_pos phi_pos _)
  69
  70theorem entrainmentConfidence_le_one (k : ℕ) : entrainmentConfidence k ≤ 1 := by
  71  unfold entrainmentConfidence
  72  rw [div_le_one (pow_pos phi_pos _)]
  73  exact one_le_pow₀ (le_of_lt one_lt_phi)
  74
  75theorem entrainmentConfidence_strict_anti {k₁ k₂ : ℕ} (h : k₁ < k₂) :
  76    entrainmentConfidence k₂ < entrainmentConfidence k₁ := by
  77  unfold entrainmentConfidence
  78  exact one_div_lt_one_div_of_lt (pow_pos phi_pos _)
  79    (pow_lt_pow_right₀ one_lt_phi h)
  80
  81/-! ## §3. Master certificate -/
  82
  83structure CorticalNeuromodulationDeviceCert where
  84  carrier_band : (8.05 : ℝ) < carrier ∧ carrier < 8.10
  85  spacing_pos : 0 < pulseSpacing
  86  spacing_band : (0.123 : ℝ) < pulseSpacing ∧ pulseSpacing < 0.125
  87  confidence_zero : entrainmentConfidence 0 = 1
  88  confidence_pos : ∀ k, 0 < entrainmentConfidence k
  89  confidence_le_one : ∀ k, entrainmentConfidence k ≤ 1
  90  confidence_strict_anti : ∀ {k₁ k₂ : ℕ}, k₁ < k₂ →
  91    entrainmentConfidence k₂ < entrainmentConfidence k₁
  92
  93def corticalNeuromodulationDeviceCert : CorticalNeuromodulationDeviceCert where
  94  carrier_band := carrier_band