Theory Banach_Theorem_Extension

(***********************************************************************************
 * 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 ‹Definitions on Functions of Metric Space›

(*<*)
theory  Banach_Theorem_Extension
  imports "HOL-Analysis.Elementary_Metric_Spaces"
begin
  (*>*)

text ‹In this theory, we define the notion of lipschitz map, non-expanding map
      and contraction map. We also establish correspondences.›


subsection ‹Definitions›

subsubsection ‹Lipschitz Map›

text ‹This notion is a generalization of contraction map and non-expanding map.›

definition lipschitz_with_on :: ‹['a :: metric_space ⇒ 'b :: metric_space, real, 'a set] ⇒ bool›
  where ‹lipschitz_with_on f α A ≡ 0 ≤ α ∧ (∀x∈A. ∀y∈A. dist (f x) (f y) ≤ α * dist x y)›

abbreviation lipschitz_with :: ‹['a :: metric_space ⇒ 'b :: metric_space, real] ⇒ bool›
  where ‹lipschitz_with f α ≡ lipschitz_with_on f α UNIV›


lemma lipschitz_with_onI :
  ‹⟦0 ≤ α; ⋀x y. ⟦x ∈ A; y ∈ A; x ≠ y; f x ≠ f y⟧ ⟹ dist (f x) (f y) ≤ α * dist x y⟧ ⟹
   lipschitz_with_on f α A›
  unfolding lipschitz_with_on_def by (metis dist_eq_0_iff zero_le_dist zero_le_mult_iff)

lemma lipschitz_withI :
  ‹⟦0 ≤ α; ⋀x y. x ≠ y ⟹ f x ≠ f y ⟹ dist (f x) (f y) ≤ α * dist x y⟧ ⟹ 
   lipschitz_with f α›
  by (rule lipschitz_with_onI)

lemma lipschitz_with_onD1 : ‹lipschitz_with_on f α A ⟹ 0 ≤ α›
  unfolding lipschitz_with_on_def by simp

lemma lipschitz_withD1 : ‹lipschitz_with f α ⟹ 0 ≤ α›
  by (rule lipschitz_with_onD1)

lemma lipschitz_with_onD2 :
  ‹lipschitz_with_on f α A ⟹ x ∈ A ⟹ y ∈ A ⟹ dist (f x) (f y) ≤ α * dist x y›
  unfolding lipschitz_with_on_def by simp

lemma lipschitz_withD2 :
  ‹lipschitz_with f α ⟹ dist (f x) (f y) ≤ α * dist x y›
  unfolding lipschitz_with_on_def by simp

lemma lipschitz_with_imp_lipschitz_with_on: ‹lipschitz_with f α ⟹ lipschitz_with_on f α A›
  by (simp add: lipschitz_with_on_def)


lemma lipschitz_with_on_imp_lipschitz_with_on_ge : ‹lipschitz_with_on f β A›
  if ‹α ≤ β› and ‹lipschitz_with_on f α A›
proof (rule lipschitz_with_onI)
  show ‹0 ≤ β› by (meson order_trans lipschitz_with_onD1 that)
next
  fix x y assume ‹x ∈ A› and ‹y ∈ A›
  from ‹lipschitz_with_on f α A›[THEN lipschitz_with_onD2, OF this]
  have ‹dist (f x) (f y) ≤ α * dist x y› .
  from order_trans[OF this] show ‹dist (f x) (f y) ≤ β * dist x y›
    by (simp add: mult_right_mono ‹α ≤ β›)
qed


theorem lipschitz_with_on_comp_lipschitz_with_on :
  ‹lipschitz_with_on (λx. g (f x)) (β * α) A›
  if ‹f ` A ⊆ B› ‹lipschitz_with_on g β B› ‹lipschitz_with_on f α A›
proof (rule lipschitz_with_onI)
  show ‹0 ≤ β * α› by (metis lipschitz_with_onD1 mult_nonneg_nonneg that(2, 3))
next
  fix x y assume ‹x ∈ A› and ‹y ∈ A›
  with ‹f ` A ⊆ B› have ‹f x ∈ B› and ‹f y ∈ B› by auto
  have ‹dist (g (f x)) (g (f y)) ≤ β * dist (f x) (f y)›
    by (fact that(2)[THEN lipschitz_with_onD2, OF ‹f x ∈ B› ‹f y ∈ B›])
  also have ‹… ≤ β * (α * dist x y)›
    by (fact mult_left_mono[OF that(3)[THEN lipschitz_with_onD2, OF ‹x ∈ A› ‹y ∈ A›]
                               that(2)[THEN lipschitz_with_onD1]])
  also have ‹… = β * α * dist x y› by simp
  finally show ‹dist (g (f x)) (g (f y)) ≤ …› .
qed

corollary lipschitz_with_comp_lipschitz_with : 
  ‹⟦lipschitz_with g β; lipschitz_with f α⟧ ⟹
   lipschitz_with (λx. g (f x)) (β * α)›
  using lipschitz_with_on_comp_lipschitz_with_on by blast



subsubsection ‹Non-expanding Map›

definition non_expanding_on :: ‹['a :: metric_space ⇒ 'b :: metric_space, 'a set] ⇒ bool›
  where ‹non_expanding_on f A ≡ lipschitz_with_on f 1 A›

abbreviation non_expanding :: ‹['a :: metric_space ⇒ 'b :: metric_space] ⇒ bool›
  where ‹non_expanding f ≡ non_expanding_on f UNIV›

lemma non_expanding_onI :
  ‹⟦⋀x y. ⟦x ∈ A; y ∈ A; x ≠ y; f x ≠ f y⟧ ⟹ dist (f x) (f y) ≤ dist x y⟧ ⟹ 
   non_expanding_on f A›
  by (simp add: lipschitz_with_onI non_expanding_on_def)

lemma non_expandingI :
  ‹⟦⋀x y. x ≠ y ⟹ f x ≠ f y ⟹ dist (f x) (f y) ≤ dist x y⟧ ⟹ non_expanding f›
  by (rule non_expanding_onI)

lemma non_expanding_onD :
  ‹non_expanding_on f A ⟹ x ∈ A ⟹ y ∈ A ⟹ dist (f x) (f y) ≤ dist x y›
  by (metis lipschitz_with_onD2 mult_1 non_expanding_on_def)

lemma non_expandingD : ‹non_expanding f ⟹ dist (f x) (f y) ≤ dist x y›
  by (simp add: non_expanding_onD)

lemma non_expanding_imp_non_expanding_on: ‹non_expanding f ⟹ non_expanding_on f A›
  by (meson non_expandingD non_expanding_onI)


lemma non_expanding_on_comp_non_expanding_on :
  ‹⟦f ` A ⊆ B; non_expanding_on g B; non_expanding_on f A⟧ ⟹
   non_expanding_on (λx. g (f x)) A›
  unfolding non_expanding_on_def
  by (metis (no_types) lipschitz_with_on_comp_lipschitz_with_on mult_1)

corollary non_expanding_comp_non_expanding  :
  ‹⟦non_expanding g; non_expanding f⟧ ⟹ non_expanding (λx. g (f x))›
  by (blast intro: non_expanding_on_comp_non_expanding_on)



subsubsection ‹Contraction Map›

definition contraction_with_on :: ‹['a :: metric_space ⇒ 'b :: metric_space, real, 'a set] ⇒ bool›
  where ‹contraction_with_on f α A ≡ α < 1 ∧ lipschitz_with_on f α A›

abbreviation contraction_with :: ‹['a :: metric_space ⇒ 'b :: metric_space, real] ⇒ bool›
  where ‹contraction_with f α ≡ contraction_with_on f α UNIV›

definition contraction_on :: ‹['a :: metric_space ⇒ 'b :: metric_space, 'a set] ⇒ bool›
  where ‹contraction_on f A ≡ ∃α. contraction_with_on f α A›

abbreviation contraction :: ‹['a :: metric_space ⇒ 'b :: metric_space] ⇒ bool›
  where ‹contraction f ≡ contraction_on f UNIV›


lemma contraction_with_onI :
  ‹⟦0 ≤ α; α < 1; ⋀x y. ⟦x ∈ A; y ∈ A; x ≠ y; f x ≠ f y⟧ ⟹ dist (f x) (f y) ≤ α * dist x y⟧
   ⟹ contraction_with_on f α A›
  by (simp add: contraction_with_on_def lipschitz_with_onI)

lemma contraction_withI :
  ‹⟦0 ≤ α; α < 1; ⋀x y. x ≠ y ⟹ f x ≠ f y ⟹ dist (f x) (f y) ≤ α * dist x y⟧ ⟹
   contraction_with f α›
  by (rule contraction_with_onI)

lemma contraction_with_onD1 : ‹contraction_with_on f α A ⟹ 0 ≤ α›
  by (simp add: contraction_with_on_def lipschitz_with_on_def)

lemma contraction_withD1 : ‹contraction_with f α ⟹ 0 ≤ α›
  by (simp add: contraction_with_onD1)

lemma contraction_with_onD2 : ‹contraction_with_on f α A ⟹ α < 1›
  by (simp add: contraction_with_on_def lipschitz_with_on_def)

lemma contraction_withD2 : ‹contraction_with f α ⟹ α < 1›
  by (simp add: contraction_with_onD2)

lemma contraction_with_onD3 :
  ‹contraction_with_on f α A ⟹ x ∈ A ⟹ y ∈ A ⟹ dist (f x) (f y) ≤ α * dist x y›
  by (simp add: contraction_with_on_def lipschitz_with_on_def)

lemma contraction_withD3 : ‹contraction_with f α ⟹ dist (f x) (f y) ≤ α * dist x y›
  by (simp add: contraction_with_on_def lipschitz_withD2)

lemma contraction_with_imp_contraction_with_on:
  ‹contraction_with f α ⟹ contraction_with_on f α A›
  by (simp add: contraction_with_on_def lipschitz_with_imp_lipschitz_with_on)

lemma contraction_imp_contraction_on: ‹contraction f ⟹ contraction_on f A›
  using contraction_on_def contraction_with_imp_contraction_with_on by blast


lemma contraction_with_on_imp_contraction_on :
  ‹contraction_with_on f α A ⟹ contraction_on f A›
  unfolding contraction_on_def by blast

lemma contraction_with_imp_contraction: ‹contraction_with f α ⟹ contraction f›
  by (simp add: contraction_with_on_imp_contraction_on)


lemma contraction_onE:
  ‹⟦contraction_on f A; ⋀α. contraction_with_on f α A ⟹ thesis⟧ ⟹ thesis›
  unfolding contraction_on_def by blast

lemma contractionE:
  ‹⟦contraction f; ⋀α. contraction_with f α ⟹ thesis⟧ ⟹ thesis›
  by (elim contraction_onE)


lemma contraction_with_on_imp_contraction_with_on_ge :
  ‹⟦α ≤ β; β < 1; contraction_with_on f α A⟧ ⟹ contraction_with_on f β A›
  by (simp add: contraction_with_on_def lipschitz_with_on_imp_lipschitz_with_on_ge)



subsection ‹Properties›

lemma contraction_with_on_imp_lipschitz_with_on[simp] :
  ‹contraction_with_on f α A ⟹ lipschitz_with_on f α A›
  by (simp add: contraction_with_on_def)

lemma non_expanding_on_imp_lipschitz_with_one_on[simp] :
  ‹non_expanding_on f A ⟹ lipschitz_with_on f 1 A›
  by (simp add: non_expanding_on_def)

lemma contraction_on_imp_non_expanding_on[simp] :
  ‹contraction_on f A ⟹ non_expanding_on f A› 
proof (elim contraction_onE, rule non_expanding_onI)
  fix α x y assume ‹x ∈ A› and ‹y ∈ A› and contra : ‹contraction_with_on f α A›
  show ‹dist (f x) (f y) ≤ dist x y›
    by (rule order_trans[OF contra[THEN contraction_with_onD3, OF ‹x ∈ A› ‹y ∈ A›]])
      (metis contra contraction_with_on_def mult_less_cancel_right1 nle_le order_less_le zero_le_dist)
qed


lemma contraction_with_on_comp_contraction_with_on :
  ‹contraction_with_on (λx. g (f x)) (β * α) A›
  if ‹f ` A ⊆ B› ‹contraction_with_on g β B› ‹contraction_with_on f α A›
proof (unfold contraction_with_on_def, intro conjI)
  from that(2, 3)[THEN contraction_with_onD2] that(2)[THEN contraction_with_onD1]
  show ‹β * α < 1› by (metis dual_order.strict_trans2 mult_less_cancel_left1 nle_le order_less_le)
next
  show ‹lipschitz_with_on (λx. g (f x)) (β * α) A›
    by (rule lipschitz_with_on_comp_lipschitz_with_on[OF ‹f ` A ⊆ B›])
      (simp_all add: that(2, 3))
qed

corollary contraction_with_comp_contraction_with :
  ‹⟦contraction_with g β; contraction_with f α⟧ ⟹ contraction_with (λx. g (f x)) (β * α)›
  by (blast intro: contraction_with_on_comp_contraction_with_on)

corollary contraction_on_comp_contraction_on :
  ‹⟦f ` A ⊆ B; contraction_on g B; contraction_on f A⟧ ⟹ contraction_on (λx. g (f x)) A›
proof (elim contraction_onE)
  fix α β assume ‹f ` A ⊆ B› ‹contraction_with_on g β B› ‹contraction_with_on f α A›
  from contraction_with_on_comp_contraction_with_on[OF this]
  show ‹contraction_on (λx. g (f x)) A› by (fact contraction_with_on_imp_contraction_on)
qed

corollary contraction_comp_contraction :
  ‹⟦contraction g; contraction f⟧ ⟹ contraction (λx. g (f x))›
  by (blast intro: contraction_on_comp_contraction_on)


lemma contraction_with_on_comp_non_expanding_on :
  ‹contraction_with_on (λx. g (f x)) β A›
  if ‹f ` A ⊆ B› ‹contraction_with_on g β B› ‹non_expanding_on f A›
proof (unfold contraction_with_on_def, intro conjI)
  from that(2)[THEN contraction_with_onD2] show ‹β < 1› .
next
  show ‹lipschitz_with_on (λx. g (f x)) β A›
    by (rule lipschitz_with_on_comp_lipschitz_with_on[OF ‹f ` A ⊆ B›, of g β 1, simplified])
      (simp_all add: that(2, 3))
qed

corollary contraction_with_comp_non_expanding  :
  ‹⟦contraction_with g β; non_expanding f⟧ ⟹ contraction_with (λx. g (f x)) β›
  by (blast intro: contraction_with_on_comp_non_expanding_on)

corollary contraction_on_comp_non_expanding_on :
  ‹⟦f ` A ⊆ B; contraction_on g B; non_expanding_on f A⟧ ⟹ contraction_on (λx. g (f x)) A›
  by (metis contraction_on_def contraction_with_on_comp_non_expanding_on)

corollary contraction_comp_non_expanding  :
  ‹⟦contraction g; non_expanding f⟧ ⟹ contraction (λx. g (f x))›
  by (blast intro: contraction_on_comp_non_expanding_on)


lemma non_expanding_on_comp_contraction_with_on :
  ‹contraction_with_on (λx. g (f x)) α A›
  if ‹f ` A ⊆ B› ‹non_expanding_on g B› ‹contraction_with_on f α A›
proof (unfold contraction_with_on_def, intro conjI)
  from that(3)[THEN contraction_with_onD2] show ‹α < 1› .
next
  show ‹lipschitz_with_on (λx. g (f x)) α A›
    by (rule lipschitz_with_on_comp_lipschitz_with_on[OF ‹f ` A ⊆ B›, of g 1, simplified])
      (simp_all add: that(2, 3))
qed

corollary non_expanding_comp_contraction_with :
  ‹⟦non_expanding g; contraction_with f α⟧ ⟹ contraction_with (λx. g (f x)) α›
  by (blast intro: non_expanding_on_comp_contraction_with_on)

corollary non_expanding_on_comp_contraction_on :
  ‹⟦f ` A ⊆ B; non_expanding_on g B; contraction_on f A⟧ ⟹ contraction_on (λx. g (f x)) A›
  by (metis contraction_on_def non_expanding_on_comp_contraction_with_on)

corollary non_expanding_comp_contraction :
  ‹⟦non_expanding g; contraction f⟧ ⟹ contraction (λx. g (f x))›
  by (blast intro: non_expanding_on_comp_contraction_on)



subsection ‹Banach's fixed-point Theorems›

text ‹We rewrite the Banach's fixed-point theorems with our new definition.›

theorem Banach_fix_type : ‹contraction f ⟹ ∃!x. f x = x›
  for f :: ‹'a :: complete_space ⇒ 'a›
  by (elim contractionE)
    (metis banach_fix_type contraction_withD1 contraction_withD2 contraction_withD3)

theorem Banach_fix:
  ‹contraction_on f s ⟹ ∃!x. x ∈ s ∧ f x = x› if ‹complete s› ‹s ≠ {}› ‹f ` s ⊆ s›
proof (elim contraction_onE, intro banach_fix[OF ‹complete s› ‹s ≠ {}› _ _ ‹f ` s ⊆ s›] ballI)
  show ‹contraction_with_on f α s ⟹ 0 ≤ α› for α by (fact contraction_with_onD1)
next
  show ‹contraction_with_on f α s ⟹ α < 1› for α by (fact contraction_with_onD2)
next
  show ‹contraction_with_on f α s ⟹ x ∈ s ⟹ y ∈ s ⟹
        dist (f x) (f y) ≤ α * dist x y› for α x y by (fact contraction_with_onD3)
qed


(*<*)
end
  (*>*)