diffractionCost_nonneg

formal source

  45    diffractionCost a a = 0 := by
  46  unfold diffractionCost; rw [div_self h]; exact Jcost_unit0
  47
  48theorem diffractionCost_nonneg (m p : ℝ) (hm : 0 < m) (hp : 0 < p) :
  49    0 ≤ diffractionCost m p := by
  50  unfold diffractionCost; exact Jcost_nonneg (div_pos hm hp)
  51
  52structure BraggAngleCert where
  53  ratio_gt_one : 1 < braggPeakRatio
  54  cost_at_prediction : ∀ a : ℝ, a ≠ 0 → diffractionCost a a = 0
  55  cost_nonneg : ∀ m p : ℝ, 0 < m → 0 < p → 0 ≤ diffractionCost m p
  56
  57noncomputable def cert : BraggAngleCert where
  58  ratio_gt_one := braggPeakRatio_gt_one
  59  cost_at_prediction := diffractionCost_at_prediction
  60  cost_nonneg := diffractionCost_nonneg
  61
  62theorem cert_inhabited : Nonempty BraggAngleCert := ⟨cert⟩
  63
  64end
  65end BraggAngleFromPhiLadder
  66end Crystallography
  67end IndisputableMonolith