Theory Fun_Ultrametric_Restriction_Spaces

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 * Author: Benjamin Puyobro, Université Paris-Saclay,
           IRT SystemX, CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)



section ‹Functions›

(*<*)
theory Fun_Ultrametric_Restriction_Spaces
  imports Ultrametric_Restriction_Spaces Banach_Theorem_Extension
begin
  (*>*)


subsection ‹Restriction Space›


instantiation ‹fun› :: (type, restriction_σ) restriction_σ
begin

definition restriction_σ_fun :: ‹('a ⇒ 'b) itself ⇒ nat ⇒ real›
  where ‹restriction_σ_fun _ ≡ restriction_σ TYPE('b)›

instance by intro_classes

end

instantiation ‹fun› :: (type, non_decseq_restriction_space) non_decseq_restriction_space
begin

definition dist_fun :: ‹['a ⇒ 'b, 'a ⇒ 'b] ⇒ real›
  where ‹dist_fun f g ≡ INF n ∈ restriction_related_set f g. restriction_σ TYPE('a ⇒ 'b) n›

definition uniformity_fun :: ‹(('a ⇒ 'b) × ('a ⇒ 'b)) filter›
  where ‹uniformity_fun ≡ INF e∈{0 <..}. principal {(x, y). dist x y < e}›

definition open_fun :: ‹('a ⇒ 'b) set ⇒ bool›
  where ‹open_fun U ≡ ∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity›

instance by intro_classes
    (simp_all add: restriction_σ_fun_def dist_fun_def open_fun_def
      uniformity_fun_def restriction_σ_tendsto_zero)

end


instance ‹fun› :: (type, decseq_restriction_space) decseq_restriction_space
  by intro_classes (simp add: restriction_σ_fun_def decseq_restriction_σ)

instance ‹fun› :: (type, strict_decseq_restriction_space) strict_decseq_restriction_space
  by intro_classes
    (simp add: restriction_σ_fun_def strict_decseq_restriction_σ)


instantiation ‹fun› :: (type, restriction_δ) restriction_δ
begin

definition restriction_δ_fun :: ‹('a ⇒ 'b) itself ⇒ real›
  where ‹restriction_δ_fun _ ≡ restriction_δ TYPE('b)›

instance by intro_classes (simp_all add: restriction_δ_fun_def)

end


instance ‹fun› :: (type, at_least_geometric_restriction_space) at_least_geometric_restriction_space
proof intro_classes
  show ‹0 < restriction_σ TYPE('a ⇒ 'b) n› for n
    by (simp add: restriction_σ_fun_def)
next
  show ‹restriction_σ TYPE('a ⇒ 'b) (Suc n)
        ≤ restriction_δ TYPE('a ⇒ 'b) * restriction_σ TYPE('a ⇒ 'b) n› for n
    by (simp add: restriction_σ_le restriction_σ_fun_def restriction_δ_fun_def)
next
  show ‹dist f g = Inf (restriction_σ_related_set f g)› for f g :: ‹'a ⇒ 'b›
    by (simp add: dist_fun_def)
qed

instance ‹fun› :: (type, geometric_restriction_space) geometric_restriction_space
proof intro_classes
  show ‹restriction_σ TYPE('a ⇒ 'b) n = restriction_δ TYPE('a ⇒ 'b) ^ n› for n
    by (simp add: restriction_σ_fun_def restriction_σ_is restriction_δ_fun_def)
next
  show ‹dist f g = Inf (restriction_σ_related_set f g)› for f g :: ‹'a ⇒ 'b›
    by (simp add: dist_fun_def)
qed


lemma dist_image_le_dist_fun : ‹dist (f x) (g x) ≤ dist f g›
  for f g :: ‹'a ⇒ 'b :: non_decseq_restriction_space›
proof (unfold dist_restriction_is, rule cInf_superset_mono)
  show ‹restriction_σ_related_set f g ≠ {}› by simp
next
  show ‹bdd_below (restriction_σ_related_set (f x) (g x))›
    by (simp add: bounded_imp_bdd_below bounded_restriction_σ_related_set)
next
  show ‹restriction_σ_related_set f g ⊆ restriction_σ_related_set (f x) (g x)›
    unfolding restriction_fun_def restriction_σ_fun_def 
    by (simp add: image_def subset_iff) metis
qed


lemma Sup_dist_image_le_dist_fun : ‹(SUP x. dist (f x) (g x)) ≤ dist f g›
  for f g :: ‹'a ⇒ 'b :: non_decseq_restriction_space›
  by (simp add: dist_image_le_dist_fun cSUP_least)
    ― ‹The other inequality will require the additional assumption \<^const>‹decseq›.›



context fixes f g :: ‹'a ⇒ 'b :: decseq_restriction_space› begin

lemma reached_dist_fun : ‹∃x. dist f g = dist (f x) (g x)›
proof (cases ‹f = g›)
  show ‹f = g ⟹ ∃x. dist f g = dist (f x) (g x)› by simp
next
  assume ‹f ≠ g›
  let ?n = ‹Sup (restriction_related_set f g)›
  from not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq_simplified(2, 3)[OF ‹f ≠ g›]
  obtain x where ‹∀m≤?n. f x ↓ m = g x ↓ m› ‹f x ↓ Suc ?n ≠ g x ↓ Suc ?n›
    unfolding restriction_fun_def by (meson lessI)
  hence ‹dist (f x) (g x) = restriction_σ TYPE('b) ?n›
    by (metis (no_types, lifting) le_neq_implies_less not_less_eq_eq
        not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq_simplified)
  with not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq_simplified(1)
    [OF ‹f ≠ g›, unfolded restriction_σ_fun_def]
  have ‹dist f g = dist (f x) (g x)› by simp
  thus ‹∃x. dist f g = dist (f x) (g x)› ..
qed


lemma dist_fun_eq_Sup_dist_image : ‹dist f g = (SUP x. dist (f x) (g x))›
proof (rule order_antisym)
  show ‹(SUP x. dist (f x) (g x)) ≤ dist f g› by (fact Sup_dist_image_le_dist_fun)
next
  from reached_dist_fun obtain x where ‹dist f g = dist (f x) (g x)› ..
  thus ‹dist f g ≤ (SUP x. dist (f x) (g x))›
  proof (rule ord_eq_le_trans)
    show ‹dist (f x) (g x) ≤ (SUP x. dist (f x) (g x))›
    proof (rule cSup_upper)
      show ‹dist (f x) (g x) ∈ range (λx. dist (f x) (g x))› by simp
    next
      show ‹bdd_above (range (λx. dist (f x) (g x)))›
        by (rule bdd_aboveI[of _ ‹dist f g›]) (auto intro: dist_image_le_dist_fun)
    qed
  qed
qed


lemma fun_restriction_space_Sup_properties :
  ‹dist (f x) (g x) ≤ dist f g›
  ‹(⋀x. dist (f x) (g x) ≤ b) ⟹ dist f g ≤ b›
  by (use reached_dist_fun in ‹auto simp add: dist_image_le_dist_fun›)


end


subsection ‹Completeness›

text ‹Actually we can obtain even better: when the instance \<^typ>‹'b› of
      \<^class>‹decseq_restriction_space› is also an instance of \<^class>‹complete_space›,
      the type \<^typ>‹'a ⇒ 'b› is an instance of \<^class>‹complete_space›.›

text ‹This is because when \<^typ>‹'b› is an instance of \<^class>‹decseq_restriction_space›
      (and not only \<^class>‹non_decseq_restriction_space›) the distance between two functions
      is reached (see @{thm reached_dist_fun}).›



text ‹The only remaining thing is to prove that completeness is preserved on higher-order.›

instance ‹fun› :: (type, complete_decseq_restriction_space) complete_decseq_restriction_space
  by intro_classes (fact restriction_chain_imp_restriction_convergent)

instance ‹fun› :: (type, complete_strict_decseq_restriction_space) complete_strict_decseq_restriction_space
  by intro_classes (fact restriction_chain_imp_restriction_convergent)

instance ‹fun› :: (type, complete_at_least_geometric_restriction_space) complete_at_least_geometric_restriction_space
  by intro_classes (fact restriction_chain_imp_restriction_convergent)

instance ‹fun› :: (type, complete_geometric_restriction_space) complete_geometric_restriction_space
  by intro_classes (fact restriction_chain_imp_restriction_convergent)



subsection ‹Kind of Extensionality›

context fixes f :: ‹['a :: metric_space, 'b :: type] ⇒
                    'c :: decseq_restriction_space› begin

lemma lipschitz_with_simplification:
  ‹lipschitz_with f α ⟷ (∀y. lipschitz_with (λx. f x y) α)›
proof (intro iffI allI)
  fix y assume assm : ‹lipschitz_with f α›
  show ‹lipschitz_with (λx. f x y) α›
  proof (rule lipschitz_withI)
    from assm[THEN lipschitz_withD1] show ‹0 ≤ α› .
  next
    show ‹dist (f x1 y) (f x2 y) ≤ α * dist x1 x2› for x1 x2
      by (rule order_trans[OF _ assm[THEN lipschitz_withD2]])
        (simp add: dist_image_le_dist_fun)
  qed
next
  assume assm : ‹∀y. lipschitz_with (λx. f x y) α›
  show ‹lipschitz_with f α›
  proof (rule lipschitz_withI)
    from assm[rule_format, THEN lipschitz_withD1] show ‹0 ≤ α› .
  next
    fix x1 x2
    obtain y where ‹dist (f x1) (f x2) = dist (f x1 y) (f x2 y)›
      by (meson reached_dist_fun)
    also have ‹… ≤ α * dist x1 x2› by (rule assm[rule_format, THEN lipschitz_withD2])
    finally show ‹dist (f x1) (f x2) ≤ α * dist x1 x2› .
  qed
qed


lemma non_expanding_simplification :
  ‹non_expanding f ⟷ (∀y. non_expanding (λx. f x y))›
  by (metis lipschitz_with_simplification non_expanding_on_def)


lemma contraction_with_simplification:
  ‹contraction_with f α ⟷ (∀y. contraction_with (λx. f x y) α)›
  by (metis contraction_with_on_def lipschitz_with_simplification)


end

(*<*)
end
  (*>*)