sensitivity

formal source

  45def h_0 : ℝ := 1
  46
  47/-- Sensitivity at frequency `f > 0`: `h_min(f) = h_0 · carrier / f`. -/
  48def sensitivity (f : ℝ) : ℝ :=
  49  if f ≤ 0 then 0 else h_0 * carrier / f
  50
  51theorem sensitivity_at_carrier : sensitivity carrier = h_0 := by
  52  unfold sensitivity h_0
  53  rw [if_neg (not_le.mpr carrier_pos)]
  54  have h_ne : carrier ≠ 0 := ne_of_gt carrier_pos
  55  field_simp
  56
  57theorem sensitivity_pos {f : ℝ} (h : 0 < f) : 0 < sensitivity f := by
  58  unfold sensitivity h_0
  59  rw [if_neg (not_le.mpr h)]
  60  apply div_pos
  61  · simp; exact carrier_pos
  62  · exact h
  63
  64/-- Sensitivity is strictly anti-monotonic in `f` (above carrier:
  65sensitivity decreases; below: increases). -/
  66theorem sensitivity_strict_anti {f₁ f₂ : ℝ} (h₁ : 0 < f₁) (h₂ : f₁ < f₂) :
  67    sensitivity f₂ < sensitivity f₁ := by
  68  unfold sensitivity h_0
  69  have h₂_pos : 0 < f₂ := lt_trans h₁ h₂
  70  rw [if_neg (not_le.mpr h₁), if_neg (not_le.mpr h₂_pos)]
  71  -- 1·carrier/f₂ < 1·carrier/f₁ ↔ carrier/f₂ < carrier/f₁ ↔ f₁ < f₂
  72  simp only [one_mul]
  73  exact div_lt_div_of_pos_left carrier_pos h₁ h₂
  74
  75/-! ## §2. Master certificate -/
  76
  77structure PhantomCoupledGWAntennaSensitivityCert where
  78  carrier_band : (8.05 : ℝ) < carrier ∧ carrier < 8.10