-
Notifications
You must be signed in to change notification settings - Fork 0
/
proving-an-inequality-with-julia-and-interval-arithmetic.html
1133 lines (927 loc) · 85.9 KB
/
proving-an-inequality-with-julia-and-interval-arithmetic.html
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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE html>
<html lang="en">
<head>
<title>Proving an inequality with Julia and interval arithmetic - You don't need to prove this</title>
<link href="https://newptcai.github.io/feeds/all.atom.xml" type="application/atom+xml" rel="alternate" title="You don't need to prove this Full Atom Feed" />
<!-- CSS -->
<link rel="stylesheet" type="text/css" href="https://newptcai.github.io/theme/css/w3.css">
<link rel="stylesheet" type="text/css" href="https://newptcai.github.io/theme/css/style.css">
<link rel="stylesheet" type="text/css" href="https://newptcai.github.io/theme/css/jqcloud.css">
<link rel="stylesheet" type="text/css" href="https://newptcai.github.io/theme/css/all.min.css">
<link rel="stylesheet" type="text/css" href="https://newptcai.github.io/theme/css/shariff.min.css">
<link rel="stylesheet" type="text/css" href="https://newptcai.github.io/theme/css/pygments-highlight-github.css">
<!-- JavaScript -->
<script src="https://newptcai.github.io/theme/js/jquery-3.5.1.min.js"></script>
<script src="https://newptcai.github.io/theme/js/jqcloud.min.js"></script>
<!-- Meta -->
<meta charset="utf-8" />
<meta http-equiv="X-UA-Compatible" content="IE=edge" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<meta name="HandheldFriendly" content="True" />
<meta name="author" content="Xing Shi Cai" />
<meta name="description" content="I want thank David P. Sanders and Benoît Richard for helping me go through the problems I met while writing …" />
<meta name="keywords" content="analysis, Julia, interval-arithmetic, experimental-math">
<!-- Facebook OpenGraph -->
<meta property="og:site_name" content="You don't need to prove this">
<meta property="og:title" content="Proving an inequality with Julia and interval arithmetic - You don't need to prove this" />
<meta property="og:description" content="I want thank David P. Sanders and Benoît Richard for helping me go through the problems I met while writing …" />
<meta property="og:image" content="https://newptcai.github.io">
<meta property="og:type" content="article" />
<meta property="og:url" content="https://newptcai.github.io/proving-an-inequality-with-julia-and-interval-arithmetic.html" />
<meta property="og:locale" content="de_DE" />
<meta property="og:locale:alternate" content="en_US" />
<!-- Twitter -->
<meta name="twitter:card" content="summary_large_image">
<meta name="twitter:title" content="Proving an inequality with Julia and interval arithmetic - You don't need to prove this">
<meta name="twitter:description" content="I want thank David P. Sanders and Benoît Richard for helping me go through the problems I met while writing …">
<meta name="twitter:image" content="https://newptcai.github.io">
</head>
<body>
<div class="w3-row w3-card w3-white">
<header id=banner>
<!-- AUTHOR INITIALS-->
<a href="https://newptcai.github.io" id=logo title="Home">XS</a>
<nav id="menu">
<ul>
<li><a href="https://newptcai.github.io/pages/research.html">Research</a></li>
<li><a href="https://newptcai.github.io/pages/teaching.html">Teaching</a></li>
<li class="active"><a href="https://newptcai.github.io/category/math.html">math</a></li>
<li ><a href="https://newptcai.github.io/category/mumble.html">mumble</a></li>
<li ><a href="https://newptcai.github.io/category/photo.html">photo</a></li>
</ul>
</nav>
</header>
</div>
<br>
<article>
<header class="w3-container col-main">
<h1>Proving an inequality with Julia and interval arithmetic</h1>
<div class="post-info">
<div class="w3-opacity w3-margin-right w3-margin-bottom" style="flex-grow: 1;">
<span> Posted on Sat 11 April 2020 in <a href="https://newptcai.github.io/category/math.html" style="font-style: italic">math</a>
</span>
</div>
<div id="article-tags">
<span class="w3-tag w3-light-grey w3-text-red w3-hover-red">
<a href="https://newptcai.github.io/tag/analysis.html" title=" All posts about Analysis
">#analysis</a>
</span>
<span class="w3-tag w3-light-grey w3-text-red w3-hover-red">
<a href="https://newptcai.github.io/tag/julia.html" title=" All posts about Julia
">#Julia</a>
</span>
<span class="w3-tag w3-light-grey w3-text-red w3-hover-red">
<a href="https://newptcai.github.io/tag/interval-arithmetic.html" title=" All posts about Interval-Arithmetic
">#interval-arithmetic</a>
</span>
<span class="w3-tag w3-light-grey w3-text-red w3-hover-red">
<a href="https://newptcai.github.io/tag/experimental-math.html" title=" All posts about Experimental-Math
">#experimental-math</a>
</span>
</div>
</div>
</header>
<br>
<div class="col-main w3-container">
<main id="article-content">
<p><em>I want thank <a href="https://github.com/dpsanders">David P. Sanders</a> <i class="fab fa-github"></i>
and <a href="https://github.com/Kolaru">Benoît Richard</a> <i class="fab fa-github"></i> for helping me go
through the problems I met while writing this post.</em></p>
<p><em>This post is written as a Jupyter notebook with Julia kernel. You can run it live on
<a href="https://mybinder.org/v2/gh/newptcai/math-note/master?filepath=2019-04-01-julia-interal-arithmetic.ipynb">Binder</a></em></p>
<hr>
<style type="text/css">.highlight .hll { background-color: var(--jp-cell-editor-active-background) }
.highlight { background: var(--jp-cell-editor-background); color: var(--jp-mirror-editor-variable-color) }
.highlight .c { color: var(--jp-mirror-editor-comment-color); font-style: italic } /* Comment */
.highlight .err { color: var(--jp-mirror-editor-error-color) } /* Error */
.highlight .k { color: var(--jp-mirror-editor-keyword-color); font-weight: bold } /* Keyword */
.highlight .o { color: var(--jp-mirror-editor-operator-color); font-weight: bold } /* Operator */
.highlight .p { color: var(--jp-mirror-editor-punctuation-color) } /* Punctuation */
.highlight .ch { color: var(--jp-mirror-editor-comment-color); font-style: italic } /* Comment.Hashbang */
.highlight .cm { color: var(--jp-mirror-editor-comment-color); font-style: italic } /* Comment.Multiline */
.highlight .cp { color: var(--jp-mirror-editor-comment-color); font-style: italic } /* Comment.Preproc */
.highlight .cpf { color: var(--jp-mirror-editor-comment-color); font-style: italic } /* Comment.PreprocFile */
.highlight .c1 { color: var(--jp-mirror-editor-comment-color); font-style: italic } /* Comment.Single */
.highlight .cs { color: var(--jp-mirror-editor-comment-color); font-style: italic } /* Comment.Special */
.highlight .kc { color: var(--jp-mirror-editor-keyword-color); font-weight: bold } /* Keyword.Constant */
.highlight .kd { color: var(--jp-mirror-editor-keyword-color); font-weight: bold } /* Keyword.Declaration */
.highlight .kn { color: var(--jp-mirror-editor-keyword-color); font-weight: bold } /* Keyword.Namespace */
.highlight .kp { color: var(--jp-mirror-editor-keyword-color); font-weight: bold } /* Keyword.Pseudo */
.highlight .kr { color: var(--jp-mirror-editor-keyword-color); font-weight: bold } /* Keyword.Reserved */
.highlight .kt { color: var(--jp-mirror-editor-keyword-color); font-weight: bold } /* Keyword.Type */
.highlight .m { color: var(--jp-mirror-editor-number-color) } /* Literal.Number */
.highlight .s { color: var(--jp-mirror-editor-string-color) } /* Literal.String */
.highlight .ow { color: var(--jp-mirror-editor-operator-color); font-weight: bold } /* Operator.Word */
.highlight .w { color: var(--jp-mirror-editor-variable-color) } /* Text.Whitespace */
.highlight .mb { color: var(--jp-mirror-editor-number-color) } /* Literal.Number.Bin */
.highlight .mf { color: var(--jp-mirror-editor-number-color) } /* Literal.Number.Float */
.highlight .mh { color: var(--jp-mirror-editor-number-color) } /* Literal.Number.Hex */
.highlight .mi { color: var(--jp-mirror-editor-number-color) } /* Literal.Number.Integer */
.highlight .mo { color: var(--jp-mirror-editor-number-color) } /* Literal.Number.Oct */
.highlight .sa { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Affix */
.highlight .sb { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Backtick */
.highlight .sc { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Char */
.highlight .dl { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Delimiter */
.highlight .sd { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Doc */
.highlight .s2 { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Double */
.highlight .se { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Escape */
.highlight .sh { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Heredoc */
.highlight .si { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Interpol */
.highlight .sx { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Other */
.highlight .sr { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Regex */
.highlight .s1 { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Single */
.highlight .ss { color: var(--jp-mirror-editor-string-color) } /* Literal.String.Symbol */
.highlight .il { color: var(--jp-mirror-editor-number-color) } /* Literal.Number.Integer.Long */</style>None
<style type="text/css">
.prompt {
min-width: 8ex;
font-size: 13px;
}
</style>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>How would you prove that
$$
f(x) = \sinh(x) - \frac{1}{2}\left(\frac{\cosh(x)}{\cosh(x-a)}\right)^{x/a} \ge 0
$$
for $a = \log(2)/2$ and all $x > 0$.</p>
<p>If you have Mathematica, this is not hard. You can also do the same thing with pencil and paper, but it will take you a bit longer 😌.</p>
<p>However, there is a third way.
You can use <a href="https://en.wikipedia.org/wiki/Validated_numerics">interval arithmetic</a>.
These are computer algorithms and softwares that compute numeric values of mathematical function with <strong>guaranteed</strong> error bounds.</p>
<p>In other words, these algorithms will not only give you an upper and lower bounds of $f(x)$,
but also also <strong>prove</strong> these bounds are correct. 😮!</p>
<p>In this post, I will show you how this can be done using <a href="https://julialang.org/">Julia</a>, a high-efficiency programming language that looks like Python but faster. It is currently my favourite choice of programming.</p>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<h2 id="Preparation">Preparation<a class="anchor-link" href="#Preparation">¶</a></h2>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>Let's install all the interval arithmetic packages that we will need if you don't already have them.</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [ ]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="k">using</span> <span class="n">Pkg</span><span class="p">;</span>
<span class="n">Pkg</span><span class="o">.</span><span class="n">activate</span><span class="p">(</span><span class="s">"."</span><span class="p">)</span>
<span class="n">Pkg</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="s">"IntervalArithmetic"</span><span class="p">);</span>
<span class="n">Pkg</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="s">"IntervalRootFinding"</span><span class="p">);</span>
<span class="n">Pkg</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="s">"ForwardDiff"</span><span class="p">)</span>
<span class="n">Pkg</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="s">"Plots"</span><span class="p">)</span>
<span class="n">Pkg</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="s">"GR"</span><span class="p">);</span>
</pre></div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<h2 id="Proof-by-picture">Proof by picture<a class="anchor-link" href="#Proof-by-picture">¶</a></h2>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>Before we try it, it is always a good idea to see if what we are trying to prove is true on a picture. (Same reason people like tinder.)</p>
<p>The expression has a constant $a$ in it, which is not a rational number. So to keep all the computations rigours, let's make it an interval. (Yes, in interval arithematic, all numbers are intervals 🤦.) We use <a href="https://github.com/JuliaIntervals/IntervalArithmetic.jl"><code>IntervalArithmetic.jl</code></a> for this.</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [2]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="k">using</span> <span class="n">IntervalArithmetic</span>
<span class="n">a</span> <span class="o">=</span> <span class="nd">@interval</span> <span class="mi">1</span><span class="o">/</span><span class="mi">2</span><span class="o">*</span><span class="n">log</span><span class="p">((</span><span class="mi">2</span><span class="p">))</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt"></div>
<div class="output_subarea output_stream output_stderr output_text">
<pre>┌ Info: Precompiling IntervalArithmetic [d1acc4aa-44c8-5952-acd4-ba5d80a2a253]
└ @ Base loading.jl:1260
</pre>
</div>
</div>
<div class="output_area">
<div class="prompt output_prompt">Out[2]:</div>
<div class="output_text output_subarea output_execute_result">
<pre>[0.346573, 0.346574]</pre>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>These two number are <strong>guaranteed</strong> true lower and upper bound of the <em>true</em> value of $a$.</p>
<p>We can now define our $f(x)$.</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [3]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="n">f</span><span class="p">(</span><span class="n">x</span><span class="p">)</span><span class="o">=</span><span class="n">sinh</span><span class="p">(</span><span class="n">x</span><span class="p">)</span> <span class="o">-</span> <span class="mi">1</span><span class="o">/</span><span class="mi">2</span> <span class="o">*</span> <span class="p">(</span><span class="n">cosh</span><span class="p">(</span><span class="n">x</span><span class="p">)</span><span class="o">/</span><span class="n">cosh</span><span class="p">(</span><span class="n">x</span><span class="o">-</span><span class="n">a</span><span class="p">))</span><span class="o">^</span><span class="p">(</span><span class="n">x</span><span class="o">/</span><span class="n">a</span><span class="p">);</span>
</pre></div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>Let's try compute it at $1$</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [4]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="n">f</span><span class="p">(</span><span class="mi">1</span><span class="p">)</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt output_prompt">Out[4]:</div>
<div class="output_text output_subarea output_execute_result">
<pre>[0.193128, 0.193129]</pre>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>Because we have defined $a$ to be an interval, when we compute $f(1)$, we also get an interval. If we have defined $a$ to be of type <code>Float64</code>, we will get a <code>Float64</code> instead.</p>
<p>So this computation tells you that, the true value of $f(1)$ is guranteed to be between these two numbers. We do not see the proof. But in theory we can follow what the computer does line by line and get human proof.</p>
<p>Now the picture.</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [5]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="k">using</span> <span class="n">Plots</span>
<span class="n">gr</span><span class="p">()</span>
<span class="n">plot</span><span class="p">(</span><span class="n">x</span><span class="o">-></span><span class="n">f</span><span class="p">(</span><span class="n">x</span><span class="p">)</span><span class="o">.</span><span class="n">lo</span><span class="p">,</span> <span class="o">-</span><span class="mi">1</span><span class="o">/</span><span class="mi">2</span><span class="p">,</span> <span class="mi">10</span><span class="p">)</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt"></div>
<div class="output_subarea output_stream output_stderr output_text">
<pre>┌ Info: Precompiling Plots [91a5bcdd-55d7-5caf-9e0b-520d859cae80]
└ @ Base loading.jl:1260
</pre>
</div>
</div>
<div class="output_area">
<div class="prompt output_prompt">Out[5]:</div>
<div class="output_svg output_subarea output_execute_result">
<?xml version="1.0" encoding="utf-8"?>
<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="600" height="400" viewBox="0 0 2400 1600">
<defs>
<clipPath id="clip3900">
<rect x="0" y="0" width="2400" height="1600"/>
</clipPath>
</defs>
<path clip-path="url(#clip3900)" d="
M0 1600 L2400 1600 L2400 0 L0 0 Z
" fill="#ffffff" fill-rule="evenodd" fill-opacity="1"/>
<defs>
<clipPath id="clip3901">
<rect x="480" y="0" width="1681" height="1600"/>
</clipPath>
</defs>
<path clip-path="url(#clip3900)" d="
M189.468 1486.45 L2352.76 1486.45 L2352.76 47.2441 L189.468 47.2441 Z
" fill="#ffffff" fill-rule="evenodd" fill-opacity="1"/>
<defs>
<clipPath id="clip3902">
<rect x="189" y="47" width="2164" height="1440"/>
</clipPath>
</defs>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
347.876,1486.45 347.876,47.2441
"/>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
833.79,1486.45 833.79,47.2441
"/>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
1319.7,1486.45 1319.7,47.2441
"/>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
1805.62,1486.45 1805.62,47.2441
"/>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
2291.53,1486.45 2291.53,47.2441
"/>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
189.468,1272.44 2352.76,1272.44
"/>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
189.468,1044.94 2352.76,1044.94
"/>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
189.468,817.449 2352.76,817.449
"/>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
189.468,589.953 2352.76,589.953
"/>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
189.468,362.457 2352.76,362.457
"/>
<polyline clip-path="url(#clip3902)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
189.468,134.961 2352.76,134.961
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
189.468,1486.45 2352.76,1486.45
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
189.468,1486.45 189.468,47.2441
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
347.876,1486.45 347.876,1469.18
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
833.79,1486.45 833.79,1469.18
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
1319.7,1486.45 1319.7,1469.18
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
1805.62,1486.45 1805.62,1469.18
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
2291.53,1486.45 2291.53,1469.18
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
189.468,1272.44 215.428,1272.44
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
189.468,1044.94 215.428,1044.94
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
189.468,817.449 215.428,817.449
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
189.468,589.953 215.428,589.953
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
189.468,362.457 215.428,362.457
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
189.468,134.961 215.428,134.961
"/>
<path clip-path="url(#clip3900)" d="M 0 0 M329.393 1508.44 Q325.781 1508.44 323.953 1512 Q322.147 1515.55 322.147 1522.67 Q322.147 1529.78 323.953 1533.35 Q325.781 1536.89 329.393 1536.89 Q333.027 1536.89 334.832 1533.35 Q336.661 1529.78 336.661 1522.67 Q336.661 1515.55 334.832 1512 Q333.027 1508.44 329.393 1508.44 M329.393 1504.73 Q335.203 1504.73 338.258 1509.34 Q341.337 1513.92 341.337 1522.67 Q341.337 1531.4 338.258 1536.01 Q335.203 1540.59 329.393 1540.59 Q323.582 1540.59 320.504 1536.01 Q317.448 1531.4 317.448 1522.67 Q317.448 1513.92 320.504 1509.34 Q323.582 1504.73 329.393 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M346.406 1534.04 L351.291 1534.04 L351.291 1539.92 L346.406 1539.92 L346.406 1534.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M366.36 1508.44 Q362.749 1508.44 360.92 1512 Q359.115 1515.55 359.115 1522.67 Q359.115 1529.78 360.92 1533.35 Q362.749 1536.89 366.36 1536.89 Q369.994 1536.89 371.8 1533.35 Q373.628 1529.78 373.628 1522.67 Q373.628 1515.55 371.8 1512 Q369.994 1508.44 366.36 1508.44 M366.36 1504.73 Q372.17 1504.73 375.226 1509.34 Q378.304 1513.92 378.304 1522.67 Q378.304 1531.4 375.226 1536.01 Q372.17 1540.59 366.36 1540.59 Q360.55 1540.59 357.471 1536.01 Q354.416 1531.4 354.416 1522.67 Q354.416 1513.92 357.471 1509.34 Q360.55 1504.73 366.36 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M810.457 1535.98 L826.776 1535.98 L826.776 1539.92 L804.832 1539.92 L804.832 1535.98 Q807.494 1533.23 812.077 1528.6 Q816.684 1523.95 817.864 1522.61 Q820.109 1520.08 820.989 1518.35 Q821.892 1516.59 821.892 1514.9 Q821.892 1512.14 819.947 1510.41 Q818.026 1508.67 814.924 1508.67 Q812.725 1508.67 810.272 1509.43 Q807.841 1510.2 805.063 1511.75 L805.063 1507.03 Q807.887 1505.89 810.341 1505.31 Q812.795 1504.73 814.832 1504.73 Q820.202 1504.73 823.396 1507.42 Q826.591 1510.11 826.591 1514.6 Q826.591 1516.73 825.781 1518.65 Q824.994 1520.54 822.887 1523.14 Q822.308 1523.81 819.207 1527.03 Q816.105 1530.22 810.457 1535.98 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M831.845 1534.04 L836.73 1534.04 L836.73 1539.92 L831.845 1539.92 L831.845 1534.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M841.845 1505.36 L860.202 1505.36 L860.202 1509.3 L846.128 1509.3 L846.128 1517.77 Q847.146 1517.42 848.165 1517.26 Q849.183 1517.07 850.202 1517.07 Q855.989 1517.07 859.368 1520.24 Q862.748 1523.42 862.748 1528.83 Q862.748 1534.41 859.276 1537.51 Q855.804 1540.59 849.484 1540.59 Q847.308 1540.59 845.04 1540.22 Q842.794 1539.85 840.387 1539.11 L840.387 1534.41 Q842.47 1535.54 844.693 1536.1 Q846.915 1536.66 849.392 1536.66 Q853.396 1536.66 855.734 1534.55 Q858.072 1532.44 858.072 1528.83 Q858.072 1525.22 855.734 1523.11 Q853.396 1521.01 849.392 1521.01 Q847.517 1521.01 845.642 1521.42 Q843.79 1521.84 841.845 1522.72 L841.845 1505.36 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M1291.5 1505.36 L1309.85 1505.36 L1309.85 1509.3 L1295.78 1509.3 L1295.78 1517.77 Q1296.8 1517.42 1297.82 1517.26 Q1298.84 1517.07 1299.85 1517.07 Q1305.64 1517.07 1309.02 1520.24 Q1312.4 1523.42 1312.4 1528.83 Q1312.4 1534.41 1308.93 1537.51 Q1305.46 1540.59 1299.14 1540.59 Q1296.96 1540.59 1294.69 1540.22 Q1292.45 1539.85 1290.04 1539.11 L1290.04 1534.41 Q1292.12 1535.54 1294.34 1536.1 Q1296.57 1536.66 1299.04 1536.66 Q1303.05 1536.66 1305.39 1534.55 Q1307.72 1532.44 1307.72 1528.83 Q1307.72 1525.22 1305.39 1523.11 Q1303.05 1521.01 1299.04 1521.01 Q1297.17 1521.01 1295.29 1521.42 Q1293.44 1521.84 1291.5 1522.72 L1291.5 1505.36 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M1317.47 1534.04 L1322.35 1534.04 L1322.35 1539.92 L1317.47 1539.92 L1317.47 1534.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M1337.42 1508.44 Q1333.81 1508.44 1331.98 1512 Q1330.18 1515.55 1330.18 1522.67 Q1330.18 1529.78 1331.98 1533.35 Q1333.81 1536.89 1337.42 1536.89 Q1341.06 1536.89 1342.86 1533.35 Q1344.69 1529.78 1344.69 1522.67 Q1344.69 1515.55 1342.86 1512 Q1341.06 1508.44 1337.42 1508.44 M1337.42 1504.73 Q1343.23 1504.73 1346.29 1509.34 Q1349.37 1513.92 1349.37 1522.67 Q1349.37 1531.4 1346.29 1536.01 Q1343.23 1540.59 1337.42 1540.59 Q1331.61 1540.59 1328.53 1536.01 Q1325.48 1531.4 1325.48 1522.67 Q1325.48 1513.92 1328.53 1509.34 Q1331.61 1504.73 1337.42 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M1776.52 1505.36 L1798.74 1505.36 L1798.74 1507.35 L1786.2 1539.92 L1781.31 1539.92 L1793.12 1509.3 L1776.52 1509.3 L1776.52 1505.36 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M1803.81 1534.04 L1808.7 1534.04 L1808.7 1539.92 L1803.81 1539.92 L1803.81 1534.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M1813.81 1505.36 L1832.17 1505.36 L1832.17 1509.3 L1818.09 1509.3 L1818.09 1517.77 Q1819.11 1517.42 1820.13 1517.26 Q1821.15 1517.07 1822.17 1517.07 Q1827.96 1517.07 1831.33 1520.24 Q1834.71 1523.42 1834.71 1528.83 Q1834.71 1534.41 1831.24 1537.51 Q1827.77 1540.59 1821.45 1540.59 Q1819.27 1540.59 1817.01 1540.22 Q1814.76 1539.85 1812.35 1539.11 L1812.35 1534.41 Q1814.44 1535.54 1816.66 1536.1 Q1818.88 1536.66 1821.36 1536.66 Q1825.36 1536.66 1827.7 1534.55 Q1830.04 1532.44 1830.04 1528.83 Q1830.04 1525.22 1827.7 1523.11 Q1825.36 1521.01 1821.36 1521.01 Q1819.48 1521.01 1817.61 1521.42 Q1815.76 1521.84 1813.81 1522.72 L1813.81 1505.36 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M2249.92 1535.98 L2257.56 1535.98 L2257.56 1509.62 L2249.25 1511.29 L2249.25 1507.03 L2257.51 1505.36 L2262.19 1505.36 L2262.19 1535.98 L2269.83 1535.98 L2269.83 1539.92 L2249.92 1539.92 L2249.92 1535.98 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M2284.9 1508.44 Q2281.29 1508.44 2279.46 1512 Q2277.65 1515.55 2277.65 1522.67 Q2277.65 1529.78 2279.46 1533.35 Q2281.29 1536.89 2284.9 1536.89 Q2288.53 1536.89 2290.34 1533.35 Q2292.17 1529.78 2292.17 1522.67 Q2292.17 1515.55 2290.34 1512 Q2288.53 1508.44 2284.9 1508.44 M2284.9 1504.73 Q2290.71 1504.73 2293.76 1509.34 Q2296.84 1513.92 2296.84 1522.67 Q2296.84 1531.4 2293.76 1536.01 Q2290.71 1540.59 2284.9 1540.59 Q2279.09 1540.59 2276.01 1536.01 Q2272.95 1531.4 2272.95 1522.67 Q2272.95 1513.92 2276.01 1509.34 Q2279.09 1504.73 2284.9 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M2301.91 1534.04 L2306.8 1534.04 L2306.8 1539.92 L2301.91 1539.92 L2301.91 1534.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M2321.87 1508.44 Q2318.26 1508.44 2316.43 1512 Q2314.62 1515.55 2314.62 1522.67 Q2314.62 1529.78 2316.43 1533.35 Q2318.26 1536.89 2321.87 1536.89 Q2325.5 1536.89 2327.31 1533.35 Q2329.13 1529.78 2329.13 1522.67 Q2329.13 1515.55 2327.31 1512 Q2325.5 1508.44 2321.87 1508.44 M2321.87 1504.73 Q2327.68 1504.73 2330.73 1509.34 Q2333.81 1513.92 2333.81 1522.67 Q2333.81 1531.4 2330.73 1536.01 Q2327.68 1540.59 2321.87 1540.59 Q2316.06 1540.59 2312.98 1536.01 Q2309.92 1531.4 2309.92 1522.67 Q2309.92 1513.92 2312.98 1509.34 Q2316.06 1504.73 2321.87 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M63.2236 1274.84 L75.7004 1274.84 L75.7004 1278.63 L63.2236 1278.63 L63.2236 1274.84 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M81.58 1285.79 L89.2188 1285.79 L89.2188 1259.42 L80.9087 1261.09 L80.9087 1256.83 L89.1725 1255.16 L93.8484 1255.16 L93.8484 1285.79 L101.487 1285.79 L101.487 1289.72 L81.58 1289.72 L81.58 1285.79 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M106.557 1283.84 L111.441 1283.84 L111.441 1289.72 L106.557 1289.72 L106.557 1283.84 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M126.51 1258.24 Q122.899 1258.24 121.071 1261.8 Q119.265 1265.35 119.265 1272.48 Q119.265 1279.58 121.071 1283.15 Q122.899 1286.69 126.51 1286.69 Q130.145 1286.69 131.95 1283.15 Q133.779 1279.58 133.779 1272.48 Q133.779 1265.35 131.95 1261.8 Q130.145 1258.24 126.51 1258.24 M126.51 1254.54 Q132.32 1254.54 135.376 1259.14 Q138.455 1263.73 138.455 1272.48 Q138.455 1281.2 135.376 1285.81 Q132.32 1290.39 126.51 1290.39 Q120.7 1290.39 117.621 1285.81 Q114.566 1281.2 114.566 1272.48 Q114.566 1263.73 117.621 1259.14 Q120.7 1254.54 126.51 1254.54 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M153.524 1258.24 Q149.913 1258.24 148.084 1261.8 Q146.279 1265.35 146.279 1272.48 Q146.279 1279.58 148.084 1283.15 Q149.913 1286.69 153.524 1286.69 Q157.158 1286.69 158.964 1283.15 Q160.793 1279.58 160.793 1272.48 Q160.793 1265.35 158.964 1261.8 Q157.158 1258.24 153.524 1258.24 M153.524 1254.54 Q159.334 1254.54 162.39 1259.14 Q165.468 1263.73 165.468 1272.48 Q165.468 1281.2 162.39 1285.81 Q159.334 1290.39 153.524 1290.39 Q147.714 1290.39 144.635 1285.81 Q141.58 1281.2 141.58 1272.48 Q141.58 1263.73 144.635 1259.14 Q147.714 1254.54 153.524 1254.54 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M63.8949 1047.34 L76.3717 1047.34 L76.3717 1051.14 L63.8949 1051.14 L63.8949 1047.34 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M91.441 1030.74 Q87.83 1030.74 86.0013 1034.31 Q84.1957 1037.85 84.1957 1044.98 Q84.1957 1052.09 86.0013 1055.65 Q87.83 1059.19 91.441 1059.19 Q95.0753 1059.19 96.8808 1055.65 Q98.7095 1052.09 98.7095 1044.98 Q98.7095 1037.85 96.8808 1034.31 Q95.0753 1030.74 91.441 1030.74 M91.441 1027.04 Q97.2512 1027.04 100.307 1031.65 Q103.385 1036.23 103.385 1044.98 Q103.385 1053.71 100.307 1058.31 Q97.2512 1062.9 91.441 1062.9 Q85.6309 1062.9 82.5522 1058.31 Q79.4967 1053.71 79.4967 1044.98 Q79.4967 1036.23 82.5522 1031.65 Q85.6309 1027.04 91.441 1027.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M108.455 1056.35 L113.339 1056.35 L113.339 1062.22 L108.455 1062.22 L108.455 1056.35 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M117.228 1027.66 L139.45 1027.66 L139.45 1029.66 L126.904 1062.22 L122.02 1062.22 L133.825 1031.6 L117.228 1031.6 L117.228 1027.66 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M144.566 1027.66 L162.922 1027.66 L162.922 1031.6 L148.848 1031.6 L148.848 1040.07 Q149.867 1039.72 150.885 1039.56 Q151.904 1039.38 152.922 1039.38 Q158.709 1039.38 162.089 1042.55 Q165.468 1045.72 165.468 1051.14 Q165.468 1056.72 161.996 1059.82 Q158.524 1062.9 152.205 1062.9 Q150.029 1062.9 147.76 1062.53 Q145.515 1062.16 143.107 1061.41 L143.107 1056.72 Q145.191 1057.85 147.413 1058.41 Q149.635 1058.96 152.112 1058.96 Q156.117 1058.96 158.455 1056.85 Q160.793 1054.75 160.793 1051.14 Q160.793 1047.53 158.455 1045.42 Q156.117 1043.31 152.112 1043.31 Q150.237 1043.31 148.362 1043.73 Q146.51 1044.15 144.566 1045.03 L144.566 1027.66 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M62.9921 819.845 L75.4689 819.845 L75.4689 823.641 L62.9921 823.641 L62.9921 819.845 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M90.5383 803.247 Q86.9272 803.247 85.0985 806.812 Q83.2929 810.354 83.2929 817.483 Q83.2929 824.59 85.0985 828.155 Q86.9272 831.696 90.5383 831.696 Q94.1725 831.696 95.9781 828.155 Q97.8068 824.59 97.8068 817.483 Q97.8068 810.354 95.9781 806.812 Q94.1725 803.247 90.5383 803.247 M90.5383 799.544 Q96.3484 799.544 99.404 804.15 Q102.483 808.733 102.483 817.483 Q102.483 826.21 99.404 830.817 Q96.3484 835.4 90.5383 835.4 Q84.7281 835.4 81.6494 830.817 Q78.5939 826.21 78.5939 817.483 Q78.5939 808.733 81.6494 804.15 Q84.7281 799.544 90.5383 799.544 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M107.552 828.849 L112.436 828.849 L112.436 834.729 L107.552 834.729 L107.552 828.849 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M117.552 800.169 L135.908 800.169 L135.908 804.104 L121.834 804.104 L121.834 812.576 Q122.853 812.229 123.871 812.067 Q124.89 811.882 125.908 811.882 Q131.695 811.882 135.075 815.053 Q138.455 818.224 138.455 823.641 Q138.455 829.22 134.982 832.321 Q131.51 835.4 125.191 835.4 Q123.015 835.4 120.746 835.03 Q118.501 834.659 116.094 833.919 L116.094 829.22 Q118.177 830.354 120.399 830.909 Q122.621 831.465 125.098 831.465 Q129.103 831.465 131.441 829.358 Q133.779 827.252 133.779 823.641 Q133.779 820.03 131.441 817.923 Q129.103 815.817 125.098 815.817 Q123.223 815.817 121.348 816.233 Q119.496 816.65 117.552 817.53 L117.552 800.169 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M153.524 803.247 Q149.913 803.247 148.084 806.812 Q146.279 810.354 146.279 817.483 Q146.279 824.59 148.084 828.155 Q149.913 831.696 153.524 831.696 Q157.158 831.696 158.964 828.155 Q160.793 824.59 160.793 817.483 Q160.793 810.354 158.964 806.812 Q157.158 803.247 153.524 803.247 M153.524 799.544 Q159.334 799.544 162.39 804.15 Q165.468 808.733 165.468 817.483 Q165.468 826.21 162.39 830.817 Q159.334 835.4 153.524 835.4 Q147.714 835.4 144.635 830.817 Q141.58 826.21 141.58 817.483 Q141.58 808.733 144.635 804.15 Q147.714 799.544 153.524 799.544 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M64.5893 592.349 L77.0661 592.349 L77.0661 596.145 L64.5893 596.145 L64.5893 592.349 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M92.1355 575.751 Q88.5244 575.751 86.6957 579.316 Q84.8902 582.858 84.8902 589.988 Q84.8902 597.094 86.6957 600.659 Q88.5244 604.2 92.1355 604.2 Q95.7697 604.2 97.5753 600.659 Q99.404 597.094 99.404 589.988 Q99.404 582.858 97.5753 579.316 Q95.7697 575.751 92.1355 575.751 M92.1355 572.048 Q97.9456 572.048 101.001 576.654 Q104.08 581.238 104.08 589.988 Q104.08 598.714 101.001 603.321 Q97.9456 607.904 92.1355 607.904 Q86.3253 607.904 83.2466 603.321 Q80.1911 598.714 80.1911 589.988 Q80.1911 581.238 83.2466 576.654 Q86.3253 572.048 92.1355 572.048 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M109.149 601.353 L114.034 601.353 L114.034 607.233 L109.149 607.233 L109.149 601.353 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M123.131 603.298 L139.45 603.298 L139.45 607.233 L117.506 607.233 L117.506 603.298 Q120.168 600.543 124.751 595.913 Q129.358 591.261 130.538 589.918 Q132.783 587.395 133.663 585.659 Q134.566 583.9 134.566 582.21 Q134.566 579.455 132.621 577.719 Q130.7 575.983 127.598 575.983 Q125.399 575.983 122.946 576.747 Q120.515 577.511 117.737 579.062 L117.737 574.339 Q120.561 573.205 123.015 572.626 Q125.469 572.048 127.506 572.048 Q132.876 572.048 136.07 574.733 Q139.265 577.418 139.265 581.909 Q139.265 584.038 138.455 585.96 Q137.668 587.858 135.561 590.45 Q134.982 591.122 131.881 594.339 Q128.779 597.534 123.131 603.298 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M144.566 572.673 L162.922 572.673 L162.922 576.608 L148.848 576.608 L148.848 585.08 Q149.867 584.733 150.885 584.571 Q151.904 584.386 152.922 584.386 Q158.709 584.386 162.089 587.557 Q165.468 590.728 165.468 596.145 Q165.468 601.724 161.996 604.825 Q158.524 607.904 152.205 607.904 Q150.029 607.904 147.76 607.534 Q145.515 607.163 143.107 606.423 L143.107 601.724 Q145.191 602.858 147.413 603.413 Q149.635 603.969 152.112 603.969 Q156.117 603.969 158.455 601.862 Q160.793 599.756 160.793 596.145 Q160.793 592.534 158.455 590.427 Q156.117 588.321 152.112 588.321 Q150.237 588.321 148.362 588.738 Q146.51 589.154 144.566 590.034 L144.566 572.673 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M89.5429 348.256 Q85.9318 348.256 84.1031 351.82 Q82.2976 355.362 82.2976 362.492 Q82.2976 369.598 84.1031 373.163 Q85.9318 376.704 89.5429 376.704 Q93.1771 376.704 94.9827 373.163 Q96.8114 369.598 96.8114 362.492 Q96.8114 355.362 94.9827 351.82 Q93.1771 348.256 89.5429 348.256 M89.5429 344.552 Q95.3531 344.552 98.4086 349.158 Q101.487 353.742 101.487 362.492 Q101.487 371.218 98.4086 375.825 Q95.3531 380.408 89.5429 380.408 Q83.7328 380.408 80.6541 375.825 Q77.5985 371.218 77.5985 362.492 Q77.5985 353.742 80.6541 349.158 Q83.7328 344.552 89.5429 344.552 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M106.557 373.857 L111.441 373.857 L111.441 379.737 L106.557 379.737 L106.557 373.857 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M126.51 348.256 Q122.899 348.256 121.071 351.82 Q119.265 355.362 119.265 362.492 Q119.265 369.598 121.071 373.163 Q122.899 376.704 126.51 376.704 Q130.145 376.704 131.95 373.163 Q133.779 369.598 133.779 362.492 Q133.779 355.362 131.95 351.82 Q130.145 348.256 126.51 348.256 M126.51 344.552 Q132.32 344.552 135.376 349.158 Q138.455 353.742 138.455 362.492 Q138.455 371.218 135.376 375.825 Q132.32 380.408 126.51 380.408 Q120.7 380.408 117.621 375.825 Q114.566 371.218 114.566 362.492 Q114.566 353.742 117.621 349.158 Q120.7 344.552 126.51 344.552 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M153.524 348.256 Q149.913 348.256 148.084 351.82 Q146.279 355.362 146.279 362.492 Q146.279 369.598 148.084 373.163 Q149.913 376.704 153.524 376.704 Q157.158 376.704 158.964 373.163 Q160.793 369.598 160.793 362.492 Q160.793 355.362 158.964 351.82 Q157.158 348.256 153.524 348.256 M153.524 344.552 Q159.334 344.552 162.39 349.158 Q165.468 353.742 165.468 362.492 Q165.468 371.218 162.39 375.825 Q159.334 380.408 153.524 380.408 Q147.714 380.408 144.635 375.825 Q141.58 371.218 141.58 362.492 Q141.58 353.742 144.635 349.158 Q147.714 344.552 153.524 344.552 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M92.1355 120.76 Q88.5244 120.76 86.6957 124.324 Q84.8902 127.866 84.8902 134.996 Q84.8902 142.102 86.6957 145.667 Q88.5244 149.208 92.1355 149.208 Q95.7697 149.208 97.5753 145.667 Q99.404 142.102 99.404 134.996 Q99.404 127.866 97.5753 124.324 Q95.7697 120.76 92.1355 120.76 M92.1355 117.056 Q97.9456 117.056 101.001 121.662 Q104.08 126.246 104.08 134.996 Q104.08 143.722 101.001 148.329 Q97.9456 152.912 92.1355 152.912 Q86.3253 152.912 83.2466 148.329 Q80.1911 143.722 80.1911 134.996 Q80.1911 126.246 83.2466 121.662 Q86.3253 117.056 92.1355 117.056 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M109.149 146.361 L114.034 146.361 L114.034 152.241 L109.149 152.241 L109.149 146.361 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M123.131 148.306 L139.45 148.306 L139.45 152.241 L117.506 152.241 L117.506 148.306 Q120.168 145.551 124.751 140.922 Q129.358 136.269 130.538 134.926 Q132.783 132.403 133.663 130.667 Q134.566 128.908 134.566 127.218 Q134.566 124.463 132.621 122.727 Q130.7 120.991 127.598 120.991 Q125.399 120.991 122.946 121.755 Q120.515 122.519 117.737 124.07 L117.737 119.348 Q120.561 118.213 123.015 117.635 Q125.469 117.056 127.506 117.056 Q132.876 117.056 136.07 119.741 Q139.265 122.426 139.265 126.917 Q139.265 129.047 138.455 130.968 Q137.668 132.866 135.561 135.459 Q134.982 136.13 131.881 139.347 Q128.779 142.542 123.131 148.306 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M144.566 117.681 L162.922 117.681 L162.922 121.616 L148.848 121.616 L148.848 130.088 Q149.867 129.741 150.885 129.579 Q151.904 129.394 152.922 129.394 Q158.709 129.394 162.089 132.565 Q165.468 135.736 165.468 141.153 Q165.468 146.732 161.996 149.833 Q158.524 152.912 152.205 152.912 Q150.029 152.912 147.76 152.542 Q145.515 152.171 143.107 151.431 L143.107 146.732 Q145.191 147.866 147.413 148.421 Q149.635 148.977 152.112 148.977 Q156.117 148.977 158.455 146.871 Q160.793 144.764 160.793 141.153 Q160.793 137.542 158.455 135.435 Q156.117 133.329 152.112 133.329 Q150.237 133.329 148.362 133.746 Q146.51 134.162 144.566 135.042 L144.566 117.681 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><polyline clip-path="url(#clip3902)" style="stroke:#009af9; stroke-width:4; stroke-opacity:1; fill:none" points="
250.694,1445.72 255.676,1405.69 260.659,1366.65 265.641,1328.58 270.624,1291.44 293.66,1131.18 316.695,987.948 339.731,859.614 362.767,744.351 385.803,640.679
408.838,547.473 431.874,463.939 454.91,389.572 482.597,311.911 510.284,246.761 537.971,193.82 565.658,152.606 589.067,126.358 612.476,107.341 635.885,94.8171
659.294,87.9763 710.151,88.6944 761.009,104.202 807.895,125.879 854.781,150.745 955.315,204.287 1071.79,255.942 1175.31,289.864 1266.08,311.467 1365.04,328.233
1464.59,339.797 1574.66,348.245 1679.39,353.416 1788.28,356.849 1879.94,358.724 1991.86,360.198 2097.06,361.054 2265.59,361.808 2291.53,361.881
"/>
<path clip-path="url(#clip3900)" d="
M1989.74 251.724 L2280.76 251.724 L2280.76 130.764 L1989.74 130.764 Z
" fill="#ffffff" fill-rule="evenodd" fill-opacity="1"/>
<polyline clip-path="url(#clip3900)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
1989.74,251.724 2280.76,251.724 2280.76,130.764 1989.74,130.764 1989.74,251.724
"/>
<polyline clip-path="url(#clip3900)" style="stroke:#009af9; stroke-width:4; stroke-opacity:1; fill:none" points="
2013.74,191.244 2157.74,191.244
"/>
<path clip-path="url(#clip3900)" d="M 0 0 M2195.58 210.931 Q2193.77 215.561 2192.06 216.973 Q2190.35 218.385 2187.48 218.385 L2184.08 218.385 L2184.08 214.82 L2186.58 214.82 Q2188.33 214.82 2189.31 213.987 Q2190.28 213.154 2191.46 210.052 L2192.22 208.107 L2181.74 182.598 L2186.25 182.598 L2194.35 202.876 L2202.46 182.598 L2206.97 182.598 L2195.58 210.931 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip3900)" d="M 0 0 M2212.85 204.589 L2220.49 204.589 L2220.49 178.223 L2212.18 179.89 L2212.18 175.631 L2220.44 173.964 L2225.12 173.964 L2225.12 204.589 L2232.76 204.589 L2232.76 208.524 L2212.85 208.524 L2212.85 204.589 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /></svg>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>So I lied to you earlier 😑️. The function has a root on $(0,\infty)$. It looks like to be somewhere between $0$ and $1$. Let's see if this is true. And above this root, $f(x)$ seems to remain positve. Can we show this?</p>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<h2 id="The-first-(only?)-root">The first (only?) root<a class="anchor-link" href="#The-first-(only?)-root">¶</a></h2>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>We can try <a href="https://github.com/JuliaIntervals/IntervalRootFinding.jl"><code>IntervalRootFinding.jl</code></a> to find at least where the root is.</p>
<p>Because we have defined $a$ to be an interval, when we compute $f(1)$, we also get an interval. (If we have defined $a$ to be of type <code>Float64</code>, we will get a <code>Float64</code> instead.)</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [6]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="k">using</span> <span class="n">IntervalRootFinding</span>
<span class="n">roots</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="nd">@interval</span><span class="p">(</span><span class="mi">0</span><span class="p">,</span> <span class="mi">1</span><span class="p">))</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt"></div>
<div class="output_subarea output_stream output_stderr output_text">
<pre>┌ Info: Precompiling IntervalRootFinding [d2bf35a9-74e0-55ec-b149-d360ff49b807]
└ @ Base loading.jl:1260
</pre>
</div>
</div>
<div class="output_area">
<div class="prompt output_prompt">Out[6]:</div>
<div class="output_text output_subarea output_execute_result">
<pre>1-element Array{Root{Interval{Float64}},1}:
Root([0.597845, 0.597846], :unique)</pre>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>Yes!
There is one root of $f(x)$ in $[0,1]$. The algorithm even tells you that it's unique.
We get a <strong>true proof</strong> for this fact without breaking a sweat 😀️.</p>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<h2 id="More-roots?">More roots?<a class="anchor-link" href="#More-roots?">¶</a></h2><p>The problem then is to show that there is no other roots. Let try $[1,2]$ first.</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [7]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="n">roots</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="nd">@interval</span><span class="p">(</span><span class="mi">1</span><span class="p">,</span> <span class="mi">2</span><span class="p">))</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt output_prompt">Out[7]:</div>
<div class="output_text output_subarea output_execute_result">
<pre>0-element Array{Root{Interval{Float64}},1}</pre>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>There is nothing. Let's try $[2,4]$</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [8]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="n">roots</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="nd">@interval</span><span class="p">(</span><span class="mi">2</span><span class="p">,</span> <span class="mi">4</span><span class="p">))</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt output_prompt">Out[8]:</div>
<div class="output_text output_subarea output_execute_result">
<pre>0-element Array{Root{Interval{Float64}},1}</pre>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>Again, no roots.
But there are two problems here.
First, it gets rather slow when you try larger interval, say $[4,8]$.
Two, if the aim is to <em>prove</em> there are no roots on $[1, \infty]$, we will not be able to do this by checking finite many bounded intervals.</p>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>For some very simple functions, like $x$, $e^{2x}$, the algorithm can actually do it. But not our $f(x)$.</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [9]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="n">roots</span><span class="p">(</span><span class="n">x</span> <span class="o">-></span> <span class="n">x</span><span class="p">,</span> <span class="mf">1.</span><span class="o">.</span><span class="n">∞</span><span class="p">)</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt output_prompt">Out[9]:</div>
<div class="output_text output_subarea output_execute_result">
<pre>0-element Array{Root{Interval{Float64}},1}</pre>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [10]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="n">roots</span><span class="p">(</span><span class="n">x</span> <span class="o">-></span> <span class="n">exp</span><span class="p">(</span><span class="n">x</span><span class="o">^</span><span class="mi">2</span><span class="p">),</span> <span class="mf">1.</span><span class="o">.</span><span class="n">∞</span><span class="p">)</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt output_prompt">Out[10]:</div>
<div class="output_text output_subarea output_execute_result">
<pre>0-element Array{Root{Interval{Float64}},1}</pre>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<h2 id="Simplified-problem">Simplified problem<a class="anchor-link" href="#Simplified-problem">¶</a></h2><p>So here's the truth about numeric methods.
You can rarely avoid doing some symbolic computation.
You should combine both the strength of numeric and symbolic.</p>
<p>I massaged the problem a bit in Mathematica and found it is equivalent to show that
$$
\log (1-s)+\frac{\log \left(\frac{1}{2 e^2}\right) (\log (s+1)-\log (2 s+1))}{\log (2)} \ge 0
$$
on $s \in [0,e^{-2}]$.
(Let's not to worry how I got it. That's not the point for today.)</p>
<p>Let's define another function $g(s)$ for the left-hand-side.</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [11]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="n">g</span><span class="p">(</span><span class="n">s</span><span class="p">)</span> <span class="o">=</span> <span class="n">log</span><span class="p">(</span><span class="o">-</span><span class="n">s</span> <span class="o">+</span> <span class="mi">1</span><span class="p">)</span><span class="o">-</span><span class="p">(</span><span class="n">log</span><span class="p">(</span><span class="mi">2</span><span class="o">*</span><span class="n">s</span> <span class="o">+</span> <span class="mi">1</span><span class="p">)</span> <span class="o">-</span> <span class="n">log</span><span class="p">(</span><span class="n">s</span> <span class="o">+</span> <span class="mi">1</span><span class="p">))</span><span class="o">*</span><span class="n">log</span><span class="p">(</span><span class="mi">1</span><span class="o">/</span><span class="mi">2</span><span class="o">/</span><span class="n">exp</span><span class="p">(</span><span class="mi">2</span><span class="p">))</span><span class="o">/</span><span class="n">log</span><span class="p">(</span><span class="mi">2</span><span class="p">)</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt output_prompt">Out[11]:</div>
<div class="output_text output_subarea output_execute_result">
<pre>g (generic function with 1 method)</pre>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>How does it look like?</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [12]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="n">box</span> <span class="o">=</span> <span class="nd">@interval</span> <span class="o">-</span><span class="n">exp</span><span class="p">(</span><span class="o">-</span><span class="mi">2</span><span class="p">)</span> <span class="n">exp</span><span class="p">(</span><span class="o">-</span><span class="mi">2</span><span class="p">)</span>
<span class="n">plot</span><span class="p">(</span><span class="n">g</span><span class="p">,</span> <span class="n">box</span><span class="o">.</span><span class="n">lo</span><span class="p">,</span> <span class="n">box</span><span class="o">.</span><span class="n">hi</span><span class="p">)</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt output_prompt">Out[12]:</div>
<div class="output_svg output_subarea output_execute_result">
<?xml version="1.0" encoding="utf-8"?>
<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="600" height="400" viewBox="0 0 2400 1600">
<defs>
<clipPath id="clip4300">
<rect x="0" y="0" width="2400" height="1600"/>
</clipPath>
</defs>
<path clip-path="url(#clip4300)" d="
M0 1600 L2400 1600 L2400 0 L0 0 Z
" fill="#ffffff" fill-rule="evenodd" fill-opacity="1"/>
<defs>
<clipPath id="clip4301">
<rect x="480" y="0" width="1681" height="1600"/>
</clipPath>
</defs>
<path clip-path="url(#clip4300)" d="
M163.936 1486.45 L2352.76 1486.45 L2352.76 47.2441 L163.936 47.2441 Z
" fill="#ffffff" fill-rule="evenodd" fill-opacity="1"/>
<defs>
<clipPath id="clip4302">
<rect x="163" y="47" width="2190" height="1440"/>
</clipPath>
</defs>
<polyline clip-path="url(#clip4302)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
495.454,1486.45 495.454,47.2441
"/>
<polyline clip-path="url(#clip4302)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
876.9,1486.45 876.9,47.2441
"/>
<polyline clip-path="url(#clip4302)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
1258.35,1486.45 1258.35,47.2441
"/>
<polyline clip-path="url(#clip4302)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
1639.79,1486.45 1639.79,47.2441
"/>
<polyline clip-path="url(#clip4302)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
2021.24,1486.45 2021.24,47.2441
"/>
<polyline clip-path="url(#clip4302)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
163.936,1224.9 2352.76,1224.9
"/>
<polyline clip-path="url(#clip4302)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
163.936,896.38 2352.76,896.38
"/>
<polyline clip-path="url(#clip4302)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
163.936,567.859 2352.76,567.859
"/>
<polyline clip-path="url(#clip4302)" style="stroke:#000000; stroke-width:2; stroke-opacity:0.1; fill:none" points="
163.936,239.337 2352.76,239.337
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
163.936,1486.45 2352.76,1486.45
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
163.936,1486.45 163.936,47.2441
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
495.454,1486.45 495.454,1469.18
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
876.9,1486.45 876.9,1469.18
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
1258.35,1486.45 1258.35,1469.18
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
1639.79,1486.45 1639.79,1469.18
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
2021.24,1486.45 2021.24,1469.18
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
163.936,1224.9 190.202,1224.9
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
163.936,896.38 190.202,896.38
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
163.936,567.859 190.202,567.859
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
163.936,239.337 190.202,239.337
"/>
<path clip-path="url(#clip4300)" d="M 0 0 M444.332 1525.04 L456.808 1525.04 L456.808 1528.83 L444.332 1528.83 L444.332 1525.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M471.878 1508.44 Q468.267 1508.44 466.438 1512 Q464.632 1515.55 464.632 1522.67 Q464.632 1529.78 466.438 1533.35 Q468.267 1536.89 471.878 1536.89 Q475.512 1536.89 477.317 1533.35 Q479.146 1529.78 479.146 1522.67 Q479.146 1515.55 477.317 1512 Q475.512 1508.44 471.878 1508.44 M471.878 1504.73 Q477.688 1504.73 480.743 1509.34 Q483.822 1513.92 483.822 1522.67 Q483.822 1531.4 480.743 1536.01 Q477.688 1540.59 471.878 1540.59 Q466.068 1540.59 462.989 1536.01 Q459.933 1531.4 459.933 1522.67 Q459.933 1513.92 462.989 1509.34 Q466.068 1504.73 471.878 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M488.891 1534.04 L493.776 1534.04 L493.776 1539.92 L488.891 1539.92 L488.891 1534.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M499.655 1535.98 L507.294 1535.98 L507.294 1509.62 L498.984 1511.29 L498.984 1507.03 L507.248 1505.36 L511.924 1505.36 L511.924 1535.98 L519.563 1535.98 L519.563 1539.92 L499.655 1539.92 L499.655 1535.98 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M534.632 1508.44 Q531.021 1508.44 529.192 1512 Q527.387 1515.55 527.387 1522.67 Q527.387 1529.78 529.192 1533.35 Q531.021 1536.89 534.632 1536.89 Q538.266 1536.89 540.072 1533.35 Q541.9 1529.78 541.9 1522.67 Q541.9 1515.55 540.072 1512 Q538.266 1508.44 534.632 1508.44 M534.632 1504.73 Q540.442 1504.73 543.498 1509.34 Q546.576 1513.92 546.576 1522.67 Q546.576 1531.4 543.498 1536.01 Q540.442 1540.59 534.632 1540.59 Q528.822 1540.59 525.743 1536.01 Q522.688 1531.4 522.688 1522.67 Q522.688 1513.92 525.743 1509.34 Q528.822 1504.73 534.632 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M825.662 1525.04 L838.139 1525.04 L838.139 1528.83 L825.662 1528.83 L825.662 1525.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M853.208 1508.44 Q849.597 1508.44 847.768 1512 Q845.963 1515.55 845.963 1522.67 Q845.963 1529.78 847.768 1533.35 Q849.597 1536.89 853.208 1536.89 Q856.842 1536.89 858.648 1533.35 Q860.476 1529.78 860.476 1522.67 Q860.476 1515.55 858.648 1512 Q856.842 1508.44 853.208 1508.44 M853.208 1504.73 Q859.018 1504.73 862.074 1509.34 Q865.152 1513.92 865.152 1522.67 Q865.152 1531.4 862.074 1536.01 Q859.018 1540.59 853.208 1540.59 Q847.398 1540.59 844.319 1536.01 Q841.264 1531.4 841.264 1522.67 Q841.264 1513.92 844.319 1509.34 Q847.398 1504.73 853.208 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M870.222 1534.04 L875.106 1534.04 L875.106 1539.92 L870.222 1539.92 L870.222 1534.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M890.175 1508.44 Q886.564 1508.44 884.736 1512 Q882.93 1515.55 882.93 1522.67 Q882.93 1529.78 884.736 1533.35 Q886.564 1536.89 890.175 1536.89 Q893.81 1536.89 895.615 1533.35 Q897.444 1529.78 897.444 1522.67 Q897.444 1515.55 895.615 1512 Q893.81 1508.44 890.175 1508.44 M890.175 1504.73 Q895.986 1504.73 899.041 1509.34 Q902.12 1513.92 902.12 1522.67 Q902.12 1531.4 899.041 1536.01 Q895.986 1540.59 890.175 1540.59 Q884.365 1540.59 881.287 1536.01 Q878.231 1531.4 878.231 1522.67 Q878.231 1513.92 881.287 1509.34 Q884.365 1504.73 890.175 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M907.235 1505.36 L925.592 1505.36 L925.592 1509.3 L911.518 1509.3 L911.518 1517.77 Q912.536 1517.42 913.555 1517.26 Q914.573 1517.07 915.592 1517.07 Q921.379 1517.07 924.759 1520.24 Q928.138 1523.42 928.138 1528.83 Q928.138 1534.41 924.666 1537.51 Q921.194 1540.59 914.874 1540.59 Q912.698 1540.59 910.43 1540.22 Q908.185 1539.85 905.777 1539.11 L905.777 1534.41 Q907.86 1535.54 910.083 1536.1 Q912.305 1536.66 914.782 1536.66 Q918.786 1536.66 921.124 1534.55 Q923.462 1532.44 923.462 1528.83 Q923.462 1525.22 921.124 1523.11 Q918.786 1521.01 914.782 1521.01 Q912.907 1521.01 911.032 1521.42 Q909.18 1521.84 907.235 1522.72 L907.235 1505.36 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M1226.36 1508.44 Q1222.74 1508.44 1220.92 1512 Q1219.11 1515.55 1219.11 1522.67 Q1219.11 1529.78 1220.92 1533.35 Q1222.74 1536.89 1226.36 1536.89 Q1229.99 1536.89 1231.8 1533.35 Q1233.62 1529.78 1233.62 1522.67 Q1233.62 1515.55 1231.8 1512 Q1229.99 1508.44 1226.36 1508.44 M1226.36 1504.73 Q1232.17 1504.73 1235.22 1509.34 Q1238.3 1513.92 1238.3 1522.67 Q1238.3 1531.4 1235.22 1536.01 Q1232.17 1540.59 1226.36 1540.59 Q1220.55 1540.59 1217.47 1536.01 Q1214.41 1531.4 1214.41 1522.67 Q1214.41 1513.92 1217.47 1509.34 Q1220.55 1504.73 1226.36 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M1243.37 1534.04 L1248.25 1534.04 L1248.25 1539.92 L1243.37 1539.92 L1243.37 1534.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M1263.32 1508.44 Q1259.71 1508.44 1257.88 1512 Q1256.08 1515.55 1256.08 1522.67 Q1256.08 1529.78 1257.88 1533.35 Q1259.71 1536.89 1263.32 1536.89 Q1266.96 1536.89 1268.76 1533.35 Q1270.59 1529.78 1270.59 1522.67 Q1270.59 1515.55 1268.76 1512 Q1266.96 1508.44 1263.32 1508.44 M1263.32 1504.73 Q1269.13 1504.73 1272.19 1509.34 Q1275.27 1513.92 1275.27 1522.67 Q1275.27 1531.4 1272.19 1536.01 Q1269.13 1540.59 1263.32 1540.59 Q1257.51 1540.59 1254.43 1536.01 Q1251.38 1531.4 1251.38 1522.67 Q1251.38 1513.92 1254.43 1509.34 Q1257.51 1504.73 1263.32 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M1290.34 1508.44 Q1286.73 1508.44 1284.9 1512 Q1283.09 1515.55 1283.09 1522.67 Q1283.09 1529.78 1284.9 1533.35 Q1286.73 1536.89 1290.34 1536.89 Q1293.97 1536.89 1295.78 1533.35 Q1297.61 1529.78 1297.61 1522.67 Q1297.61 1515.55 1295.78 1512 Q1293.97 1508.44 1290.34 1508.44 M1290.34 1504.73 Q1296.15 1504.73 1299.2 1509.34 Q1302.28 1513.92 1302.28 1522.67 Q1302.28 1531.4 1299.2 1536.01 Q1296.15 1540.59 1290.34 1540.59 Q1284.53 1540.59 1281.45 1536.01 Q1278.39 1531.4 1278.39 1522.67 Q1278.39 1513.92 1281.45 1509.34 Q1284.53 1504.73 1290.34 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M1608.3 1508.44 Q1604.69 1508.44 1602.86 1512 Q1601.05 1515.55 1601.05 1522.67 Q1601.05 1529.78 1602.86 1533.35 Q1604.69 1536.89 1608.3 1536.89 Q1611.93 1536.89 1613.74 1533.35 Q1615.57 1529.78 1615.57 1522.67 Q1615.57 1515.55 1613.74 1512 Q1611.93 1508.44 1608.3 1508.44 M1608.3 1504.73 Q1614.11 1504.73 1617.16 1509.34 Q1620.24 1513.92 1620.24 1522.67 Q1620.24 1531.4 1617.16 1536.01 Q1614.11 1540.59 1608.3 1540.59 Q1602.49 1540.59 1599.41 1536.01 Q1596.35 1531.4 1596.35 1522.67 Q1596.35 1513.92 1599.41 1509.34 Q1602.49 1504.73 1608.3 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M1625.31 1534.04 L1630.2 1534.04 L1630.2 1539.92 L1625.31 1539.92 L1625.31 1534.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M1645.27 1508.44 Q1641.66 1508.44 1639.83 1512 Q1638.02 1515.55 1638.02 1522.67 Q1638.02 1529.78 1639.83 1533.35 Q1641.66 1536.89 1645.27 1536.89 Q1648.9 1536.89 1650.71 1533.35 Q1652.54 1529.78 1652.54 1522.67 Q1652.54 1515.55 1650.71 1512 Q1648.9 1508.44 1645.27 1508.44 M1645.27 1504.73 Q1651.08 1504.73 1654.13 1509.34 Q1657.21 1513.92 1657.21 1522.67 Q1657.21 1531.4 1654.13 1536.01 Q1651.08 1540.59 1645.27 1540.59 Q1639.46 1540.59 1636.38 1536.01 Q1633.32 1531.4 1633.32 1522.67 Q1633.32 1513.92 1636.38 1509.34 Q1639.46 1504.73 1645.27 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M1662.33 1505.36 L1680.68 1505.36 L1680.68 1509.3 L1666.61 1509.3 L1666.61 1517.77 Q1667.63 1517.42 1668.65 1517.26 Q1669.66 1517.07 1670.68 1517.07 Q1676.47 1517.07 1679.85 1520.24 Q1683.23 1523.42 1683.23 1528.83 Q1683.23 1534.41 1679.76 1537.51 Q1676.28 1540.59 1669.97 1540.59 Q1667.79 1540.59 1665.52 1540.22 Q1663.28 1539.85 1660.87 1539.11 L1660.87 1534.41 Q1662.95 1535.54 1665.17 1536.1 Q1667.4 1536.66 1669.87 1536.66 Q1673.88 1536.66 1676.22 1534.55 Q1678.55 1532.44 1678.55 1528.83 Q1678.55 1525.22 1676.22 1523.11 Q1673.88 1521.01 1669.87 1521.01 Q1668 1521.01 1666.12 1521.42 Q1664.27 1521.84 1662.33 1522.72 L1662.33 1505.36 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M1989.86 1508.44 Q1986.25 1508.44 1984.42 1512 Q1982.62 1515.55 1982.62 1522.67 Q1982.62 1529.78 1984.42 1533.35 Q1986.25 1536.89 1989.86 1536.89 Q1993.5 1536.89 1995.3 1533.35 Q1997.13 1529.78 1997.13 1522.67 Q1997.13 1515.55 1995.3 1512 Q1993.5 1508.44 1989.86 1508.44 M1989.86 1504.73 Q1995.67 1504.73 1998.73 1509.34 Q2001.81 1513.92 2001.81 1522.67 Q2001.81 1531.4 1998.73 1536.01 Q1995.67 1540.59 1989.86 1540.59 Q1984.05 1540.59 1980.97 1536.01 Q1977.92 1531.4 1977.92 1522.67 Q1977.92 1513.92 1980.97 1509.34 Q1984.05 1504.73 1989.86 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M2006.87 1534.04 L2011.76 1534.04 L2011.76 1539.92 L2006.87 1539.92 L2006.87 1534.04 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M2017.64 1535.98 L2025.28 1535.98 L2025.28 1509.62 L2016.97 1511.29 L2016.97 1507.03 L2025.23 1505.36 L2029.91 1505.36 L2029.91 1535.98 L2037.55 1535.98 L2037.55 1539.92 L2017.64 1539.92 L2017.64 1535.98 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M2052.62 1508.44 Q2049 1508.44 2047.18 1512 Q2045.37 1515.55 2045.37 1522.67 Q2045.37 1529.78 2047.18 1533.35 Q2049 1536.89 2052.62 1536.89 Q2056.25 1536.89 2058.06 1533.35 Q2059.88 1529.78 2059.88 1522.67 Q2059.88 1515.55 2058.06 1512 Q2056.25 1508.44 2052.62 1508.44 M2052.62 1504.73 Q2058.43 1504.73 2061.48 1509.34 Q2064.56 1513.92 2064.56 1522.67 Q2064.56 1531.4 2061.48 1536.01 Q2058.43 1540.59 2052.62 1540.59 Q2046.81 1540.59 2043.73 1536.01 Q2040.67 1531.4 2040.67 1522.67 Q2040.67 1513.92 2043.73 1509.34 Q2046.81 1504.73 2052.62 1504.73 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M62.9921 1227.3 L75.4689 1227.3 L75.4689 1231.09 L62.9921 1231.09 L62.9921 1227.3 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M90.5383 1210.7 Q86.9272 1210.7 85.0985 1214.27 Q83.2929 1217.81 83.2929 1224.94 Q83.2929 1232.04 85.0985 1235.61 Q86.9272 1239.15 90.5383 1239.15 Q94.1725 1239.15 95.9781 1235.61 Q97.8068 1232.04 97.8068 1224.94 Q97.8068 1217.81 95.9781 1214.27 Q94.1725 1210.7 90.5383 1210.7 M90.5383 1207 Q96.3484 1207 99.404 1211.6 Q102.483 1216.19 102.483 1224.94 Q102.483 1233.66 99.404 1238.27 Q96.3484 1242.85 90.5383 1242.85 Q84.7281 1242.85 81.6494 1238.27 Q78.5939 1233.66 78.5939 1224.94 Q78.5939 1216.19 81.6494 1211.6 Q84.7281 1207 90.5383 1207 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M107.552 1236.3 L112.436 1236.3 L112.436 1242.18 L107.552 1242.18 L107.552 1236.3 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M130.353 1211.7 L118.547 1230.15 L130.353 1230.15 L130.353 1211.7 M129.126 1207.62 L135.006 1207.62 L135.006 1230.15 L139.936 1230.15 L139.936 1234.03 L135.006 1234.03 L135.006 1242.18 L130.353 1242.18 L130.353 1234.03 L114.751 1234.03 L114.751 1229.52 L129.126 1207.62 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M65.0754 898.776 L77.5522 898.776 L77.5522 902.572 L65.0754 902.572 L65.0754 898.776 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M92.6216 882.179 Q89.0105 882.179 87.1818 885.744 Q85.3763 889.285 85.3763 896.415 Q85.3763 903.522 87.1818 907.086 Q89.0105 910.628 92.6216 910.628 Q96.2558 910.628 98.0614 907.086 Q99.8901 903.522 99.8901 896.415 Q99.8901 889.285 98.0614 885.744 Q96.2558 882.179 92.6216 882.179 M92.6216 878.475 Q98.4318 878.475 101.487 883.082 Q104.566 887.665 104.566 896.415 Q104.566 905.142 101.487 909.748 Q98.4318 914.332 92.6216 914.332 Q86.8114 914.332 83.7328 909.748 Q80.6772 905.142 80.6772 896.415 Q80.6772 887.665 83.7328 883.082 Q86.8114 878.475 92.6216 878.475 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M109.635 907.781 L114.52 907.781 L114.52 913.66 L109.635 913.66 L109.635 907.781 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M123.617 909.725 L139.936 909.725 L139.936 913.66 L117.992 913.66 L117.992 909.725 Q120.654 906.971 125.237 902.341 Q129.844 897.688 131.024 896.346 Q133.27 893.822 134.149 892.086 Q135.052 890.327 135.052 888.637 Q135.052 885.883 133.107 884.147 Q131.186 882.411 128.084 882.411 Q125.885 882.411 123.432 883.174 Q121.001 883.938 118.223 885.489 L118.223 880.767 Q121.047 879.633 123.501 879.054 Q125.955 878.475 127.992 878.475 Q133.362 878.475 136.557 881.161 Q139.751 883.846 139.751 888.336 Q139.751 890.466 138.941 892.387 Q138.154 894.285 136.047 896.878 Q135.469 897.549 132.367 900.767 Q129.265 903.961 123.617 909.725 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M91.0244 553.657 Q87.4133 553.657 85.5846 557.222 Q83.7791 560.764 83.7791 567.893 Q83.7791 575 85.5846 578.565 Q87.4133 582.106 91.0244 582.106 Q94.6586 582.106 96.4642 578.565 Q98.2929 575 98.2929 567.893 Q98.2929 560.764 96.4642 557.222 Q94.6586 553.657 91.0244 553.657 M91.0244 549.954 Q96.8345 549.954 99.8901 554.56 Q102.969 559.143 102.969 567.893 Q102.969 576.62 99.8901 581.227 Q96.8345 585.81 91.0244 585.81 Q85.2142 585.81 82.1355 581.227 Q79.08 576.62 79.08 567.893 Q79.08 559.143 82.1355 554.56 Q85.2142 549.954 91.0244 549.954 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M108.038 579.259 L112.922 579.259 L112.922 585.139 L108.038 585.139 L108.038 579.259 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M127.992 553.657 Q124.381 553.657 122.552 557.222 Q120.746 560.764 120.746 567.893 Q120.746 575 122.552 578.565 Q124.381 582.106 127.992 582.106 Q131.626 582.106 133.432 578.565 Q135.26 575 135.26 567.893 Q135.26 560.764 133.432 557.222 Q131.626 553.657 127.992 553.657 M127.992 549.954 Q133.802 549.954 136.857 554.56 Q139.936 559.143 139.936 567.893 Q139.936 576.62 136.857 581.227 Q133.802 585.81 127.992 585.81 Q122.182 585.81 119.103 581.227 Q116.047 576.62 116.047 567.893 Q116.047 559.143 119.103 554.56 Q122.182 549.954 127.992 549.954 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M92.6216 225.136 Q89.0105 225.136 87.1818 228.7 Q85.3763 232.242 85.3763 239.372 Q85.3763 246.478 87.1818 250.043 Q89.0105 253.585 92.6216 253.585 Q96.2558 253.585 98.0614 250.043 Q99.8901 246.478 99.8901 239.372 Q99.8901 232.242 98.0614 228.7 Q96.2558 225.136 92.6216 225.136 M92.6216 221.432 Q98.4318 221.432 101.487 226.038 Q104.566 230.622 104.566 239.372 Q104.566 248.099 101.487 252.705 Q98.4318 257.288 92.6216 257.288 Q86.8114 257.288 83.7328 252.705 Q80.6772 248.099 80.6772 239.372 Q80.6772 230.622 83.7328 226.038 Q86.8114 221.432 92.6216 221.432 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M109.635 250.737 L114.52 250.737 L114.52 256.617 L109.635 256.617 L109.635 250.737 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M123.617 252.682 L139.936 252.682 L139.936 256.617 L117.992 256.617 L117.992 252.682 Q120.654 249.927 125.237 245.298 Q129.844 240.645 131.024 239.302 Q133.27 236.779 134.149 235.043 Q135.052 233.284 135.052 231.594 Q135.052 228.839 133.107 227.103 Q131.186 225.367 128.084 225.367 Q125.885 225.367 123.432 226.131 Q121.001 226.895 118.223 228.446 L118.223 223.724 Q121.047 222.589 123.501 222.011 Q125.955 221.432 127.992 221.432 Q133.362 221.432 136.557 224.117 Q139.751 226.802 139.751 231.293 Q139.751 233.423 138.941 235.344 Q138.154 237.242 136.047 239.835 Q135.469 240.506 132.367 243.724 Q129.265 246.918 123.617 252.682 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><polyline clip-path="url(#clip4302)" style="stroke:#009af9; stroke-width:4; stroke-opacity:1; fill:none" points="
225.884,1445.72 246.05,1422.93 432.51,1224.98 544.566,1116.25 639.307,1029.77 742.222,941.098 837.101,863.918 938.822,785.736 1056.67,700.691 1161.41,629.791
1253.25,571.029 1353.38,510.402 1454.11,452.85 1565.48,393.02 1671.44,339.611 1781.62,287.529 1874.36,246.289 1987.6,199.017 2094.04,157.534 2264.56,96.7372
2290.81,87.9763
"/>
<path clip-path="url(#clip4300)" d="
M1989.74 251.724 L2280.76 251.724 L2280.76 130.764 L1989.74 130.764 Z
" fill="#ffffff" fill-rule="evenodd" fill-opacity="1"/>
<polyline clip-path="url(#clip4300)" style="stroke:#000000; stroke-width:4; stroke-opacity:1; fill:none" points="
1989.74,251.724 2280.76,251.724 2280.76,130.764 1989.74,130.764 1989.74,251.724
"/>
<polyline clip-path="url(#clip4300)" style="stroke:#009af9; stroke-width:4; stroke-opacity:1; fill:none" points="
2013.74,191.244 2157.74,191.244
"/>
<path clip-path="url(#clip4300)" d="M 0 0 M2195.58 210.931 Q2193.77 215.561 2192.06 216.973 Q2190.35 218.385 2187.48 218.385 L2184.08 218.385 L2184.08 214.82 L2186.58 214.82 Q2188.33 214.82 2189.31 213.987 Q2190.28 213.154 2191.46 210.052 L2192.22 208.107 L2181.74 182.598 L2186.25 182.598 L2194.35 202.876 L2202.46 182.598 L2206.97 182.598 L2195.58 210.931 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /><path clip-path="url(#clip4300)" d="M 0 0 M2212.85 204.589 L2220.49 204.589 L2220.49 178.223 L2212.18 179.89 L2212.18 175.631 L2220.44 173.964 L2225.12 173.964 L2225.12 204.589 L2232.76 204.589 L2232.76 208.524 L2212.85 208.524 L2212.85 204.589 Z" fill="#000000" fill-rule="evenodd" fill-opacity="1" /></svg>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>So it looks like that there is only one root of $g(s)$ on $[-e^{-2}, e^{2}]$. Is it true?</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [13]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="n">roots</span><span class="p">(</span><span class="n">g</span><span class="p">,</span> <span class="n">box</span><span class="p">)</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">
<div class="output_area">
<div class="prompt output_prompt">Out[13]:</div>
<div class="output_text output_subarea output_execute_result">
<pre>1-element Array{Root{Interval{Float64}},1}:
Root([-2.34965e-16, 1.79785e-16], :unique)</pre>
</div>
</div>
</div>
</div>
</div>
<div class="cell border-box-sizing text_cell rendered"><div class="prompt input_prompt">
</div><div class="inner_cell">
<div class="text_cell_render border-box-sizing rendered_html">
<p>Yes! And we know <em>analytically</em> that $g(0)=0$. So $0$ is the only root of $g$. That means if $g(e^{-2})> 0$, $g(s)$ must remain non-negative between $0$ and $e^{-2}$. Let's check</p>
</div>
</div>
</div>
<div class="cell border-box-sizing code_cell rendered">
<div class="input">
<div class="prompt input_prompt">In [14]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-julia"><pre><span></span><span class="n">b</span> <span class="o">=</span> <span class="nd">@interval</span> <span class="n">box</span><span class="o">.</span><span class="n">hi</span>
<span class="n">g</span><span class="p">(</span><span class="n">b</span><span class="p">)</span> <span class="o">>=</span> <span class="mi">0</span>
</pre></div>
</div>
</div>
</div>
<div class="output_wrapper">
<div class="output">