Theory Ultrametric_Restriction_Spaces_Locale

(***********************************************************************************
 * 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 ‹Locales factorizing the proof Work›

(*<*)
theory Ultrametric_Restriction_Spaces_Locale
  imports Restriction_Spaces.Restriction_Spaces_Locales Elementary_Ultrametric_Spaces
begin
  (*>*)

subsection ‹Preliminaries on strictly decreasing Sequences›

abbreviation strict_decseq :: ‹(nat ⇒ 'a :: order) ⇒ bool›
  where ‹strict_decseq ≡ monotone (<) (λx y. y < x)›

lemma strict_decseq_def : ‹strict_decseq X ⟷ (∀m n. m < n ⟶ X n < X m)›
  by (fact monotone_def)

lemma strict_decseqI : ‹strict_decseq X› if ‹⋀n. X (Suc n) < X n›
  by (metis Suc_le_eq decseqD decseq_Suc_iff le_less_trans nless_le strict_decseq_def that)

lemma strict_decseqD : ‹strict_decseq X ⟹ m < n ⟹ X n < X m›
  using strict_decseq_def by blast

lemma strict_decseq_def_bis : ‹strict_decseq X ⟷ (∀m n. X n < X m ⟷ m < n)›
  by (metis linorder_less_linear order_less_imp_not_less strict_decseq_def)

lemma strict_decseq_def_ter : ‹strict_decseq X ⟷ (∀m n. X n ≤ X m ⟷ m ≤ n)›
  unfolding strict_decseq_def_bis
  by (rule iffI, metis le_simps(2) order_le_less, simp add: less_le_not_le)

lemma strict_decseq_imp_decseq : ‹strict_decseq σ ⟹ decseq σ›
  by (simp add: monotone_on_def order_le_less)


lemma strict_decseq_SucI : ‹(⋀n. X (Suc n) < X n) ⟹ strict_decseq X›
  by (metis Suc_le_eq decseqD decseq_Suc_iff less_le_not_le order_less_le strict_decseq_def)

lemma strict_decseq_SucD : ‹strict_decseq A ⟹ A (Suc i) < A i›
  by (simp add: strict_decseq_def)



text ‹
Classically, a restriction space is given the structure of a metric space by defining
‹dist x y ≡ Inf {(1 / 2) ^ n| n. x ↓ n = y ↓ n}›.
This obviously also works if we replace \<^term>‹1 / 2 :: real› by any real \<^term>‹δ›
such that \<^term>‹0 < (δ :: real)› and \<^term>‹(δ :: real) < 1›.
But more generally, this still works if we set
‹dist x y ≡ Inf {σ n| n. x ↓ n = y ↓ n}› where \<^term>‹σ› is a sequence of \<^typ>‹real›
verifying \<^term>‹∀n. 0 < (σ :: nat ⇒ real) n› and \<^term>‹σ ⇢ 0›.
As you would expect, the more structure you have, the more powerful theorems you get.
We explore all these variants in the theory below.
›

subsection ‹The Construction with Locales›

text ‹Our formalization will extend the class \<^class>‹metric_space›.
      But some proofs are redundant, especially when it comes to the product type.
      So first we will be working with locales, and interpret them with the classes.›

locale NonDecseqRestrictionSpace = PreorderRestrictionSpace +
  ―‹Factorization of the proof work.›
  fixes M :: ‹'a set› and restriction_σ :: ‹nat ⇒ real› (‹σ⇩↓›)
    and restriction_dist :: ‹'a ⇒ 'a ⇒ real› (‹dist⇩↓›)
  assumes restriction_σ_tendsto_zero : ‹restriction_σ ⇢ 0›
    and zero_less_restriction_σ [simp] : ‹0 < restriction_σ n›
    and dist_restriction_is :
    ‹dist⇩↓ x y = (INF n ∈ restriction_related_set x y. restriction_σ n)›
begin

lemma zero_le_restriction_σ [simp] : ‹0 ≤ σ⇩↓ n› 
  by (simp add: order_less_imp_le)

lemma restriction_σ_neq_zero [simp] : ‹σ⇩↓ n ≠ 0› 
  by (metis zero_less_restriction_σ order_less_irrefl)


(* lemma eventually_inf_to:
  ‹r ⇢ k ⟹ ∀e>0. k ∈ ball k (k + e) ⟶ (∀⇩F n in sequentially. r n ∈ ball k (k + e))›
  unfolding eventually_sequentially inj_on_def
  using lim_explicit by blast *)


lemma bounded_range_restriction_σ: ‹bounded (range σ⇩↓)›
  by (fact convergent_imp_bounded[OF restriction_σ_tendsto_zero])

abbreviation restriction_σ_related_set :: ‹'a ⇒ 'a ⇒ real set›
  where ‹restriction_σ_related_set x y ≡ σ⇩↓ ` restriction_related_set x y›

abbreviation restriction_σ_not_related_set :: ‹'a ⇒ 'a ⇒ real set›
  where ‹restriction_σ_not_related_set x y ≡ σ⇩↓ ` restriction_not_related_set x y›

lemma nonempty_restriction_σ_related_set :
  ‹restriction_σ_related_set x y ≠ {}› by simp

lemma restriction_σ_related_set_Un_restriction_σ_not_related_set :
  ‹restriction_σ_related_set x y ∪ restriction_σ_not_related_set x y = range σ⇩↓›
  by blast

lemma ‹bdd_above (restriction_σ_related_set x y)›
  by (meson bdd_above.I2 bdd_above.unfold bounded_imp_bdd_above
      bounded_range_restriction_σ rangeI)

lemma ‹bdd_above (restriction_σ_not_related_set x y)›
  by (meson bdd_above.E bdd_above.I2 bounded_imp_bdd_above
      bounded_range_restriction_σ range_eqI)

lemma bounded_restriction_σ_related_set: ‹bounded (restriction_σ_related_set x y)›
  by (meson bounded_range_restriction_σ bounded_subset image_mono top_greatest)

lemma bounded_restriction_σ_not_related_set: ‹bounded (restriction_σ_not_related_set x y)›
  by (meson bounded_range_restriction_σ bounded_subset image_mono subset_UNIV)

corollary restriction_space_Inf_properties:
  ‹a ∈ restriction_σ_related_set x y ⟹ dist⇩↓ x y ≤ a›
  ‹⟦⋀a. a ∈ restriction_σ_related_set x y ⟹ b ≤ a⟧ ⟹ b ≤ dist⇩↓ x y›
  unfolding dist_restriction_is
  by (simp_all add: bounded_has_Inf(1) bounded_restriction_σ_related_set cInf_greatest)

lemma restriction_σ_related_set_alt :
  ‹restriction_σ_related_set x y = {σ⇩↓ n| n. n ∈ restriction_related_set x y}›
  by blast


lemma exists_less_restriction_σ : ‹∃n. m < n ∧ σ⇩↓ n < σ⇩↓ m›
proof (rule ccontr)
  assume ‹¬ (∃n>m. σ⇩↓ n < σ⇩↓ m)›
  hence ‹∀n≥m. σ⇩↓ m ≤ σ⇩↓ n›
    by (metis linorder_not_le nle_le)
  hence ‹¬ σ⇩↓ ⇢ 0›
    by (meson Lim_bounded2 linorder_not_le zero_less_restriction_σ)
  with restriction_σ_tendsto_zero show False by simp
qed


lemma ‹dist⇩↓ x y = Inf (restriction_σ_related_set x y)›
  by (fact dist_restriction_is)


lemma not_related_imp_dist_restriction_is_some_restriction_σ :
  ‹∃n. dist⇩↓ x y = σ⇩↓ n ∧ (∀m≤n. x ↓ m ⪅ y ↓ m) › if ‹¬ x ⪅ y›
proof -
  have ‹finite (restriction_related_set x y)›
    by (simp add: finite_restriction_related_set_iff ‹¬ x ⪅ y›)
  have ‹Inf (restriction_σ_related_set x y) ∈ restriction_σ_related_set x y›
    by (rule closed_contains_Inf[OF nonempty_restriction_σ_related_set])
      (simp_all add: ‹finite (restriction_related_set x y)› finite_imp_closed)
  hence ‹dist⇩↓ x y ∈ restriction_σ_related_set x y›
    by (fold dist_restriction_is)
  with restriction_related_le obtain n
    where ‹n ∈ restriction_related_set x y› ‹dist⇩↓ x y = σ⇩↓ n›
      ‹∀m≤n. x ↓ m ⪅ y ↓ m›  by blast
  with ‹dist⇩↓ x y ∈ restriction_σ_related_set x y› show ?thesis by blast
qed


lemma not_related_imp_dist_restriction_le_some_restriction_σ :
  ‹¬ x ⪅ y ⟹ ∃n. dist⇩↓ x y ≤ σ⇩↓ n ∧ (¬ x ↓ Suc n ⪅ y ↓ Suc n) ∧ (∀m≤n. x ↓ m ⪅ y ↓ m)›
  by (blast intro: restriction_space_Inf_properties
      dest: ex_not_restriction_related_optimized)


lemma restriction_dist_eq_0_iff_related : ‹dist⇩↓ x y = 0 ⟷ x ⪅ y›
proof (rule iffI)
  show ‹dist⇩↓ x y = 0 ⟹ x ⪅ y›
    by (erule contrapos_pp)
      (auto dest: not_related_imp_dist_restriction_is_some_restriction_σ)
next
  show ‹dist⇩↓ x y = 0› if ‹x ⪅ y›
  proof (rule order_antisym)
    show ‹0 ≤ dist⇩↓ x y› by (simp add: cINF_greatest dist_restriction_is)
  next
    define Δ where ‹Δ n ≡ - σ⇩↓ n› for n
    have * : ‹Δ n ≤ - dist⇩↓ x y› for n
      unfolding Δ_def using ‹x ⪅ y› restriction_space_Inf_properties(1)
      by simp (metis UNIV_restriction_related_set_iff rangeI)
    from restriction_σ_tendsto_zero tendsto_minus_cancel_left
    have ‹Δ ⇢ 0› unfolding Δ_def by force
    from lim_le[OF convergentI[OF ‹Δ ⇢ 0›] "*"] limI[OF ‹Δ ⇢ 0›]
    show ‹dist⇩↓ x y ≤ 0› by simp
  qed
qed


end


locale DecseqRestrictionSpace = NonDecseqRestrictionSpace +
  assumes decseq_restriction_σ : ‹decseq σ⇩↓›
begin

lemma dist_restriction_is_bis :
  ‹dist⇩↓ x y = (if x ⪅ y then 0 else σ⇩↓ (Sup (restriction_related_set x y)))›
  if ‹x ∈ M› and ‹y ∈ M›
proof (split if_split, intro conjI impI)
  from ‹x ∈ M› and ‹y ∈ M› show ‹x ⪅ y ⟹ restriction_dist x y = 0›
    by (simp add: restriction_dist_eq_0_iff_related)
next
  show ‹dist⇩↓ x y = σ⇩↓ (Sup (restriction_related_set x y))› if ‹¬ x ⪅ y›
  proof (rule order_antisym)
    show ‹dist⇩↓ x y ≤ σ⇩↓ (Sup (restriction_related_set x y))›
      unfolding dist_restriction_is
      by (rule cINF_lower[OF _ Sup_in_restriction_related_set[OF ‹¬ x ⪅ y›]])
        (meson bdd_below.I2 zero_le_restriction_σ)
  next
    show ‹σ⇩↓ (Sup (restriction_related_set x y)) ≤ dist⇩↓ x y›
    proof (unfold dist_restriction_is, rule cINF_greatest)
      show ‹restriction_related_set x y ≠ {}› by (fact nonempty_restriction_related_set)
    next
      fix n assume ‹n ∈ restriction_related_set x y›
      hence ‹n ≤ Sup (restriction_related_set x y)›
        by (metis ‹n ∈ restriction_related_set x y› le_cSup_finite
            finite_restriction_related_set_iff ‹¬ x ⪅ y›)
      from decseqD[OF decseq_restriction_σ this]
      show ‹restriction_σ (Sup (restriction_related_set x y)) ≤ restriction_σ n› .
    qed
  qed
qed


lemma not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq :
  ‹dist⇩↓ x y = σ⇩↓ (Sup (restriction_related_set x y))›
  ‹∀m≤Sup (restriction_related_set x y). x ↓ m ⪅ y ↓ m›
  ‹∀m>Sup (restriction_related_set x y). ¬ x ↓ m ⪅ y ↓ m›
  if ‹¬ x ⪅ y› and ‹x ∈ M› and ‹y ∈ M›
  subgoal by (subst dist_restriction_is_bis; simp add: ‹¬ x ⪅ y› ‹x ∈ M› ‹y ∈ M›)
  subgoal using Sup_in_restriction_related_set[OF ‹¬ x ⪅ y›] restriction_related_le by blast
  using cSup_upper[OF _ bdd_above_restriction_related_set_iff[THEN iffD2, OF ‹¬ x ⪅ y›],
      of ‹Suc (Sup (restriction_related_set x y))›]
  by (metis (mono_tags, lifting) Suc_leI dual_order.refl mem_Collect_eq not_less_eq_eq restriction_related_le)



theorem restriction_dist_tendsto_zero_independent_of_restriction_σ :
  ―‹Very powerful theorem: the convergence of the distance to \<^term>‹0 :: real›
     is actually independent from the restriction sequence chosen.›
  ―‹This is the theorem for which we had to work with locales first.›

assumes ‹DecseqRestrictionSpace (↓) (⪅) restriction_σ' restriction_dist'›
  and ‹Σ ∈ M› and ‹range σ ⊆ M›
shows ‹(λn. dist⇩↓ (σ n) Σ) ⇢ 0 ⟷ (λn. restriction_dist' (σ n) Σ) ⇢ 0›
proof -
  { fix restriction_σ restriction_dist restriction_σ' restriction_dist'
    assume a1 : ‹DecseqRestrictionSpace (↓) (⪅) restriction_σ  restriction_dist ›
      and a2 : ‹DecseqRestrictionSpace (↓) (⪅) restriction_σ' restriction_dist'›
      and  * : ‹(λn. restriction_dist (σ n) Σ) ⇢ 0›

    interpret i1 : DecseqRestrictionSpace ‹(↓)› ‹(⪅)› M restriction_σ  restriction_dist  by (fact a1)
    interpret i2 : DecseqRestrictionSpace ‹(↓)› ‹(⪅)› M restriction_σ' restriction_dist' by (fact a2)



    have ‹(λn. restriction_dist' (σ n) Σ) ⇢ 0›
    proof (rule metric_LIMSEQ_I)
      fix ε :: real assume ‹0 < ε›

      from metric_LIMSEQ_D[OF i2.restriction_σ_tendsto_zero ‹0 < ε›]
      obtain N where ** : ‹N ≤ n ⟹ restriction_σ' n < ε› for n by auto

      fix N' :: nat

      have ‹∃N'. ∀n≥N'. N ∈ restriction_related_set (σ n) Σ›
      proof (rule ccontr)
        assume ‹∄N'. ∀n≥N'. N ∈ restriction_related_set (σ n) Σ›
        hence *** : ‹∀N'. ∃n≥N'. ¬ σ n ↓ N ⪅ Σ ↓ N› by simp
        have **** : ‹∀N'. ∃n≥N'. restriction_σ N ≤ restriction_dist (σ n) Σ›
        proof (rule allI)
          fix N' :: nat
          from "***" obtain n where ‹N' ≤ n› ‹¬ σ n ↓ N ⪅ Σ ↓ N› by blast
          hence ‹¬ σ n ⪅ Σ› using mono_restriction_related by blast
          have ‹restriction_σ N ≤ restriction_dist (σ n) Σ›
          proof (subst i1.dist_restriction_is_bis)
            show ‹σ n ∈ M› ‹Σ ∈ M›
              by (simp_all add: assms(2, 3) range_subsetD)
          next
            show ‹restriction_σ N ≤ (if σ n ⪅ Σ then 0
                  else restriction_σ (Sup (restriction_related_set (σ n) Σ)))›
              using ‹¬ σ n ⪅ Σ› ‹¬ σ n ↓ N ⪅ Σ ↓ N› assms(2, 3) nle_le
                not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq(2)
              by (fastforce intro: decseqD[OF i1.decseq_restriction_σ])
          qed
          with ‹N' ≤ n› show ‹∃n≥N'. restriction_σ N ≤ restriction_dist (σ n) Σ› by blast
        qed
        from metric_LIMSEQ_D[OF "*", of ‹restriction_σ N›]
        have ‹∃N''. ∀n≥N''. restriction_dist (σ n) Σ < restriction_σ N›
          by (metis abs_of_nonneg i1.zero_le_restriction_σ i1.zero_less_restriction_σ norm_conv_dist order_trans real_norm_def
              verit_comp_simplify1(3))
        with "****" show False by fastforce
      qed

      then obtain N' where *** : ‹N' ≤ n ⟹ N ∈ restriction_related_set (σ n) Σ› for n by blast
      have ‹restriction_dist' (σ n) Σ < ε› if ‹N' ≤ n› for n
      proof (rule le_less_trans[OF i2.restriction_space_Inf_properties(1), of ‹restriction_σ' N›])
        from ‹N' ≤ n› "***"
        show ‹restriction_σ' N ∈ i2.restriction_σ_related_set (σ n) Σ› by blast
      next
        show ‹restriction_σ' N < ε› by (simp add: "**")
      qed
      thus ‹∃N. ∀n≥N. dist (restriction_dist' (σ n) Σ) 0 < ε›
        by (metis abs_of_nonneg dist_0_norm dist_commute i2.not_related_imp_dist_restriction_is_some_restriction_σ
            i2.restriction_dist_eq_0_iff_related i2.zero_less_restriction_σ order_less_imp_not_less real_norm_def
            verit_comp_simplify1(3))
    qed }
  note * = this

  show ‹(λn. dist⇩↓ (σ n) Σ) ⇢ 0 = (λn. restriction_dist' (σ n) Σ) ⇢ 0›
    using "*" DecseqRestrictionSpace_axioms assms(1) by blast
qed

end


(*<*)
end
  (*>*)