def
definition
diffractionCost
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Crystallography.BraggAngleFromPhiLadder on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
38theorem braggPeakRatio_gt_one : 1 < braggPeakRatio := one_lt_phi
39
40/-- J-cost on diffraction peak ratio. -/
41def diffractionCost (measured_angle predicted_angle : ℝ) : ℝ :=
42 Jcost (measured_angle / predicted_angle)
43
44theorem diffractionCost_at_prediction (a : ℝ) (h : a ≠ 0) :
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