Todd Waugh Ambridge, January 2024

# Global optimisation

\begin{code}
{-# OPTIONS --without-K --safe #-}

open import MLTT.Spartan
open import UF.FunExt
open import Fin.Type
open import Fin.Bishop


module TWA.Thesis.Chapter4.GlobalOptimisation (fe : FunExt) where

open import TWA.Thesis.Chapter3.ClosenessSpaces fe
open import TWA.Thesis.Chapter4.ApproxOrder fe
\end{code}

## Absolute global optimisation

\begin{code}
is-global-minimal : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (_≀_ : Y β†’ Y β†’ 𝓦 Μ‡ )
                  β†’ (X β†’ Y) β†’ X β†’ 𝓀 βŠ” 𝓦 Μ‡
is-global-minimal {𝓀} {π“₯} {𝓦'} {X} _≀_ f xβ‚€ = (x : X) β†’ f xβ‚€ ≀ f x

has-global-minimal : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (_≀_ : Y β†’ Y β†’ 𝓦 Μ‡ )
                   β†’ (X β†’ Y) β†’ 𝓀 βŠ” 𝓦 Μ‡
has-global-minimal f = Σ ∘ (is-global-minimal f)

Fin-global-minimal : (n : β„•) β†’ Fin n β†’ {Y : 𝓀 Μ‡ }
                 β†’ (_≀_ : Y β†’ Y β†’ 𝓦 Μ‡ )
                 β†’ is-linear-preorder _≀_
                 β†’ (f : Fin n β†’ Y)
                 β†’ has-global-minimal _≀_ f
Fin-global-minimal 1 𝟎 _≀_ (p , _) f = 𝟎 , Ξ³
 where
  Ξ³ : is-global-minimal _≀_ f 𝟎
  Ξ³ 𝟎 = ≀-refl⟨ p ⟩ (f 𝟎)
Fin-global-minimal (succ (succ n)) x _≀_ l@(p , _) f
 with Fin-global-minimal (succ n) 𝟎 _≀_ l (f ∘ suc)
... | (x'β‚€ , m) = Cases (≀-linear⟨ l ⟩ (f (suc x'β‚€)) (f 𝟎)) γ₁ Ξ³β‚‚
 where
  γ₁ : f (suc x'β‚€) ≀ f 𝟎 β†’ has-global-minimal _≀_ f
  γ₁ x'β‚€β‰€πŸŽ = suc x'β‚€ , Ξ³
   where
    Ξ³ : (x : Fin (succ (succ n))) β†’ f (suc x'β‚€) ≀ f x
    Ξ³ 𝟎 = x'β‚€β‰€πŸŽ
    Ξ³ (suc x) = m x
  Ξ³β‚‚ : f 𝟎 ≀ f (suc x'β‚€) β†’ has-global-minimal _≀_ f
  Ξ³β‚‚ πŸŽβ‰€x'β‚€ = 𝟎 , Ξ³
   where
    Ξ³ : (x : Fin (succ (succ n))) β†’ f 𝟎 ≀ f x
    Ξ³ 𝟎 = ≀-refl⟨ p ⟩ (f 𝟎)
    Ξ³ (suc x)
     = ≀-trans⟨ p ⟩ (f 𝟎) (f (suc x'β‚€)) (f (suc x)) πŸŽβ‰€x'β‚€ (m x)

finite-global-minimal : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                      β†’ X β†’ finite-linear-order X
                      β†’ (_≀_ : Y β†’ Y β†’ 𝓦 Μ‡ )
                      β†’ is-linear-preorder _≀_
                      β†’ (f : X β†’ Y)
                      β†’ has-global-minimal _≀_ f
finite-global-minimal x (n , e@(g , _ , (h , ΞΌ))) _≀_ l f
 = h xβ‚€ , Ξ» x β†’ transport (f (h xβ‚€) ≀_) (ap f (ΞΌ x)) (Ξ³β‚€ (g x))
 where
 Ξ³ : has-global-minimal _≀_ (f ∘ h)
 Ξ³ = Fin-global-minimal n (g x) _≀_ l (f ∘ h)
 xβ‚€ : Fin n
 xβ‚€ = pr₁ Ξ³
 Ξ³β‚€ : is-global-minimal _≀_ (f ∘ h) xβ‚€
 Ξ³β‚€ = prβ‚‚ Ξ³
\end{code}

## Approximate global optimisation

\begin{code}
is_global-minimal : β„• β†’ {𝓀 π“₯ : Universe}
                  β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                  β†’ (_≀ⁿ_ : Y β†’ Y β†’ β„• β†’ 𝓦 Μ‡ )
                  β†’ (f : X β†’ Y) β†’ X β†’ 𝓦 βŠ” 𝓀 Μ‡
(is Ο΅ global-minimal) {𝓀} {π“₯} {X} _≀ⁿ_ f xβ‚€
 = (x : X) β†’ (f xβ‚€ ≀ⁿ f x) Ο΅

has_global-minimal : β„• β†’ {𝓀 π“₯ : Universe} {X : 𝓀 Μ‡ }
                   β†’ {Y : π“₯ Μ‡ }
                   β†’ (_≀ⁿ_ : Y β†’ Y β†’ β„• β†’ 𝓦 Μ‡ )
                   β†’ (f : X β†’ Y) β†’ (𝓦 βŠ” 𝓀) Μ‡
(has Ο΅ global-minimal) {𝓀} {π“₯} {𝓦} {X} _≀ⁿ_ f
 = Ξ£ ((is Ο΅ global-minimal) {𝓀} {π“₯} {𝓦} {X} _≀ⁿ_ f)

F-Ο΅-global-minimal : {X : 𝓀 Μ‡ } (Y : ClosenessSpace π“₯)
                   β†’ X β†’ finite-linear-order X
                   β†’ (_≀ⁿ_ : ⟨ Y ⟩ β†’ ⟨ Y ⟩ β†’ β„• β†’ 𝓦' Μ‡ )
                   β†’ is-approx-order Y _≀ⁿ_
                   β†’ (Ο΅ : β„•) β†’ (f : X β†’ ⟨ Y ⟩)
                   β†’ (has Ο΅ global-minimal) _≀ⁿ_ f
F-Ο΅-global-minimal Y x l _≀ⁿ_ a Ο΅
 = finite-global-minimal x l (Ξ» x y β†’ (x ≀ⁿ y) Ο΅) (≀ⁿ-all-linear Y a Ο΅)
\end{code}

## Global optimisation theorem

\begin{code}
cover-continuity-lemma
 : (X : ClosenessSpace 𝓀) {X' : 𝓀' Μ‡ } (Y : ClosenessSpace π“₯)
 β†’ (_≀ⁿ_ : ⟨ Y ⟩ β†’ ⟨ Y ⟩ β†’ β„• β†’ 𝓦' Μ‡ )
 β†’ is-approx-order Y _≀ⁿ_
 β†’ (Ο΅ : β„•) β†’ (f : ⟨ X ⟩ β†’ ⟨ Y ⟩) (Ο• : f-ucontinuous X Y f)
 β†’ let Ξ΄ = pr₁ (Ο• Ο΅) in (((g , _) , _) : X' is Ξ΄ net-of X)
 β†’ finite-linear-order X'
 β†’ (x : ⟨ X ⟩) β†’ Ξ£ x' κž‰ X' , (f (g x') ≀ⁿ f x) Ο΅
cover-continuity-lemma
 X Y _≀ⁿ_ a Ο΅ f Ο• ((g , h , Ξ·) , _) e x
 = h x
 , ≀ⁿ-close Y a Ο΅ (f (g (h x))) (f x)
     (C-sym Y Ο΅ (f x) (f (g (h x)))
       (prβ‚‚ (Ο• Ο΅) x (g (h x))
         (Ξ· x)))

global-opt : (X : ClosenessSpace 𝓀) (Y : ClosenessSpace π“₯)
           β†’ ⟨ X ⟩
           β†’ (_≀ⁿ_ : ⟨ Y ⟩ β†’ ⟨ Y ⟩ β†’ β„• β†’ 𝓦' Μ‡ )
           β†’ is-approx-order Y _≀ⁿ_
           β†’ (Ο΅ : β„•)
           β†’ (f : ⟨ X ⟩ β†’ ⟨ Y ⟩) (Ο• : f-ucontinuous X Y f)
           β†’ totally-bounded X 𝓀'
           β†’ (has Ο΅ global-minimal) _≀ⁿ_ f
global-opt {𝓀} {π“₯} {𝓦'} {𝓀'} X Y x₁ _≀ⁿ_ a Ο΅ f Ο• t
 = (g x'β‚€)
 , (Ξ» x β†’ ≀ⁿ-trans Y a Ο΅
            (f (g x'β‚€)) (f (g (h x))) (f x)
            (m (h x)) (h-min x))
 where
  Ξ΄ : β„•
  Ξ΄ = pr₁ (Ο• Ο΅)
  X' : 𝓀' Μ‡
  X' =  pr₁ (t Ξ΄)
  X'-is-Ξ΄-net : X' is Ξ΄ net-of X
  X'-is-Ξ΄-net  = prβ‚‚ (t Ξ΄)
  X'-is-finite : finite-linear-order X'
  X'-is-finite = prβ‚‚ X'-is-Ξ΄-net
  g :   X'  β†’ ⟨ X ⟩
  g = pr₁ (pr₁ X'-is-Ξ΄-net)
  h : ⟨ X ⟩ β†’   X'
  h = pr₁ (prβ‚‚ (pr₁ X'-is-Ξ΄-net))
  Ξ· : (x : ⟨ X ⟩) β†’ Ξ£ x' κž‰ X' , (f (g x') ≀ⁿ f x) Ο΅
  Ξ· = cover-continuity-lemma X Y _≀ⁿ_
        a Ο΅ f Ο• X'-is-Ξ΄-net X'-is-finite
  h-min : (x : ⟨ X ⟩) β†’ (f (g (h x)) ≀ⁿ f x) Ο΅
  h-min x = prβ‚‚ (Ξ· x)
  first  : has Ο΅ global-minimal _≀ⁿ_ (f ∘ g)
  first
   = F-Ο΅-global-minimal Y (h x₁) X'-is-finite _≀ⁿ_ a Ο΅ (f ∘ g)
  x'β‚€ : X'
  x'β‚€ = pr₁ first
  m  : is Ο΅ global-minimal _≀ⁿ_ (f ∘ g) x'β‚€
  m  = prβ‚‚ first
\end{code}