`phi_harmonic_forced`

definition

show as: view math explainer →

module: IndisputableMonolith.Cost.FrequencyLadder
domain: Cost
line: 92 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.FrequencyLadder on GitHub at line 92.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  89  ratio_unique : ∀ r > 0, IsSelfSimilarRatio r → r = phi
  90
  91/-- The φ-harmonic is forced for any positive frequency. -/
  92noncomputable def phi_harmonic_forced {f : ℝ} (hf : 0 < f) : PhiHarmonicForced f where
  93  harmonic := f * phi
  94  harmonic_eq := rfl
  95  ratio_is_phi := by rw [mul_div_cancel_left₀ _ (ne_of_gt hf)]
  96  ratio_self_similar := by
  97    rw [mul_div_cancel_left₀ _ (ne_of_gt hf)]
  98    exact phi_is_self_similar
  99  ratio_unique := fun r hr_pos hr_ss => phi_unique_self_similar hr_pos hr_ss
 100
 101end FrequencyLadder
 102end Cost
 103end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.