Commit 2024-04-03 10:19 1cca755b

View on Github →

chore: swap argument order in cfc and cfcₙ (#11468) This changes the argument order for cfc and cfcₙ from cfc (a : A) (f : R → R) to cfc (f : R → R) (a : A). This has a few advantages:

  1. It's closer to the usual reading (cfc f a vs. f(a) on paper).
  2. argument order looks better for cfc_comp (cfc (g ∘ f) a = cfc g (cfc f a) instead of cfc a (g ∘ f) = cfc (cfc f a) g).
  3. it will be much easier to speak of operator convexity and monotonicity if we can just write cfc f.

Estimated changes

modified theorem cfcUnits_pow
modified theorem cfcUnits_zpow
modified theorem cfc_add
modified theorem cfc_apply
modified theorem cfc_apply_of_not_and
modified theorem cfc_apply_of_not_predicate
modified theorem cfc_comp'
modified theorem cfc_comp
modified theorem cfc_comp_const_mul
modified theorem cfc_comp_inv
modified theorem cfc_comp_neg
modified theorem cfc_comp_polynomial
modified theorem cfc_comp_pow
modified theorem cfc_comp_smul
modified theorem cfc_comp_star
modified theorem cfc_comp_zpow
modified theorem cfc_congr
modified theorem cfc_const
modified theorem cfc_const_mul
modified theorem cfc_const_mul_id
modified theorem cfc_const_one
modified theorem cfc_const_zero
modified theorem cfc_eq_cfc_iff_eqOn
modified theorem cfc_eval_C
modified theorem cfc_eval_X
modified theorem cfc_id'
modified theorem cfc_id
modified theorem cfc_inv
modified theorem cfc_map_div
modified theorem cfc_map_polynomial
modified theorem cfc_map_spectrum
modified theorem cfc_mul
modified theorem cfc_neg
modified theorem cfc_neg_id
modified theorem cfc_one
modified theorem cfc_polynomial
modified theorem cfc_pow
modified theorem cfc_pow_id
modified theorem cfc_predicate
modified theorem cfc_star
modified theorem cfc_star_id
modified theorem cfc_sub
modified theorem cfc_zero
modified theorem eqOn_of_cfc_eq_cfc
modified theorem isUnit_cfc_iff
modified theorem cfc_map_quasispectrum
modified theorem cfcₙ_add
modified theorem cfcₙ_apply
modified theorem cfcₙ_apply_of_not_and_and
modified theorem cfcₙ_comp'
modified theorem cfcₙ_comp
modified theorem cfcₙ_comp_const_mul
modified theorem cfcₙ_comp_neg
modified theorem cfcₙ_comp_star
modified theorem cfcₙ_congr
modified theorem cfcₙ_const_mul
modified theorem cfcₙ_const_mul_id
modified theorem cfcₙ_const_zero
modified theorem cfcₙ_eq_cfcₙ_iff_eqOn
modified theorem cfcₙ_id'
modified theorem cfcₙ_id
modified theorem cfcₙ_mul
modified theorem cfcₙ_neg
modified theorem cfcₙ_neg_id
modified theorem cfcₙ_predicate
modified theorem cfcₙ_star
modified theorem cfcₙ_star_id
modified theorem cfcₙ_sub
modified theorem cfcₙ_zero
modified theorem eqOn_of_cfcₙ_eq_cfcₙ