mul_infi_of_nonneg

Stream: Is there code for X?

[Eric Wieser]

Does this exist for Inf or some more general setting?

lemma real.mul_infi_of_nonneg {ι} (r : ℝ) (hr : 0 ≤ r) (f : ι → ℝ) :
  r * (⨅ i, f i) = ⨅ i, r * f i :=
begin
  casesI is_empty_or_nonempty ι,
  { simp [real.cinfi_empty] },
  obtain rfl | hrp := hr.eq_or_lt,
  { simp only [zero_mul, real.cinfi_const_zero] },
  change order_iso.mul_left₀ _ hrp _ = ⨅ i, order_iso.mul_left₀ _ hrp _,
  by_cases hb : bdd_below (range f),
  { exact order_iso.map_cinfi _ hb },
  rw [infi, infi, real.Inf_of_not_bdd_below hb, real.Inf_of_not_bdd_below (mt (λ H, _) hb),
    order_iso.mul_left₀_apply, mul_zero],
  have := H.smul_of_nonneg (inv_nonneg.mpr hr),
  simpa [←image_smul, ←range_comp, function.comp, smul_eq_mul, inv_mul_cancel_left₀ hrp.ne'],
end

(cc @Pierre-Alexandre Bazin, this would help in your seminorm PR)

Should the name mention infi or cinfi?

[Eric Wieser]

Aha!

lemma real.mul_infi_of_nonneg {ι} (r : ℝ) (hr : 0 ≤ r) (f : ι → ℝ) :
  r * (⨅ i, f i) = ⨅ i, r * f i :=
(real.Inf_smul_of_nonneg hr _).symm.trans $ congr_arg Inf $ (range_comp _ _).symm

docs#real.Inf_smul_of_nonneg is very close

[Eric Wieser]

#12105