pointwise min and max

Stream: Is there code for X?

[Yakov Pechersky]

Do we have something like the following already? @Filippo A. E. Nuccio , you were asking about pointwise function inequality, so you might know...

import analysis.convex.basic

universes u v

open set linear_map submodule
variables {E : Type u} {β : Type v}

section pointwise_min

variables [linear_order β]

@[simp] def pointwise.min (f g : E → β) (x : E) : β := min (f x) (g x)
@[simp] def pointwise.max (f g : E → β) (x : E) : β := max (f x) (g x)
@[simp] def pointwise.abs [has_neg β] (f : E → β) : E → β := pointwise.max f (-f : E → β)

variables {f g : E → β}

lemma pointwise.min_eq_left (h : f ≤ g) : pointwise.min f g = f :=
funext $ λ x, min_eq_left (h x)
lemma pointwise.min_eq_right (h : g ≤ f) : pointwise.min f g = g :=
funext $ λ x, min_eq_right (h x)
lemma pointwise.max_eq_left (h : g ≤ f) : pointwise.max f g = f :=
funext $ λ x, max_eq_left (h x)
lemma pointwise.max_eq_right (h : f ≤ g) : pointwise.max f g = g :=
funext $ λ x, max_eq_right (h x)

end pointwise_min

section convex

variables [ordered_add_comm_group E] [linear_ordered_add_comm_monoid β] [module ℝ E] [module ℝ β]
   [ordered_module ℝ E] [ordered_module ℝ β]
   {s : set E} {f g : E → β}

lemma convex_on.pointwise_max (hf : convex_on s f) (hg : convex_on s g) :
   convex_on s (pointwise.max f g) :=
begin
   refine ⟨hf.left, λ x y hx hy a b ha hb hab, _⟩,
   rw convex_on_iff_div at hf hg,
   simp only [max_le_iff, pointwise.max],
   split,
   { calc
      f (a • x + b • y) ≤ a • f x + b • f y :
         by simpa [hab] using hf.right hx hy ha hb (zero_lt_one.trans_le hab.ge)
      ...               ≤ a • max (f x) (g x) + b • max (f y) (g y) :
         add_le_add
            (smul_le_smul_of_nonneg (le_max_left _ _) ha)
            (smul_le_smul_of_nonneg (le_max_left _ _) hb) },
   { calc
      g (a • x + b • y) ≤ a • g x + b • g y :
         by simpa [hab] using hg.right hx hy ha hb (zero_lt_one.trans_le hab.ge)
      ...               ≤ a • max (f x) (g x) + b • max (f y) (g y) :
         add_le_add
            (smul_le_smul_of_nonneg (le_max_right _ _) ha)
            (smul_le_smul_of_nonneg (le_max_right _ _) hb) }
end

lemma concave_on.pointwise_min (hf : concave_on s f) (hg : concave_on s g) :
   concave_on s (pointwise.min f g) :=
@convex_on.pointwise_max _ (order_dual β) _ _ _ _ _ _ _ _ _ hf hg

end convex

[Filippo A. E. Nuccio]

I am sorry, I really don't know. I was indeed looking for pointwise inequality, but the pi.le_def lemma was enough for me and I haven't dug any deeper.

[Yakov Pechersky]

Do you think my pointwise.min should be called pi.min?

[Filippo A. E. Nuccio]

Well, I don't know. I would say that pi.min should express the existence of a universal min assuming all Types have a min; but I think that there might be other definitions of min, no?

[Yakov Pechersky]

Yes, I agree, good point. That's maybe indicates it should be called pointwise.

[Filippo A. E. Nuccio]

I would rather argue that I'd call it pointwise_min rather than with a dot since it seems to me that no dot-notation is involved.

[Yakov Pechersky]

Also makes sense. Maybe we will have a pointwise namespace at somepoint?

[Filippo A. E. Nuccio]

This seems a good idea.

[Eric Wieser]

We already have pointwise.min, it's has_inf.inf / docs#pi.has_inf:

-- added on to your example above
example (f g : E → β) : pointwise.min f g = f ⊓ g := rfl
example (f g : E → β) : pointwise.max f g = f ⊔ g := rfl

[Kyle Miller]

Going off topic a bit, if there were J-like "verb trains" (which wouldn't make any sense for Lean to have), then λ x, min (f x) (g x) could be written as f min g, which I suppose is essentially what the has_inf.inf instance is doing by using an operator version of min. "Verb trains" are all just short-hand ways of doing common sorts of combinators, and I'm slightly surprised that this particular combinator doesn't already exist in function.lean. Neither on_fun nor combine do quite the right thing (combine is the "dyadic fork" in J-speak, but there's no "monadic fork").

I'm not suggesting adding the missing combinators though. Plain-old lambdas usually seem to be the clearer and more accessible choice, if there's not already a specialized meaningful notation.

[Yakov Pechersky]

#8958

[Anne Baanen]

Kyle Miller said:

I'm slightly surprised that this particular combinator doesn't already exist in function.lean.

They do already exist, kind of, in unassembled format:

import tactic.suggest
import logic.function.basic

variables {α β : Type} [linear_order β] (f g : α → β)

open combinator

-- If you like SKI-ing:
#reduce S (S (K min) f) g

-- Or alternatively, if you like Haskell:
/-- I didn't manage to put an instance on `(→) α`, so introduce a synonym. -/
def reader' (α β : Type*) := α → β

instance reader'.applicative : applicative (reader' α) :=
{ pure := λ β, combinator.K,
  seq := λ β γ, combinator.S }

#reduce (min <$> f <*> g : reader' α β)

[Kyle Miller]

I guess K could be used to turn 2-argument combine into a 1-argument combine. I might have run into an elaborator bug, though:

universes u v

open set
variables {E : Type u} {β : Type v}

section pointwise_min

variables [linear_order β]
open combinator

@[simp] def pointwise.min (f g : E → β) : E → β := (K f -[min]- K g) punit.star

/-
kernel failed to type check declaration 'pointwise.min' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  Π {E : Type u} {β : Type v} [_inst_1 : linear_order β], (E → β) → (E → β) → E → β
elaborated value:
  λ {E : Type u} {β : Type v} [_inst_1 : linear_order β] (f g : E → β), (K f -[min]- K g) punit.star
nested exception message:
type mismatch at application
  @K (E → β)
term
  E → β
has type
  Type (max u v)
but is expected to have type
  Type u_1
-/

end pointwise_min