`ratio_factor_unique`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.LogicAsFunctionalEquation.PositiveRatioForcing
domain: Foundation
line: 38 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.PositiveRatioForcing on GitHub at line 38.

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

  35    _ = C (x / y) 1 := by rw [hleft, hright]
  36
  37/-- The ratio factor is unique on positive ratios. -/
  38theorem ratio_factor_unique
  39    (C : ComparisonOperator) (F G : ℝ → ℝ)
  40    (hF : ∀ x y : ℝ, 0 < x → 0 < y → C x y = F (x / y))
  41    (hG : ∀ x y : ℝ, 0 < x → 0 < y → C x y = G (x / y)) :
  42    ∀ r : ℝ, 0 < r → F r = G r := by
  43  intro r hr
  44  have hF' := hF r 1 hr one_pos
  45  have hG' := hG r 1 hr one_pos
  46  simpa using hF'.symm.trans hG'
  47
  48/-- The canonical factor obtained from scale invariance is exactly
  49`derivedCost`. -/
  50theorem ratioCost_eq_derivedCost (C : ComparisonOperator) :
  51    ratioCost C = derivedCost C := by
  52  rfl
  53
  54/-- Searchable alias: positive ratios are forced by scale-free comparison. -/
  55theorem positive_ratio_is_forced_by_scale_free_comparison
  56    (C : ComparisonOperator)
  57    (hScale : ScaleInvariant C) :
  58    ∃ F : ℝ → ℝ, ∀ x y : ℝ, 0 < x → 0 < y → C x y = F (x / y) :=
  59  scale_free_comparison_factors_through_ratio C hScale
  60
  61end LogicAsFunctionalEquation
  62end Foundation
  63end IndisputableMonolith

papers checked against this theorem

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