Inf and Sup of smul of a set

Stream: Is there code for X?

[Yaël Dillies]

Where should these two lemmas go?
I wanted to put them in data.real.basic but map_cInf_of_continuous_at_of_monotone requires topology.algebra.ordered.basic and topological_space ℝ. For info, bdd_below_smul_iff_of_pos and bdd_above_smul_iff_of_pos are added in #9078 and will reside in algebra.bounds.

lemma Sup_smul {a : ℝ} (ha : 0 ≤ a) (s : set ℝ) :
  Sup (a • s) = a * Sup s :=
begin
  obtain rfl | hs := s.eq_empty_or_nonempty,
  { rw [set.smul_set_empty, real.Sup_empty, mul_zero] },
  by_cases bdd_above s,
  { rw [←set.image_smul, eq_comm],
    exact map_cSup_of_continuous_at_of_monotone (continuous_mul_left a).continuous_at
      (monotone_mul_left_of_nonneg ha) hs h
    },
  rw [Sup_of_not_bdd_above h, mul_zero],
  obtain rfl | ha' := ha.eq_or_lt,
  { rw zero_smul_set hs,
    exact cSup_singleton 0 },
  exact Sup_of_not_bdd_above (mt (bdd_above_smul_iff_of_pos ha').2),
end

lemma Inf_smul {a : ℝ} (ha : 0 ≤ a) (s : set ℝ) :
  Inf (a • s) = a * Inf s :=
begin
  obtain rfl | hs := s.eq_empty_or_nonempty,
  { rw [set.smul_set_empty, real.Inf_empty, mul_zero] },
  by_cases bdd_below s,
  { rw [←set.image_smul, eq_comm],
    exact map_cInf_of_continuous_at_of_monotone (continuous_mul_left a).continuous_at
      (monotone_mul_left_of_nonneg ha) hs h },
  rw [Inf_of_not_bdd_below h, mul_zero],
  obtain rfl | ha' := ha.eq_or_lt,
  { rw zero_smul_set hs,
    exact cInf_singleton 0 },
  refine real.Inf_of_not_bdd_below (λ H, h _),
  exact Inf_of_not_bdd_below (mt (bdd_below_smul_iff_of_pos ha').2),
end

[Eric Wieser]

Those should generalize to a smul on each side

[Eric Wieser]

(or at least, to the action by nnreal)

[Yaël Dillies]

Sure, yeah. But where? :thinking:

[Yury G. Kudryashov]

You can prove it using docs#order_iso.map_cSup instead of continuity.

[Yury G. Kudryashov]

If 0 < a, then multiplication by a is an order_iso.

[Eric Wieser]

docs#order_iso.mul_left'

[Yaël Dillies]

Ah so what we're missing is order-reversing isomorphisms?

[Eric Wieser]

You don't need that for the above, right?

[Yaël Dillies]

No but I do for the a ≤ 0 versions. I guess I won't care because I don't need them now.

[Eric Wieser]

I guess we could have mul_left'' (a < 0) : α ≃o order_dual α

[Yaël Dillies]

Yeah, but that's a bit hacky and follows suit of what I'm trying to avoid by defining antitone functions.

[Yury G. Kudryashov]

Advice: don't try to do 2 large refactors at once.

[Yury G. Kudryashov]

(I tried several times, failed)

[Yury G. Kudryashov]

Another way is to use Inf (-s) = - Inf s

[Yury G. Kudryashov]

BTW, I'm going to add a more general versions of these lemmas.

[Yury G. Kudryashov]

My plan is to define conditionally_complete_lattice_default α (d : out_param α) with additional axioms Sup ∅ = d, Inf ∅ = d and similarly for unbounded sets.

[Yury G. Kudryashov]

Then prove your lemmas (and a few others) for the case d = 0.

[Yury G. Kudryashov]

I've started in branch#ccl-Sup (I tried a different approach first, there are still traces of the old approach).

[Yury G. Kudryashov]

/me is away for 2-3 hrs.

[Yaël Dillies]

Yury G. Kudryashov said:

My plan is to define conditionally_complete_lattice_default α (d : out_param α) with additional axioms Sup ∅ = d, Inf ∅ = d and similarly for unbounded sets.

That great! I had that in mind too. Then many more ℝ-specific lemmas will be gone.

[Yaël Dillies]

Yury G. Kudryashov said:

Advice: don't try to do 2 large refactors at once.

I think it's going fine! Defining antitone isn't really a refactor at all.

[Yury G. Kudryashov]

I meant, don't try to refactor two related things at once (e.g., you start refactoring A, and in the middle of this you decide to refactor B as well).

[Yury G. Kudryashov]

Sorry for bad wording.

[Yaël Dillies]

Oh yes, sure. Generalizing finset.center_mass away from ℝ isn't much. Do you still think I shouldn't do both at once?

[Yury G. Kudryashov]

I think that you will find your way. Different people are good/bad at different things.

[Yury G. Kudryashov]

If you'll see that you're refactoring too much in one branch, you can cherry-pick parts of the diff to a new branch.

[Yury G. Kudryashov]

I know how to quickly do it with magit, probably other git GUIs can help with it too.

[Yaël Dillies]

Problem is, I've never worked with finsupp. So your words are probably wise.

[Yaël Dillies]

I'll already rename it, change the order of the arguments and kill ℝ.

[Eric Wieser]

Runaway refactors are a great tool to teach you how to use git effectively to manage your own work!

[Yaël Dillies]

Yury G. Kudryashov said:

You can prove it using docs#order_iso.map_cSup instead of continuity.

Can you expand? I didn't manage.

[Yaël Dillies]

What I tried was

import algebra.module.ordered

variables {α β : Type*} [linear_ordered_field α] [ordered_add_comm_group β]

@[simps] def order_iso.smul_left [mul_action_with_zero α β] [ordered_smul α β] {a : α} (ha : 0 < a) : β ≃o β :=
{ to_fun := λ b, a • b,
  inv_fun := λ b, a⁻¹ • b,
  left_inv := inv_smul_smul' ha.ne',
  right_inv := smul_inv_smul' ha.ne',
  map_rel_iff' := λ b₁ b₂, smul_le_smul_iff_of_pos ha }

lemma real.Inf_smul_of_nonneg [module α ℝ] [ordered_smul α ℝ] {a : α} (ha : 0 ≤ a) (s : set ℝ) :
  Inf (a • s) = a • Inf s :=
begin
  obtain rfl | hs := s.eq_empty_or_nonempty,
  { rw [smul_set_empty, real.Inf_empty, smul_zero] },
  obtain rfl | ha' := ha.eq_or_lt,
  { rw [zero_smul_set hs, zero_smul],
    exact cInf_singleton 0 },
  by_cases bdd_below s,
  { rw [←order_iso.smul_left_apply _ ha', (order_iso.smul_left ℝ ha').map_cInf hs h],
    sorry
    },
  sorry
end

[Yaël Dillies]

Do we have anything about the cInf of a subtype? It would be a generalization of docs#infi_subtype

[Yury G. Kudryashov]

docs#Inf_eq_infi' only depends on has_Inf

[Yaël Dillies]

So, I've generalized the lemmas, but I still don't know where to put them.

import algebra.pointwise
import algebra.module.ordered
import data.real.basic

open set
open_locale pointwise

variables {α : Type*} [linear_ordered_field α] [module α ℝ] [ordered_smul α ℝ]

lemma real.Inf_smul_of_nonneg {a : α} (ha : 0 ≤ a) (s : set ℝ) :
  Inf (a • s) = a • Inf s :=
begin
  obtain rfl | hs := s.eq_empty_or_nonempty,
  { rw [smul_set_empty, real.Inf_empty, smul_zero] },
  obtain rfl | ha' := ha.eq_or_lt,
  { rw [zero_smul_set hs, zero_smul],
    exact cInf_singleton 0 },
  by_cases bdd_below s,
  { rw ←order_iso.smul_left_apply ℝ ha',
    exact ((order_iso.smul_left ℝ ha').map_cInf' hs h).symm },
  { rw [real.Inf_of_not_bdd_below (mt (bdd_below_smul_iff_of_pos ha').1 h),
      real.Inf_of_not_bdd_below h, smul_zero] }
end

lemma real.Sup_smul_of_nonneg {a : α} (ha : 0 ≤ a) (s : set ℝ) :
  Sup (a • s) = a • Sup s :=
begin
  obtain rfl | hs := s.eq_empty_or_nonempty,
  { rw [smul_set_empty, real.Sup_empty, smul_zero] },
  obtain rfl | ha' := ha.eq_or_lt,
  { rw [zero_smul_set hs, zero_smul],
    exact cSup_singleton 0 },
  by_cases bdd_above s,
  { rw [←order_iso.smul_left_apply _ ha'],
    exact ((order_iso.smul_left ℝ ha').map_cSup' hs h).symm },
  { rw [real.Sup_of_not_bdd_above (mt (bdd_above_smul_iff_of_pos ha').1 h),
      real.Sup_of_not_bdd_above h, smul_zero] }
end

lemma real.Inf_smul_of_nonpos {a : α} (ha : a ≤ 0) (s : set ℝ) :
  Inf (a • s) = a • Sup s :=
begin
  obtain rfl | hs := s.eq_empty_or_nonempty,
  { rw [smul_set_empty, real.Inf_empty, real.Sup_empty, smul_zero] },
  obtain rfl | ha' := ha.eq_or_lt,
  { rw [zero_smul_set hs, zero_smul],
    exact cInf_singleton 0 },
  by_cases bdd_above s,
  { rw [←order_iso.smul_left_dual_apply ℝ ha'],
    exact ((order_iso.smul_left_dual ℝ ha').map_cInf' hs h).symm },
  { rw [real.Inf_of_not_bdd_below (mt (bdd_below_smul_iff_of_neg ha').1 h),
      real.Sup_of_not_bdd_above h, smul_zero] }
end

lemma real.Sup_smul_of_nonpos {a : α} (ha : a ≤ 0) (s : set ℝ) :
  Sup (a • s) = a • Inf s :=
begin
  obtain rfl | hs := s.eq_empty_or_nonempty,
  { rw [smul_set_empty, real.Sup_empty, real.Inf_empty, smul_zero] },
  obtain rfl | ha' := ha.eq_or_lt,
  { rw [zero_smul_set hs, zero_smul],
    exact cSup_singleton 0 },
  by_cases bdd_below s,
  { rw [←order_iso.smul_left_dual_apply ℝ ha'],
    exact ((order_iso.smul_left_dual ℝ ha').map_cSup' hs h).symm },
  { rw [real.Sup_of_not_bdd_above (mt (bdd_above_smul_iff_of_neg ha').1 h),
      real.Inf_of_not_bdd_below h, smul_zero] }
end

[Yaël Dillies]

I couldn't find any file that had this combination of imports yet (but I did it manually so I might be wrong). What about I create a new file data.real.pointwise or data.real.smul?

[Yaël Dillies]

#9707

[Yaël Dillies]

Hopefully the final PR before the Minkowski functional one!