From bd134cea871d94932ca1f7c369f4e8c3debf4979 Mon Sep 17 00:00:00 2001 From: Chenghui Weng <144981080+weng-chenghui@users.noreply.github.com> Date: Thu, 22 Oct 2026 21:44:11 +0900 Subject: [PATCH] Add negligible sequences and harmonic Lipschitz characterization --- CHANGELOG_UNRELEASED.md | 14 ++ _CoqProject | 2 + theories/Make | 2 + theories/all_analysis.v | 2 + theories/negligible_seq.v | 163 ++++++++++++++++++++++ theories/negligible_seq_harmonic.v | 208 +++++++++++++++++++++++++++++ 6 files changed, 391 insertions(+) create mode 100644 theories/negligible_seq.v create mode 100644 theories/negligible_seq_harmonic.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6e327b2b46..ef10363857 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -151,6 +151,20 @@ + lemmas `cstMcounting_esum`, `sintegral_counting_esum`, `integral_countingT_esum`, `integral_counting_esum` +- new file `negligible_seq.v`: + + definition `negligible_seq` + + lemmas `negligible_seq_cvgP`, `negligible_seq_submod_closed`, + `le_negligible_seq`, `negligible_seq_eqoP`, `negligible_seqXnM`, + `negligible_seqV`, `negligible_seq_exprnN` + +- new file `negligible_seq_harmonic.v`: + + definitions `harmonic_coord`, `harmonic_dist`, `extend_infty`, + `lipschitz_at_infty`, `harmonic_lipschitz` + + lemmas `harmonic_distxx`, `harmonic_dist_infty`, `lipschitz_at_inftyP`, + `lipschitz_at_infty_le`, `negligible_seq_lipschitz_at_inftyP`, + `harmonic_dist_ge_inv`, `harmonic_lipschitzW`, + `lipschitz_at_inftyS_harmonic`, `negligible_seq_harmonic_lipschitzP` + ### Changed - in `esum.v`: diff --git a/_CoqProject b/_CoqProject index 26a7e4faa9..559d79a57b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -94,6 +94,8 @@ theories/normedtype_theory/normedtype.v theories/functional_analysis/hahn_banach_theorem.v theories/sequences.v +theories/negligible_seq.v +theories/negligible_seq_harmonic.v theories/realfun.v theories/exp.v diff --git a/theories/Make b/theories/Make index adca81b9dd..f0d6196e58 100644 --- a/theories/Make +++ b/theories/Make @@ -62,6 +62,8 @@ functional_analysis/hahn_banach_theorem.v realfun.v sequences.v +negligible_seq.v +negligible_seq_harmonic.v exp.v elementary_functions/trigonometry_functions.v diff --git a/theories/all_analysis.v b/theories/all_analysis.v index 1e55428254..78f0314ca4 100644 --- a/theories/all_analysis.v +++ b/theories/all_analysis.v @@ -5,6 +5,8 @@ From mathcomp Require Export cantor. From mathcomp Require Export normedtype. From mathcomp Require Export realfun. From mathcomp Require Export sequences. +From mathcomp Require Export negligible_seq. +From mathcomp Require Export negligible_seq_harmonic. From mathcomp Require Export exp. From mathcomp Require Export trigo. From mathcomp Require Export esum. diff --git a/theories/negligible_seq.v b/theories/negligible_seq.v new file mode 100644 index 0000000000..4ce59627f7 --- /dev/null +++ b/theories/negligible_seq.v @@ -0,0 +1,163 @@ +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import boot order algebra. +From mathcomp Require Import boolp classical_sets functions. +From mathcomp Require Import topology normedtype landau. + +(**md**************************************************************************) +(* # Negligible sequences *) +(* *) +(* A sequence is negligible when its absolute value is eventually below every *) +(* inverse power of the index. Negligible sequences form a submodule of the *) +(* sequences. *) +(* *) +(* Reference: *) +(* - J. Katz, Y. Lindell. Introduction to Modern Cryptography, 2nd edition. *) +(* CRC Press, 2015. Definition 3.4. *) +(* *) +(* ``` *) +(* negligible_seq == predicate of the sequences u : R ^nat such that for *) +(* every c, `|u n| < n%:R ^- c for n large enough *) +(* ``` *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section negligible_seq_pred. +Context {R : archiRealFieldType}. + +Definition negligible_seq : {pred R ^nat} := + mem [set u | forall c : nat, \forall n \near \oo, `|u n| < n%:R ^- c]. +Definition negligible_seq_key : pred_key negligible_seq. +Proof. exact. Qed. +Canonical negligible_seq_keyed := KeyedPred negligible_seq_key. + +End negligible_seq_pred. + +Section negligible_seq. +Context {R : archiRealFieldType}. +Implicit Types u v : R ^nat. + +Lemma negligible_seq_cvgP u : u \in negligible_seq <-> + forall c : nat, (fun n => n%:R ^+ c * u n) @ \oo --> 0. +Proof. +split=> [/set_mem un c|un]. + apply/cvgr0Pnorm_lt => e e_gt0; near=> n. + have n_gt0 : (0 < n)%N by near: n; exact: nbhs_infty_gt. + rewrite normrM normrX normr_nat. + have : `|u n| < n%:R ^- c.+1 by near: n; exact: un. + rewrite -(ltr_pM2l (_ : 0 < n%:R ^+ c)) ?exprn_gt0 ?ltr0n // exprSr invfM. + rewrite mulVKf ?expf_neq0 ?pnatr_eq0 -?lt0n // => /lt_trans; apply. + rewrite -[e]invrK ltf_pV2 ?posrE ?ltr0n ?invr_gt0 //. + by near: n; exact: nbhs_infty_gtr. +apply/mem_set => c; near=> n. +have n_gt0 : (0 < n)%N by near: n; exact: nbhs_infty_gt. +have : `|n%:R ^+ c * u n| < 1. + by near: n; apply: (cvgr0Pnorm_lt _).1 ltr01; exact: un. +by rewrite normrM normrX normr_nat -ltr_pdivlMl ?exprn_gt0 ?ltr0n ?mulr1. +Unshelve. all: by end_near. Qed. + +Lemma negligible_seq_submod_closed : submod_closed (@negligible_seq R). +Proof. +split=> [|a u v /negligible_seq_cvgP un /negligible_seq_cvgP vn]. + apply/negligible_seq_cvgP => c. + by under eq_fun do rewrite /= mulr0; exact: cvg_cst. +apply/negligible_seq_cvgP => c; under eq_fun do rewrite /= mulrDr mulrCA. +rewrite -(addr0 0) -{1}(mulr0 a); apply: cvgD (vn c). +by apply: cvgM; [exact: cvg_cst|exact: un]. +Qed. + +HB.instance Definition _ := + GRing.isSubmodClosed.Build _ _ negligible_seq negligible_seq_submod_closed. + +Lemma le_negligible_seq u v : + (\forall n \near \oo, `|u n| <= `|v n|) -> + v \in negligible_seq -> u \in negligible_seq. +Proof. +move=> uv /set_mem vn; apply/mem_set => c. +by apply: filterS2 uv (vn c) => n; exact: le_lt_trans. +Qed. + +Lemma negligible_seq_eqoP u : + u \in negligible_seq <-> forall c : nat, u =o_\oo (fun n => n%:R ^- c : R). +Proof. +split=> [/negligible_seq_cvgP un c|uo]. + apply/eqoP => e e_gt0; near=> n. + have n_gt0 : (0 < n)%N by near: n; exact: nbhs_infty_gt. + have : `|n%:R ^+ c * u n| < e. + by near: n; apply: (cvgr0Pnorm_lt _).1 e_gt0; exact: un. + rewrite normrM normrX normr_nat normfV normrX normr_nat. + by rewrite ler_pdivlMr ?exprn_gt0 ?ltr0n // mulrC => /ltW. +apply/mem_set => c; near=> n. +have n_gt0 : (0 < n)%N by near: n; exact: nbhs_infty_gt. +have : `|u n| <= 2^-1 * `|n%:R ^- c : R|. + by near: n; apply: (eqoP _ _ _).1 (uo c) _ _; rewrite invr_gt0 ltr0n. +rewrite normfV normrX normr_nat => /le_lt_trans; apply. +by rewrite gtr_pMl ?invf_lt1 ?ltr1n // invr_gt0 exprn_gt0 ?ltr0n. +Unshelve. all: by end_near. Qed. + +Lemma negligible_seqXnM u d : + u \in negligible_seq -> (fun n => n%:R ^+ d * u n) \in negligible_seq. +Proof. +move=> /negligible_seq_cvgP un; apply/negligible_seq_cvgP => c. +by under eq_fun do rewrite mulrA -exprD; exact: un. +Qed. + +Let exp2_gt_linear (c k : nat) : (c * c + c <= k)%N -> (c * k.+1 < 2 ^ k)%N. +Proof. +move=> k_ge; have [d kE] : exists d, k = (c + d)%N. + by exists (k - c)%N; rewrite subnKC // (leq_trans _ k_ge) // leq_addl. +have cc_le : (c * c <= d)%N by move: k_ge; rewrite kE addnC leq_add2l. +rewrite kE; apply: leq_trans (_ : c.+1 * d.+1 <= _)%N; last first. + by rewrite expnD leq_mul // ltn_expl. +by rewrite mulnS mulnDr mulSn mulnS addnA addnA ltn_add2r addnC ltn_add2r ltnS. +Qed. + +Let exp2_gt_monomial (c n : nat) : + (2 ^ (c * c + c) <= n)%N -> (n ^ c < 2 ^ n)%N. +Proof. +move=> n_ge; have n_gt0 : (0 < n)%N by rewrite (leq_trans _ n_ge) // expn_gt0. +move: n_ge; case: c => [_|c n_ge]. + by rewrite expn0 -{1}(expn0 2) ltn_exp2l. +set k := trunc_log 2 n. +have k_ge : (c.+1 * c.+1 + c.+1 <= k)%N by apply: trunc_log_max. +apply: leq_ltn_trans (_ : 2 ^ (c.+1 * k.+1) < _)%N. + by rewrite mulnC expnM leq_exp2r // ltnW // trunc_log_ltn. +rewrite ltn_exp2l //. +by apply: leq_trans (exp2_gt_linear k_ge) (trunc_logP _ _). +Qed. + +Lemma negligible_seqV v : + (forall c : nat, \forall n \near \oo, n%:R ^+ c <= v n) -> + (fun n => (v n)^-1) \in negligible_seq. +Proof. +move=> v_ge; apply/mem_set => c; near=> n. +have n_gt1 : (1 < n)%N by near: n; exact: nbhs_infty_gt. +have Xn_gt0 k : 0 < n%:R ^+ k :> R by rewrite exprn_gt0 // ltr0n ltnW. +have vn : n%:R ^+ c.+1 <= v n by near: n; exact: v_ge. +have vn_gt0 := lt_le_trans (Xn_gt0 _) vn. +rewrite normfV gtr0_norm // (@le_lt_trans _ _ (n%:R ^- c.+1)) //. + by rewrite lef_pV2 ?posrE. +by rewrite ltf_pV2 ?posrE ?ltr_eXn2l ?ltr1n. +Unshelve. all: by end_near. Qed. + +Lemma negligible_seq_exprnN (p : nat) : (1 < p)%N -> + (fun n => p%:R ^- n : R) \in negligible_seq. +Proof. +move=> p_gt1; apply: negligible_seqV => c; near=> n. +rewrite -natrX -natrX ler_nat. +rewrite (leq_trans (ltnW (exp2_gt_monomial _))) ?leq_exp2r //. + by near: n; exact: nbhs_infty_ge. +by near: n; exact: nbhs_infty_gt. +Unshelve. all: by end_near. Qed. + +End negligible_seq. diff --git a/theories/negligible_seq_harmonic.v b/theories/negligible_seq_harmonic.v new file mode 100644 index 0000000000..44830e70d9 --- /dev/null +++ b/theories/negligible_seq_harmonic.v @@ -0,0 +1,208 @@ +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import boot order algebra. +From mathcomp Require Import boolp classical_sets functions. +From mathcomp Require Import topology normedtype landau. +From mathcomp Require Import negligible_seq. + +(**md**************************************************************************) +(* # Negligible sequences and the harmonic metric *) +(* *) +(* The index of a sequence is read as a point of the one-point *) +(* compactification of the natural numbers, with None the point at infinity. *) +(* At exponent c the index n has the coordinate n ^- c and the point at *) +(* infinity the coordinate 0; the distance of two points is the distance of *) +(* their coordinates. A sequence is negligible iff its extension by 0 at *) +(* infinity is Lipschitz at infinity for every exponent, and iff it is *) +(* Lipschitz for every positive exponent. Both conditions exclude Some 0. *) +(* *) +(* The distance is a pseudometric only: for c > 0, index 0 has coordinate *) +(* 0 ^- c = 0 of the point at infinity, and at c = 0 every index has the *) +(* coordinate 1. The Lipschitz conditions therefore exclude the index 0, and *) +(* the second characterization ranges over positive exponents. *) +(* *) +(* ``` *) +(* harmonic_coord c x == n ^- c if x is Some n, 0 if x is None *) +(* harmonic_dist c x y == `|harmonic_coord c x - harmonic_coord c y| *) +(* extend_infty u == the extension of u : R ^nat to option nat by *) +(* 0 at None *) +(* lipschitz_at_infty c u == there is L such that `|u n| <= L * n ^- c *) +(* for every positive n *) +(* harmonic_lipschitz c u == extend_infty u is Lipschitz for *) +(* harmonic_dist c on the points other than *) +(* Some 0 *) +(* ``` *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section harmonic_dist. +Context {R : archiRealFieldType}. +Implicit Types (c : nat) (x y z : option nat) (u : R ^nat). + +Definition harmonic_coord c x : R := if x is Some n then n%:R ^- c else 0. + +Definition harmonic_dist c x y : R := + `|harmonic_coord c x - harmonic_coord c y|. + +Lemma harmonic_distxx c x : harmonic_dist c x x = 0. +Proof. by rewrite /harmonic_dist subrr normr0. Qed. + +Lemma harmonic_dist_infty c n : harmonic_dist c (Some n) None = n%:R ^- c. +Proof. by rewrite /harmonic_dist /= subr0 ger0_norm // invr_ge0 exprn_ge0. Qed. + +Definition extend_infty u x : R := if x is Some n then u n else 0. + +End harmonic_dist. + +Section lipschitz_at_infty. +Context {R : archiRealFieldType}. +Implicit Types (c d m n : nat) (u : R ^nat). + +Let inv_expn_le_base k (a b : R) : 0 < a -> a <= b -> b ^- k <= a ^- k. +Proof. +move=> a_gt0 ab; have b_gt0 := lt_le_trans a_gt0 ab. +by rewrite lef_pV2 ?posrE ?exprn_gt0 // lerXn2r // nnegrE; exact: ltW. +Qed. + +Let inv_expn_le_exponent c d n : + (0 < n)%N -> (c <= d)%N -> n%:R ^- d <= n%:R ^- c :> R. +Proof. +move=> n_gt0 cd. +by rewrite lef_pV2 ?posrE ?exprn_gt0 ?ltr0n // ler_weXn2l // ler1n. +Qed. + +(* The extension of u by 0 is Lipschitz at the point at infinity for + harmonic_dist c, with the index 0 excluded. *) +Definition lipschitz_at_infty c u : Prop := + exists L : R, forall n, (0 < n)%N -> `|u n| <= L * n%:R ^- c. + +Let lipschitz_const_ge0 c u (L : R) : + (forall n, (0 < n)%N -> `|u n| <= L * n%:R ^- c) -> 0 <= L. +Proof. by move/(_ 1%N isT); rewrite expr1n invr1 mulr1; exact: le_trans. Qed. + +Lemma lipschitz_at_inftyP c u : lipschitz_at_infty c u <-> + exists L : R, forall x, x != Some 0%N -> + `|extend_infty u x - extend_infty u None| <= L * harmonic_dist c x None. +Proof. +split=> -[L uL]; exists L. + case=> [[|n]|] //= _; first by rewrite subr0 harmonic_dist_infty; exact: uL. + by rewrite subrr normr0 harmonic_distxx mulr0. +move=> n n_gt0; have := uL (Some n); rewrite /= subr0 harmonic_dist_infty. +by apply; rewrite -lt0n. +Qed. + +Lemma lipschitz_at_infty_le c d u : + (c <= d)%N -> lipschitz_at_infty d u -> lipschitz_at_infty c u. +Proof. +move=> cd [L uL]; exists L => n n_gt0; apply: le_trans (uL n n_gt0) _. +by rewrite ler_wpM2l ?(lipschitz_const_ge0 uL) ?inv_expn_le_exponent. +Qed. + +Lemma negligible_seq_lipschitz_at_inftyP u : + u \in negligible_seq <-> forall c, lipschitz_at_infty c u. +Proof. +split=> [/set_mem un c|un]. + have [N _ uN] := un c. + pose M := \big[maxr/0]_(i < N) (`|u i| * i%:R ^+ c). + exists (maxr 1 M) => n n_gt0. + have [Nn|nN] := leqP N n. + apply/ltW/(lt_le_trans (uN n Nn)). + by rewrite ler_peMl ?invr_ge0 ?exprn_ge0 // le_max lexx. + rewrite ler_pdivlMr ?exprn_gt0 ?ltr0n // le_max. + by rewrite (le_bigmax _ _ (Ordinal nN)) orbT. +apply/mem_set => c; have [L uL] := un c.+1. +have L_ge0 := lipschitz_const_ge0 uL; near=> n. +have n_gt0 : (0 < n)%N by near: n; exact: nbhs_infty_gt. +apply: le_lt_trans (uL n n_gt0) _. +rewrite exprS invfM mulrA gtr_pMl ?invr_gt0 ?exprn_gt0 ?ltr0n //. +rewrite ltr_pdivrMr ?ltr0n // mul1r; apply: lt_le_trans (archi_boundP L_ge0) _. +by rewrite ler_nat; near: n; exact: nbhs_infty_ge. +Unshelve. all: by end_near. Qed. + +(* The extension of u by 0 is Lipschitz for harmonic_dist c on the points + other than the index 0, whose coordinate is that of the point at + infinity when c is positive. *) +Definition harmonic_lipschitz c u : Prop := + exists L : R, forall x y, x != Some 0%N -> y != Some 0%N -> + `|extend_infty u x - extend_infty u y| <= L * harmonic_dist c x y. + +Lemma harmonic_dist_ge_inv c m n : (0 < c)%N -> (0 < m)%N -> (m < n)%N -> + m%:R ^- c.+1 <= 2 * harmonic_dist c (Some m) (Some n) :> R. +Proof. +case: c => // c _ m_gt0 mn. +have mR_gt0 : 0 < m%:R :> R by rewrite ltr0n. +have dmn_ge0 : 0 <= m%:R ^- c.+1 - n%:R ^- c.+1 :> R. + by rewrite subr_ge0 inv_expn_le_base // ler_nat; exact: ltnW. +rewrite /harmonic_dist /= ger0_norm //. +pose a : R := m%:R; pose b : R := m.+1%:R. +have b_gt0 : 0 < b by rewrite ltr0n. +have a_neq0 := lt0r_neq0 mR_gt0; have b_neq0 := lt0r_neq0 b_gt0. +apply: le_trans (_ : _ <= 2 * (a ^- c.+1 - a ^- c / b)) _. + rewrite 2!exprSr 2!invfM -mulrBr mulrCA -mulrA. + rewrite ler_pM2l ?invr_gt0 ?exprn_gt0 //. + have -> : a^-1 - b^-1 = a^-1 / b. + apply: (mulIf b_neq0); rewrite mulfVK // mulrBl mulVf //. + by rewrite /b -addn1 natrD mulrDr mulVf // mulr1 addrC addKr. + rewrite mulrCA ler_pM2l ?invr_gt0 // ler_pdivlMr // mulrC ler_pdivrMr //. + by rewrite -natrM ler_nat mul2n -addnn -addn1 leq_add2l. +have bn : b <= n%:R by rewrite ler_nat. +rewrite ler_pM2l // lerB // (le_trans (inv_expn_le_base _ b_gt0 bn)) //. +rewrite exprSr invfM ler_pM2r ?invr_gt0 //. +by rewrite inv_expn_le_base // ler_nat. +Qed. + +Lemma harmonic_lipschitzW c u : + harmonic_lipschitz c u -> lipschitz_at_infty c u. +Proof. +by move=> [L uL]; apply/lipschitz_at_inftyP; exists L => x x_neq0; exact: uL. +Qed. + +Lemma lipschitz_at_inftyS_harmonic c u : + (0 < c)%N -> lipschitz_at_infty c.+1 u -> harmonic_lipschitz c u. +Proof. +move=> c_gt0 [L uL]; have L_ge0 := lipschitz_const_ge0 uL. +have uL4 n : (0 < n)%N -> `|u n| <= 4 * L * n%:R ^- c. + move=> n_gt0; apply: le_trans (uL n n_gt0) _. + by rewrite ler_pM ?invr_ge0 ?exprn_ge0 ?ler_peMl ?ler1n ?inv_expn_le_exponent. +have uLlt m n : (0 < m)%N -> (m < n)%N -> + `|u m - u n| <= 4 * L * harmonic_dist c (Some m) (Some n). + move=> m_gt0 mn; have n_gt0 := ltn_trans m_gt0 mn. + apply: le_trans (ler_normB _ _) _. + apply: le_trans (lerD (uL m m_gt0) (uL n n_gt0)) _. + apply: le_trans (_ : _ <= 2 * L * m%:R ^- c.+1) _. + rewrite -mulrA mulr2n mulrDl mul1r lerD2l ler_wpM2l //. + by rewrite inv_expn_le_base ?ltr0n // ler_nat; exact: ltnW. + have -> : 4 * L = 2 * L * 2 by rewrite mulrAC -natrM. + rewrite -[_ * 2 * _]mulrA ler_wpM2l ?mulr_ge0 //. + exact: harmonic_dist_ge_inv. +exists (4 * L) => -[[|m]|] [[|n]|] //= _ _. +- have [mn|nm|->] := ltngtP m n. + + exact: uLlt. + + by rewrite distrC /harmonic_dist [X in _ <= 4 * L * X]distrC uLlt. + + by rewrite subrr normr0 harmonic_distxx mulr0. +- by rewrite subr0 harmonic_dist_infty uL4. +- rewrite sub0r normrN /harmonic_dist /= sub0r normrN. + rewrite [X in _ <= 4 * L * X]ger0_norm ?invr_ge0 ?exprn_ge0 //. + exact: uL4. +- by rewrite subrr normr0 harmonic_distxx mulr0. +Qed. + +Lemma negligible_seq_harmonic_lipschitzP u : + u \in negligible_seq <-> forall c, (0 < c)%N -> harmonic_lipschitz c u. +Proof. +apply: iff_trans (negligible_seq_lipschitz_at_inftyP u) _. +split=> uL c; first by move=> c_gt0; exact: lipschitz_at_inftyS_harmonic. +exact: lipschitz_at_infty_le (leqnSn c) (harmonic_lipschitzW (uL c.+1 isT)). +Qed. + +End lipschitz_at_infty.