agda-unimath/src/linear-algebra/lipschitz-continuity-scalar-multiplication-normed-real-vector-spaces.lagda.md at 7ab85e2e3216a073a97fcd32ba0b258c6bf5526a · UniMath/agda-unimath · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
# Lipschitz continuity of scalar multiplication in normed real vector spaces

```agda
module linear-algebra.lipschitz-continuity-scalar-multiplication-normed-real-vector-spaces where
```

<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-functions
open import foundation.identity-types
open import foundation.universe-levels

open import linear-algebra.lipschitz-maps-normed-real-vector-spaces
open import linear-algebra.normed-real-vector-spaces

open import real-numbers.absolute-value-real-numbers
open import real-numbers.dedekind-real-numbers
open import real-numbers.difference-real-numbers
open import real-numbers.distance-real-numbers
open import real-numbers.inequality-real-numbers
open import real-numbers.multiplication-real-numbers
```

</details>

## Idea

Scalar multiplication in
[normed real vector spaces](linear-algebra.normed-real-vector-spaces.md) is
[Lipschitz continuous](linear-algebra.lipschitz-maps-normed-real-vector-spaces.md)
in each argument.

## Properties

### Given a constant `c`, `v ↦ cv` is Lipschitz continuous

```agda
module _
  {l1 l2 : Level}
  (V : Normed-ℝ-Vector-Space l1 l2)
  (c : ℝ l1)
  where abstract

  is-lipschitz-left-mul-Normed-ℝ-Vector-Space :
    is-lipschitz-map-Normed-ℝ-Vector-Space V V (mul-Normed-ℝ-Vector-Space V c)
  is-lipschitz-left-mul-Normed-ℝ-Vector-Space =
    is-lipschitz-real-constant-map-Normed-ℝ-Vector-Space
      ( V)
      ( V)
      ( mul-Normed-ℝ-Vector-Space V c)
      ( nonnegative-abs-ℝ c)
      ( λ x y → leq-eq-ℝ (multiplicative-dist-Normed-ℝ-Vector-Space V c x y))
```

### Given a constant vector `v`, `c ↦ cv` is Lipschitz continuous

```agda
module _
  {l1 l2 : Level}
  (V : Normed-ℝ-Vector-Space l1 l2)
  (v : type-Normed-ℝ-Vector-Space V)
  where abstract

  is-lipschitz-right-mul-Normed-ℝ-Vector-Space :
    is-lipschitz-map-Normed-ℝ-Vector-Space
      ( normed-real-vector-space-ℝ l1)
      ( V)
      ( λ c → mul-Normed-ℝ-Vector-Space V c v)
  is-lipschitz-right-mul-Normed-ℝ-Vector-Space =
    let
      dist-V = dist-Normed-ℝ-Vector-Space V
      norm-V = map-norm-Normed-ℝ-Vector-Space V
      _*V_ = mul-Normed-ℝ-Vector-Space V
      _-V_ = diff-Normed-ℝ-Vector-Space V
    in
      is-lipschitz-real-constant-map-Normed-ℝ-Vector-Space
        ( normed-real-vector-space-ℝ l1)
        ( V)
        ( λ c → mul-Normed-ℝ-Vector-Space V c v)
        ( nonnegative-norm-Normed-ℝ-Vector-Space V v)
        ( λ c1 c2 →
          leq-eq-ℝ
            ( equational-reasoning
              dist-V (c1 *V v) (c2 *V v)
              ＝ norm-V ((c1 -ℝ c2) *V v)
                by
                  ap
                    ( norm-V)
                    ( inv
                      ( right-distributive-mul-diff-Normed-ℝ-Vector-Space V
                        ( c1)
                        ( c2)
                        ( v)))
              ＝ dist-ℝ c1 c2 *ℝ norm-V v
                by is-absolutely-homogeneous-norm-Normed-ℝ-Vector-Space V _ _
              ＝ norm-V v *ℝ dist-ℝ c1 c2
                by commutative-mul-ℝ _ _))
```