Library Lebesgue.Bochner.square_bij

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Leclerc
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

From Requisite Require Import stdlib.
From Coq Require Import ssreflect Utf8.

Section square_bij_def.

    Context (n : nat).

    Definition square_bij :=
        fun c : (nat × nat) ⇒
        let (k1, k2) := c in
        k1 × n + k2.

    Definition square_bij_inv :=
        fun m : nat
            ((m / n), (m mod n)).

End square_bij_def.

Section square_bij_prop.

    Context (n : nat).

    Lemma is_bij_square :
         k1 k2 : nat, k2 n square_bij_inv (S n) (square_bij (S n) (k1, k2)) = (k1, k2).
    Proof.
        movek1 k2 Hk2.
        unfold square_bij, square_bij_inv.
        congr pair.
            rewrite Nat.div_add_l ⇒ //.
            rewrite Nat.div_small ⇒ //.
            apply le_n_S ⇒ //.
            rewrite Nat.add_comm.
            rewrite Nat.Div0.mod_add ⇒ //.
            rewrite Nat.mod_small ⇒ //.
            apply le_n_S ⇒ //.
    Qed.

    Lemma confined_snd_square_inv :
         m : nat, (snd (square_bij_inv (S n) m)) n.
    Proof.
        movem.
        unfold square_bij_inv, snd.
        suff: (m mod S n < S n) by lia.
        apply Nat.mod_upper_bound ⇒ //.
    Qed.

    Lemma is_bij_square_inv :
         m : nat, square_bij (S n) (square_bij_inv (S n) m) = m.
    Proof.
        movem; unfold square_bij_inv, square_bij.
        rewrite Nat.mul_comm.
        rewrite <-Nat.div_mod ⇒ //.
    Qed.

    Lemma square_bij_corner :
         n' : nat,
            square_bij (S n) (n', n) = ((S n') × (S n) - 1).
    Proof.
        unfold square_bij; lia.
    Qed.

    Lemma square_bij_inv_corner :
         n' : nat,
            square_bij_inv (S n) ((S n') × (S n) - 1) = (n', n).
    Proof.
        moven'.
        pose Hnn' := square_bij_corner n'; clearbody Hnn'.
        assert
            (square_bij_inv (S n) (square_bij (S n) (n', n))
            = square_bij_inv (S n) (S n' × S n - 1))
            as Eq by congruence.
        rewrite is_bij_square in Eq; easy.
    Qed.

    Lemma confined_square_inv : n' : nat,
         m : nat, m S n' × S n - 1
            let (k1, k2) := square_bij_inv (S n) m in
            k1 n' k2 n.
    Proof.
        moven' m Hm; split.
        assert (m < S n' × S n) by lia.
        suff: (m / S n < S n') by lia.
        apply Nat.Div0.div_lt_upper_bound ⇒ //.
            rewrite Nat.mul_comm ⇒ //.
        suff: (m mod S n < S n) by lia.
        apply Nat.mod_upper_bound ⇒ //.
    Qed.

    Lemma confined_square : n' : nat,
         k1 k2 : nat,
            k1 n' k2 n square_bij (S n) (k1, k2) (S n' × S n) - 1.
    Proof.
        moven' k1 k2 [Hk1 Hk2].
        unfold square_bij.
        replace
            (S n' × S n - 1)
            with
            ((n' × S n) + n)
            by lia.
        apply Nat.add_le_mono ⇒ //.
        apply Nat.mul_le_mono ⇒ //.
    Qed.

End square_bij_prop.

From Coquelicot Require Import
    Hierarchy
.

Section square_bij_sum.

    Lemma sum_n_m_shift {G : AbelianGroup} :
         n m k : nat, u : nat G,
            sum_n_m (fun xu (k + x)) n m
            = sum_n_m u (k + n) (k + m).
    Proof.
        induction nm k.
            replace (k + 0) with k by lia.
            move: m k.
            induction mk u.
                rewrite sum_n_n; replace (k + 0) with k by lia; rewrite sum_n_n.
                reflexivity.
                rewrite sum_n_Sm.
                    2 : lia.
                replace (k + S m) with (S (k + m)) by lia.
                rewrite sum_n_Sm.
                    2 : lia.
                congr plus; auto.
            moveu.
            replace (k + S n) with (S (k + n)) by lia.
            case_eq (m <? S n).
                move /Nat.ltb_ltHmn.
                rewrite sum_n_m_zero.
                    2 : assumption.
                assert (k + m < S (k + n)) as Hkmn by lia.
                rewrite sum_n_m_zero.
                    2 : assumption.
                reflexivity.
            move /Nat.ltb_geHnm.
            assert (n m) as Hnm_wk by lia.
            pose IHn_mk := IHn m k u; clearbody IHn_mk.
            rewrite sum_Sn_m in IHn_mk.
                2 : lia.
            assert ((k + n) (k + m)) as Hknm by lia.
            rewrite (sum_Sn_m u) in IHn_mk.
                2 : lia.
            apply plus_reg_l with (u (k + n)) ⇒ //.
    Qed.

    Lemma square_bij_sum {G : AbelianGroup} :
         n1 n2 : nat, u : nat G,
            sum_n u (S n1 × S n2 - 1) =
            sum_n (
                fun k1sum_n (
                    fun k2u (square_bij (S n2) (k1, k2))
                ) n2
            ) n1.
    Proof.
        induction n1n2 u.
        simpl; replace (n2 + 0 - 0) with n2 by lia.
        rewrite sum_O ⇒ //=.
        replace (S (S n1) × S n2 - 1)
            with ((S n1) × (S n2) - 1 + S n2)
            by lia.
        rewrite sum_Sn.
        rewrite <-IHn1.
        assert (0 S (S n1 × S n2 - 1)) as H0 by lia.
        assert ((S n1 × S n2 - 1) (S n1 × S n2 - 1 + S n2)) as H1 by lia.
        unfold sum_n at 1; rewrite (sum_n_m_Chasles _ _ _ _ H0 H1).
        replace (sum_n_m u 0 (S n1 × S n2 - 1)) with (sum_n u (S n1 × S n2 - 1))
            by unfold sum_n ⇒ //.
        congr plus.
        clear H0 H1 IHn1.

        replace (S (S n1 × S n2 - 1)) with (S n1 × S n2) by lia.
        replace (S n1 × S n2 - 1 + S n2) with (S n1 × S n2 + n2) by lia.
        unfold square_bij.
        unfold sum_n; rewrite (sum_n_m_shift 0 n2 (S n1 × S n2) u).
        replace (S n1 × S n2 + 0) with (S n1 × S n2) by lia.
        reflexivity.
    Qed.

End square_bij_sum.

Global Opaque square_bij.
Global Opaque square_bij_inv.