feat: Extend a nonnegative function (#7418)

The result of extending a nonnegative function by a nonnegative function is nonnegative.

Mathlib/Algebra/Order/Pi.lean

@@ -15,14 +15,10 @@ import Mathlib.Tactic.Positivity
 This file defines instances for ordered group, monoid, and related structures on Pi types.
 -/
 
-set_option autoImplicit true
-
-variable {ι α β : Type*}
-
-variable {I : Type u}
+variable {ι I α β γ : Type*}
 
 -- The indexing type
-variable {f : I → Type v}
+variable {f : I → Type*}
 
 -- The family of types already equipped with instances
 variable (x y : ∀ i, f i) (i : I)
@@ -110,7 +106,7 @@ instance orderedCommRing [∀ i, OrderedCommRing (f i)] : OrderedCommRing (∀ i
 end Pi
 
 namespace Function
-
+section const
 variable (β) [One α] [Preorder α] {a : α}
 
 @[to_additive const_nonneg_of_nonneg]
@@ -149,6 +145,18 @@ theorem const_lt_one : const β a < 1 ↔ a < 1 :=
 #align function.const_lt_one Function.const_lt_one
 #align function.const_neg Function.const_neg
 
+end const
+
+section extend
+variable [One γ] [LE γ] {f : α → β} {g : α → γ} {e : β → γ}
+
+@[to_additive extend_nonneg] lemma one_le_extend (hg : 1 ≤ g) (he : 1 ≤ e) : 1 ≤ extend f g e :=
+  fun _b ↦ by classical exact one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)
+
+@[to_additive] lemma extend_le_one (hg : g ≤ 1) (he : e ≤ 1) : extend f g e ≤ 1 :=
+  fun _b ↦ by classical exact dite_le_one (fun _ ↦ hg _) (fun _ ↦ he _)
+
+end extend
 end Function
 --Porting note: Tactic code not ported yet
 -- namespace Tactic

Mathlib/Order/Basic.lean

@@ -1452,3 +1452,41 @@ noncomputable instance AsLinearOrder.linearOrder {α} [PartialOrder α] [IsTotal
   le_total := @total_of α (· ≤ ·) _
   decidableLE := Classical.decRel _
 #align as_linear_order.linear_order AsLinearOrder.linearOrder
+
+section dite
+variable [One α] {p : Prop} [Decidable p] {a : p → α} {b : ¬ p → α}
+
+@[to_additive dite_nonneg]
+lemma one_le_dite [LE α] (ha : ∀ h, 1 ≤ a h) (hb : ∀ h, 1 ≤ b h) : 1 ≤ dite p a b := by
+  split; exacts [ha ‹_›, hb ‹_›]
+
+@[to_additive]
+lemma dite_le_one [LE α] (ha : ∀ h, a h ≤ 1) (hb : ∀ h, b h ≤ 1) : dite p a b ≤ 1 := by
+  split; exacts [ha ‹_›, hb ‹_›]
+
+@[to_additive dite_pos]
+lemma one_lt_dite [LT α] (ha : ∀ h, 1 < a h) (hb : ∀ h, 1 < b h) : 1 < dite p a b := by
+  split; exacts [ha ‹_›, hb ‹_›]
+
+@[to_additive]
+lemma dite_lt_one [LT α] (ha : ∀ h, a h < 1) (hb : ∀ h, b h < 1) : dite p a b < 1 := by
+  split; exacts [ha ‹_›, hb ‹_›]
+
+end dite
+
+section
+variable [One α] {p : Prop} [Decidable p] {a b : α}
+
+@[to_additive ite_nonneg]
+lemma one_le_ite [LE α] (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ ite p a b := by split <;> assumption
+
+@[to_additive]
+lemma ite_le_one [LE α] (ha : a ≤ 1) (hb : b ≤ 1) : ite p a b ≤ 1 := by split <;> assumption
+
+@[to_additive ite_pos]
+lemma one_lt_ite [LT α] (ha : 1 < a) (hb : 1 < b) : 1 < ite p a b := by split <;> assumption
+
+@[to_additive]
+lemma ite_lt_one [LT α] (ha : a < 1) (hb : b < 1) : ite p a b < 1 := by split <;> assumption
+
+end