### A Pluto.jl notebook ###
# v1.0.3

using Markdown
using InteractiveUtils

# This Pluto notebook uses @bind for interactivity. When running this notebook outside of Pluto, the following 'mock version' of @bind gives bound variables a default value (instead of an error).
macro bind(def, element)
    #! format: off
    return quote
        local iv = try Base.loaded_modules[Base.PkgId(Base.UUID("6e696c72-6542-2067-7265-42206c756150"), "AbstractPlutoDingetjes")].Bonds.initial_value catch; b -> missing; end
        local el = $(esc(element))
        global $(esc(def)) = Core.applicable(Base.get, el) ? Base.get(el) : iv(el)
        el
    end
    #! format: on
end

# ╔═╡ 48796a9c-7802-4a7f-90cd-f46c3d907739
using RadiiPolynomial, LinearAlgebra, PlutoUI

# ╔═╡ d8fb42e3-9375-4384-ade4-b9696bdc602f
md"""
# Practical Considerations for Validated Numerics (૭ ｡•̀ ᵕ •́｡ )૭ᕙ

Olivier Hénot

National Taiwan University

[github.com/OlivierHnt/RadiiPolynomial.jl](https://github.com/OlivierHnt/RadiiPolynomial.jl)
"""

# ╔═╡ 4831623b-fa2d-4be3-b2bd-9b12345a940c
md"""
## Pluto notebook

1. Install Julia: [juliaup](https://github.com/julialang/juliaup) or [julialang.org/downloads](https://julialang.org/downloads) 
2. In a Julia REPL
```julia
using Pkg; Pkg.add("Pluto")
using Pluto; Pluto.run()
```
3. Open this file

*Nota bene*

- **reactive cells** (order on screen $\ne$ order of execution)
- **one statement per cell** (or use `begin ... end` / `let ... end`).
"""

# ╔═╡ 31cd8c18-c40d-4485-858f-29458fd460c4
TableOfContents(title = "Contents", depth = 2)

# ╔═╡ e2d66180-59da-4717-8a00-0ac0f98ffe72
md"""
## Goal

##### (Hopefully) get a better sense of how to validate numerics

##### 👉 Ask questions at any point!
"""

# ╔═╡ 079a81d9-311f-4e73-b0a4-6d2014704db9
md"""
## Context

**Numerical.** a computer... computes numbers... and these verify the hypotheses of a theorem (interval arithmetic, fixed-point theorems in Banach spaces, a posteriori validation)

**Formal.** a computer checks that every inference in the formal proof is valid (Coq / Lean)

| Step | Potential issue | Fix |
|------|----------|----------|
| the theorem | the argument itself | derivation → Coq / Lean |
| the arithmetic | rounding | floats → interval arithmetic |
| the code | it computes something else | tests → verified code |
| | compiler | assumed → certified compiler |

👉 Achieve different levels of certification
"""

# ╔═╡ 0bb7d68c-9a0e-4bc5-a6bd-1f260abbe716
md"""
## Example

`IntervalArithmetic` allows us to change the rounding strategy:
- `:none`, no rounding control at all **(not rigorous)**
- `:ulp`, bound each operation by one ulp (cheaper but less tight, still rigorous)
- `:correct`, correctly rounded *(default)*
"""

# ╔═╡ fa137974-b3e7-4b5b-8161-466dd182d991
begin
	IntervalArithmetic.configure(; rounding = :none)
	@eval diam( log(interval(2)^interval(3.2)) )   # @eval because of Pluto
end

# ╔═╡ 294a9cc3-9b81-466a-8c05-7d4d7a33aa1c
begin
	IntervalArithmetic.configure(; rounding = :ulp)
	@eval diam( log(interval(2)^interval(3.2)) )   # @eval because of Pluto
end

# ╔═╡ ba6bb7cb-1f4c-42ac-aa69-dfd41647fbbe
begin
	IntervalArithmetic.configure(; rounding = :correct)
	@eval diam( log(interval(2)^interval(3.2)) )   # @eval because of Pluto
end

# ╔═╡ 2acd5716-1526-4b14-87f7-fad3ca5f909c
md"""
## Rounding error might also not dominate

```math
f(x) = \frac{\sin(x) + e^x}{1 + x^2}
```
"""

# ╔═╡ 425d72ea-cdbe-4e84-8fcb-45f33c1c0d9c
f_wide(x) = (sin(x) + exp(x))^3 / (1 + x^2)

# ╔═╡ f46e0154-bdfd-4571-b403-01a5bc6422bb
bounds(f_wide(interval(0.5, 0.6)))

# ╔═╡ 3084e068-167c-48e3-9d82-0b37e774c5ab
inf(f_wide(interval(0.5))), sup(f_wide(interval(0.6)))

# ╔═╡ 9585eb68-632f-495a-b8c2-5a302683af5f
md"""
👉 the **formulation** of the problem matters!
"""

# ╔═╡ f1cb2d7d-3b57-41fe-9af5-2ab3d17ff559
md"""
## `exact`

Interval arithmetic has to know whether a literal is the number you *meant*
"""

# ╔═╡ 77e6f495-37c1-4d84-a211-405343866518
without_exact = interval(1.26)^3 - 2

# ╔═╡ d2c3b4de-044b-4398-b7b2-8ade6b8de82e
with_exact = interval(1.26)^3 - exact(2)

# ╔═╡ 82855ad9-8ef4-47db-b2f0-ec8531ff810f
isguaranteed(without_exact), isguaranteed(with_exact)

# ╔═╡ 1ca187f3-2124-4ef9-ba24-e9622e89980e
md"""
The `_NG` suffix means **not guaranteed**. In the above, `2` entered the computation as a value whose provenance cannot be vouched for

`exact(2)` asserts that the literal is exactly the quantity intended
"""

# ╔═╡ 24298937-2f40-4819-bde2-a2c867c26c97
md"""
**CAUTION:** `exact(0.1)` is *not* one tenth, it is the `Float64` nearest to `0.1`

For ``1/10`` write `interval(1)/interval(10)`. In the validation `exact(0.5)` is safe, one half
is a dyadic rational

👉 check `isguaranteed` on the final bound before believing a proof
"""

# ╔═╡ 89e1d6f0-c97e-4c66-8b97-3b288017e013
exact(0.1)

# ╔═╡ 1fff7ef6-f3fa-475b-a68d-2df824a61d35
exact(1) + (0.0)

# ╔═╡ 57792c0a-c9ab-4ab9-a4a1-4792db07122a
md"""
## Scope

Interval arithmetic encloses a **number** ... we want to enclose a **function**

##### First look at a validation

We prove that the initial value problem

```math
\dot{u}(t) = u(t)(1 - u(t)), \qquad
u(0) = 1/2,
```

has an analytic solution near a polynomial approximation. A solution is a zero of

```math
[F(u)](t) = u(t) - \frac{1}{2} - \int_0^t u(s)(1-u(s)) \, \mathrm{d}s.
```
"""

# ╔═╡ bcf6acba-683c-4d55-a2e0-66611e2f1539
begin
	# vector field and Jacobian
	f(u)  = u * (exact(1) - u)
	Df(u) = exact(1) - exact(2) * u
		
	# IVP as a zero-finding problem
	F(u, f)   = u - exact(0.5) - Integral(1) * f
	DF(u, Df) = exact(I) - Integral(1) * Multiplication(Df)
	
	# approximate solution
	K = 20
	u_guess = zeros(Taylor(K))
	u_bar, converged = newton(u -> (F(u, f(u)), DF(u, Df(u))), u_guess)
	Π = Projection(Taylor(K))

	# approximate inverse
	A_finite = inv(Π * DF(u_bar, Df(u_bar)) * Π)
	
	# bounds, with interval arithmetic
	ν   = interval(2)
	X   = Ell1(GeometricWeight(ν))
	u_i = interval(u_bar)
	A_i = interval(A_finite) + (interval(I) - interval(Π))
	opnormA = max(opnorm(interval(A_finite), X), exact(1))
	#-
	Y = norm(A_i * F(u_i, f(u_i)), X)
	#-
	r_s    = 10sup(Y)
	u_inf  = InfiniteSequence(u_i, X; total_error = interval(r_s))
	Df_inf = Df(u_inf)
	Df_bar, r_Df = sequence(Df_inf), total_error(Df_inf)
	Π₊  = Projection(Taylor(K+1))
	Z₁  = opnorm((exact(I) - A_i * DF(u_i, Df_bar)) * Π₊, X) + opnormA * ν * r_Df
	
	# check the hypotheses of the Radii Polynomial Theorem
	ie, proved = interval_of_existence(Y, Z₁, r_s)
	inf(ie), proved
end

# ╔═╡ ee701aaa-c54a-4801-abeb-8a858cbc80a1
if proved
	Markdown.MD(Markdown.Admonition("correct", "Theorem", [md"""
	There is an analytic solution of the initial value problem within **$(inf(ie))** of
	`u_bar` in the ``\ell^1_\nu`` norm.
	"""]))
else
	Markdown.MD(Markdown.Admonition("danger", "Not proved", [md"The hypotheses were not met."]))
end

# ╔═╡ 69de5796-ee5b-4d02-9ad3-3076d962f59e
md"""
## A posteriori validation method

1. **Formulation.** Reduce the problem to ``F(u) = 0`` in a Banach space and pick the
   fixed-point operator ``G(u) = u - A F(u)``.
2. **Approximation (floats).** Get ``\bar u`` and ``A \approx DF(\bar u)^{-1}``.
3. **Bounds (interval arithmetic).** Pick ``r_\star \ge 0`` and compute ``Y, Z_1`` such that
   ```math
   \|A F(\bar u)\| \le Y, \qquad \sup_{u \in B(\bar u, r_\star)} \|I - A \, DF(u)\| \le Z_1.
   ```
4. **Conclusion.** If ``Z_1 < 1``, ``A`` is injective and ``r \coloneqq Y/(1 - Z_1) \le r_\star``, then the Banach Fixed-Point Theorem gives a unique zero of ``F`` in ``B(\bar u, r)``.
"""

# ╔═╡ 8010d077-9436-437c-aaa1-fe8eb7fb8d09
md"""
# 1. Framework
"""

# ╔═╡ 5693d21a-8975-4737-863b-102833bf5c83
md"""
## Vector spaces

A `VectorSpace` says **which coefficients exist**

```
VectorSpace
├─ CartesianSpace (× and ^)
├─ ScalarSpace
└─ SequenceSpace
   ├─ BaseSpace   (Taylor, Fourier, Chebyshev)
   └─ TensorSpace (⊗)
```

**Observation:** It carries no topology at all
- no question of convergence since only finitely many coefficients
- the norm is adjusted several times to validate a solution
"""

# ╔═╡ 46e107b0-a942-4d71-ab78-a723cbfb8861
md"""
## Model spaces

**`Taylor(K)`** is the span of ``\phi_k(t) = t^k`` for ``k = 0,\dots,K``

👉 useful for local analytic functions
"""

# ╔═╡ 350c9e95-ce2a-46fe-ab9e-d498fa8b9bf8
Taylor(3), dimension(Taylor(3)), indices(Taylor(3))

# ╔═╡ 679a5aae-fc60-4dbc-8314-3cb0d58b27af
md"""
**`Fourier(K, ω)`** is the span of ``\phi_k(t) = e^{i \omega k t}`` for ``k = -K,\dots,K``

👉 useful for periodic functions
"""

# ╔═╡ 348d5df8-b567-476a-beb1-fe6e939abd93
Fourier(2, 1.0), dimension(Fourier(2, 1.0)), indices(Fourier(2, 1.0))

# ╔═╡ 12fca3d3-810a-4b66-9921-a6738c832d4f
md"""
**`Chebyshev(K)`** is the span of $\phi_k(t) = T_k(t)$ for ``k = 0,\dots,K``

**CAUTION:** the stored ``\{a_0, a_1, a_2 \dots\}`` correspond to standard Chebyshev coefficients ``\{a_0, 2a_1, 2a_2, \dots\}``.

👉 useful for functions defined on whole segment

"""

# ╔═╡ 322aab35-dd31-4494-9924-f1d4fb48106d
Chebyshev(3), dimension(Chebyshev(3)), indices(Chebyshev(3))

# ╔═╡ cc6f0c84-3013-4d21-b804-d9eb8a69c7f8
md"""
## More dimensions

`⊗` (`\otimes<tab>`) builds a **tensor** space modelling functions of several variables

`×` (`\times<tab>`) and `^` build **cartesian** spaces modelling systems
"""

# ╔═╡ 04249be4-7b62-4300-9404-18e46cd73ef0
Taylor(2) ⊗ Fourier(1, 1.0)

# ╔═╡ e6257c2e-036e-4cff-be55-dcb9a45c2f93
collect(indices(Taylor(2) ⊗ Fourier(1, 1.0)))

# ╔═╡ 2aa5793f-bf8a-433e-a927-6a2711449d41
ScalarSpace() × Taylor(2)^2

# ╔═╡ e0ee8939-4765-499a-98af-5fa5d84df524
indices(ScalarSpace() × Taylor(2)^2)

# ╔═╡ 7aab7c62-3527-485e-90e5-d2c0bbb383b2
md"""
## Sequences

A `Sequence` is a space together with coefficients.

Indexing follows the indices of the space.
"""

# ╔═╡ 544c84f4-a782-4e2e-8acb-efb405a138b0
one_t² = Sequence(Taylor(2), [1.0, 0.0, 1.0]) # t ↦ 1 + t²

# ╔═╡ 7e985c90-b7d9-4678-a2d0-f72e52b9436b
one_t²[0], one_t²[2], one_t²(0.5), 1+0.5^2

# ╔═╡ 85fd0164-0ee5-42ed-a8ea-1a40d8aa9f83
cos_seq = Sequence(Fourier(1, 1.0), [0.5, 0.0, 0.5]) # t ↦ (exp(i t) + exp(-i t))/2

# ╔═╡ ef39921e-ff8e-4c3f-ab63-2d2ed6960e81
cos_seq[-1], cos_seq[0], cos_seq(0.3), cos(0.3)

# ╔═╡ 4709ca0f-075a-4aab-9322-45fdc383af60
md"""
`to_coef` interpolates a function at the grid points associated with the space.
"""

# ╔═╡ ab6c4925-5fa4-45ab-939e-b9765856b8df
exp_cheb = to_coef(t -> exp(t), Chebyshev(10))

# ╔═╡ 69bf6a13-7b7a-4fd6-8fe2-ef3c7aa40aa1
real(exp_cheb(0.3)) - exp(0.3)

# ╔═╡ baeec1a6-890f-4c3c-8c9e-4b05a357267b
md"""
## Norms

A `BanachSpace` specifies **how to measure**

```
BanachSpace  (Ell1, Ell2, EllInf, NormedCartesianSpace)
```

`norm` takes a `Sequence` **and** a `BanachSpace`
"""

# ╔═╡ ef944a89-309d-431f-8f93-fa5d8bd5f57f
one_t_t² = Sequence(Taylor(2), [1.0, 1.0, 1.0])

# ╔═╡ 7717fa25-187d-4c73-a081-9d3d430b0a77
norm(one_t_t², Ell1()), norm(one_t_t², Ell2()), norm(one_t_t², EllInf())

# ╔═╡ 9b04ae37-695a-4962-8f7c-8b96f8716aa8
md"""
We can add a **weight**

```
Weight       (IdentityWeight, GeometricWeight, AlgebraicWeight, BesselWeight)
```
"""

# ╔═╡ 66f645f9-9e95-43ba-ad40-731638036b87
norm(one_t_t², Ell1(GeometricWeight(2.0)))

# ╔═╡ 89a357c1-1035-4c0a-8a9f-cc2af519edb6
md"""
The weighted ``\ell^1`` norm

```math
\|a\|_{\ell^1_\nu} = \sum_k |a_k| \nu^{|k|}
```

is an important one as ``\|a\|_{\ell^1_\nu} < \infty`` guarantees analyticity.

**Example.**
For a Taylor series, ``\sum_k |a_k| \nu^k < \infty`` says the series converges on a disc of radius ``\nu``.

`geometricweight` reads the observed decay rate straight off a numerical solution.
"""

# ╔═╡ f6477d9f-3653-4efd-acab-8032db5cc412
observed_rate = rate(geometricweight(u_bar))

# ╔═╡ 73f000f1-a046-453c-a7d2-abbfe6531972
md"""
Our solution is ``u(t) = 1/(1+e^{-t})``, whose poles are at ``t = \pm i\pi, \pm 3i\pi, \dots``.
The nearest is at distance ``\pi``.

**The decay rate of the numerically computed Taylor coefficients detects the singularity of a function.**
"""

# ╔═╡ 0121e789-66c7-431d-a332-02fdfb3f101e
md"""
## Infinite sequences

```math
u = \underbrace{\bar u}_{\text{stored}}
  + \underbrace{(\Pi_K u - \bar u)}_{\text{finite error}}
  + \underbrace{(I - \Pi_K) u}_{\text{tail}}
```

where ``\Pi_K`` truncates to a sequence of order ``K``.

`InfiniteSequence` bundles
- `Sequence`
- `Ell1(::Weight)`
- `finite_error` which bounds ``\|\Pi_K u - \bar u\|``
- `tail_error` which bounds ``\|(I - \Pi_K) u\|``
- **AND** `total_error` for the case where the error cannot be attributed to either part
"""

# ╔═╡ e12188ba-5b8a-4107-ba99-b8514409f70d
X_geo = Ell1(GeometricWeight(interval(1.2)))

# ╔═╡ ccca795a-1fc1-466c-90e9-6e63d617bd26
u_∞ = InfiniteSequence(Sequence(Taylor(6), interval.([0.5, 0.1, 0.01, 0, 0, 0, 0])), X_geo)

# ╔═╡ 06e2a684-1d2e-42c3-8929-240d035f9d01
exp_∞ = exp(u_∞)

# ╔═╡ 583ee905-b0c1-4056-8c5b-33ea844472a9
finite_error(exp_∞), tail_error(exp_∞), total_error(exp_∞)

# ╔═╡ 22bbf71a-0cbd-464e-83dc-21ec8eb75ea1
md"""
# ⏸
"""

# ╔═╡ ec5c92d6-9328-44c0-937c-6d365d93d85c
md"""
# 2. Operations and nonlinearities
"""

# ╔═╡ 0acf47ec-2403-43ef-b47e-236763e46fac
md"""
## Basic operations
"""

# ╔═╡ 2c80e517-170b-4d97-83a8-d8de893341ab
Sequence(Taylor(1), [0.0, 1.0]) + Sequence(Taylor(3), [1.0, 2.0, 1.0, 0.5])

# ╔═╡ f8fda321-500d-4c06-9f2a-5428428d480e
md"""
## Multiplication

Product of series correspond to a **discrete convolution** ``u(t) v(t) = (u*v)(t)`` where

```math
\begin{alignat}{2}
(u * v)_k &= \sum_{j=0}^k u_j v_{k-j}, \quad &&k \ge 0 \qquad \text{(Taylor)} \\
(u * v)_k &= \sum_{j \in \mathbb{Z}} u_j v_{k-j}, \quad &&k \in \mathbb{Z} \qquad \text{(Fourier)}\\
(u * v)_k &= \sum_{j \in \mathbb{Z}} u_{|j|} v_{|k-j|}, \quad &&k \ge 0 \qquad \text{(Chebyshev)}
\end{alignat}
```
"""

# ╔═╡ 22a27c6b-16d7-41de-879e-1cdd17546c53
poly_a = Sequence(Taylor(3), [1.0, -0.5, 0.25, -0.125]);

# ╔═╡ fdffe33e-7f1f-447f-8271-e3699c73384f
poly_b = Sequence(Taylor(4), [2.0, 1.0, -0.5, 0.5, 1.0]);

# ╔═╡ 6551cdb1-6395-463f-b78d-2a1b1c92335e
poly_a * poly_b

# ╔═╡ f7bb08b1-b2ca-4792-bdef-5fc6602abcf6
poly_a_∞, poly_b_∞ = InfiniteSequence(poly_a, Ell1()), InfiniteSequence(poly_b, Ell1());

# ╔═╡ 63bb01a1-6b07-4c42-80a2-54708d1d10ae
poly_a_∞ * poly_b_∞

# ╔═╡ a90b7ff4-1938-4c04-837f-34a3b66074ae
md"""
## Nonlinearities

### Algebraic

Some algebraic nonlinearities are handled by using the a posteriori validation method.

For instance, the square root of ``v`` is obtained by finding a zero of

```math
0 = F(u) \coloneqq u^{*2} - v
```
"""

# ╔═╡ fa908908-7044-4f5b-8325-410cb97d257b
four_ish = InfiniteSequence(Taylor(6), interval([4, 0.1, 0.01, 0, 0, 0, 0]), Ell1())

# ╔═╡ a70dabf1-d319-4a4a-8a09-4432f2c67019
sqrt(four_ish)

# ╔═╡ 6af0eebf-0e57-468b-a1ee-b42a0410aa5f
md"""
### General analytic nonlinearities

For an arbitrary analytic ``g``,
- we evaluate on a grid,
- transform back to coefficient space, and
- bound the error with Poisson summation formula + Cauchy estimate on a contour of radius ν

The structure `Nonlinearity` takes ``g`` together with its poles and branch cut
"""

# ╔═╡ 6653119f-3930-41d3-b666-b0260b67f521
md"""
**Example.**

```math
g(u) = \frac{1}{1 + u^{9.65}}
```

- the fractional power carries a **branch cut** along the negative reals
- **poles** are the solutions of ``u^{9.65} = -1``, which are on the unit circle at angles ``\pi(2k+1)/9.65``. Total of 10 satisfying ``\pi(2k+1)/9.65 \in (-π, π]``
"""

# ╔═╡ d2ff3f2a-6f30-4874-9c0d-d0509102d68c
p_exp = 9.65

# ╔═╡ 4f7d9e2f-b7dd-4ed6-b7a4-c70a9e0b16dd
g_poles = [cispi(interval((2k+1)/(193//20))) for k in -5:4]

# ╔═╡ e8fbddb2-fbdb-4a10-83fc-6df516e1dc74
pole_points = [mid(real(q)) + im*mid(imag(q)) for q in g_poles]

# ╔═╡ a1a32931-96fd-414d-815d-757927b27210
g = Nonlinearity(x -> inv(exact(1) + x^exact(193//20)), g_poles, interval(-Inf, 0))

# ╔═╡ 48f1b71c-93a6-4d4e-af2f-3b681b8f0c45
md"""
## Verifying no crossing

For a Chebyshev sequence the ``\ell^1_\nu`` norm corresponds to the **Bernstein ellipse**

```math
\mathbb{E}_\nu
\coloneqq
\left\{
\frac{1}{2}\left(w+w^{-1}\right)
\,:\,
1 \le |w| \le \nu
\right\}.
```
"""

# ╔═╡ a15b44b5-2823-4814-b3d9-be67043c88b0
md"""
scale = $(@bind u_scale Slider(0.4:0.1:1.4, default = 0.7, show_value = true))

shift = $(@bind u_shift Slider(-0.6:0.1:0.0, default = 0.0, show_value = true))
"""

# ╔═╡ 13d250b3-53b2-4496-aa33-83b1a930a07b
u_demo = real(to_coef(t -> u_shift + u_scale * (0.6 + 0.2t + 0.05t^3), Chebyshev(10)));

# ╔═╡ 8dc53841-1ba1-4268-ad95-90fc703e6274
g_of_u = try
	g(InfiniteSequence(interval(u_demo), Ell1(GeometricWeight(interval(2)))); codomain = Chebyshev(45))
catch err
	sprint(showerror, err)
end

# ╔═╡ 1f0a5954-a288-435a-8401-aa5c7171c3de
md"""
# ⏸
"""

# ╔═╡ 401a60c2-b074-46e6-8512-16792d68f4e8
md"""
# 3. Linear operators
"""

# ╔═╡ 75b7bb66-fa09-4f01-95bd-2220feb6c07e
md"""
## LinearOperator

Represent ``L : X \to Y``, where
- **domain** ``X`` as a `VectorSpace`
- **codomain** ``Y`` as a `VectorSpace`
- **coefficients** as a matrix
"""

# ╔═╡ 910e4b97-ef29-4725-86b3-91b35671d740
L_demo = LinearOperator(Taylor(1), Taylor(2), [1.0 2.0 ; 3.0 4.0 ; 5.0 6.0])

# ╔═╡ 68def751-770d-4ef6-acff-26ab9363740e
domain(L_demo), codomain(L_demo)

# ╔═╡ 09a0c075-b082-455a-8005-6bfec753cae9
L_demo * Sequence(Taylor(5), [1:6;])

# ╔═╡ 7af86038-572d-4787-957c-87515090f4d5
md"""
`opnorm` takes a `BanachSpace`, exactly like `norm`
"""

# ╔═╡ 064ef2c0-6725-47d1-bfe3-1528370cf97c
opnorm(L_demo, Ell1()), opnorm(L_demo, Ell1(GeometricWeight(2.0)))

# ╔═╡ 87f850d0-7e3c-4203-8019-5b226f41e397
L_demo + LinearOperator(Taylor(4), Taylor(0), [1.0 2.0 3.0 4.0 5.0])

# ╔═╡ 25af025f-608b-4b0b-b3cb-006e8b625a69
md"""
## Special operators
"""

# ╔═╡ ee8ec795-99e4-445c-bd53-e7e7b43b2c85
md"""
#### Projection

`Projection(s)` is the truncation ``\Pi`` onto `s`, a **rectangular identity**

```math
\Pi
=
\begin{pmatrix}
1      &        &        & 0      & \cdots \\
       & \ddots &        & \vdots &        \\
       &        & 1      & 0      & \cdots
\end{pmatrix}
```

👉 it acts on sequences and on operators alike
"""

# ╔═╡ a90b3b8f-a249-430e-9afc-e6f611efd5ec
Projection(Taylor(2)) * Sequence(Taylor(10), [1:11;])

# ╔═╡ 3998ef6c-7695-4338-8c5d-eae1b4403002
Projection(Taylor(3)) * LinearOperator(Taylor(1), Taylor(1), [1 2 ; 3 4])

# ╔═╡ a69d7624-0397-4e07-ac17-a336ff4bfac0
md"""
#### Multiplication

`Multiplication(a)` is the operator ``b \mapsto a * b``. In **every** space

```math
[\mathcal{M}(a)]_{k,j} = a_{k-j}, \qquad a_i \coloneqq 0 \text{ outside the range of } a
```

**Taylor** (``k, j \ge 0``) is lower triangular

```math
\mathcal{M}(a)
=
\begin{pmatrix}
a_0     &         &        \\
a_1     & a_0     &        \\
\vdots  & a_1     & \ddots \\
a_{K_a} & \vdots  & \ddots \\
        & a_{K_a} & \ddots \\
        &         & \ddots \\
        &         &        
\end{pmatrix}
```
"""

# ╔═╡ 8feaf874-7f8c-4405-994e-aeada1d61658
ℳ = Multiplication(Sequence(Taylor(1), [1.0, 2.0]))   # b ↦ (1 + 2t) * b

# ╔═╡ aa72aef9-5f57-4dfb-945d-9f848c850cd4
Projection(Taylor(3)) * ℳ

# ╔═╡ 4a7e7ff3-b8f3-4aeb-8828-6edf027676a2
md"""
**Fourier** (``k, j \in \mathbb{Z}``) has negative indices, so

```math
\mathcal{M}(a)
=
\begin{pmatrix}
\ddots&         &          &    \\
\ddots& a_{-K_a} &          &          \\
\ddots& \vdots   & a_{-K_a} &           \\
\ddots& a_0      & \vdots   & \ddots   \\
\ddots& \vdots   & a_0      & \ddots   \\
& a_{K_a}  & \vdots   & \ddots  \\
&          & a_{K_a}  & \ddots  \\
&          &          & \ddots   \\
\end{pmatrix}
```

👉 in both cases the codomain **grows** to ``K_a + K_b``
"""

# ╔═╡ f16decea-2303-42e8-a845-5ba8169667f8
ℳ_fourier = Multiplication(Sequence(Fourier(1, 1.0), [7.0, 10.0, 20.0]));

# ╔═╡ 634e84da-2c95-459e-be0e-b3dd37c2c7d3
Projection(Fourier(2, 1.0)) * ℳ_fourier

# ╔═╡ 674b7796-4755-4ed7-9a85-274938adb926
md"""
#### Derivation and integration

``\mathcal{D} t^j = j \, t^{j-1}`` on Taylor, so the matrix is the **superdiagonal** and the codomain **loses** an order

```math
\mathcal{D}
=
\begin{pmatrix}
0 & 1 &        &        &   \\
  & 0 & 2      &        &   \\
  &   & \ddots & \ddots &   \\
  &   &        & 0      & K
\end{pmatrix}
```

``\mathcal{D} e^{\mathrm{i}\omega k t} = \mathrm{i} \omega k \, e^{\mathrm{i}\omega k t}`` on
Fourier, so the matrix is **diagonal** and the codomain is **unchanged**

```math
\mathcal{D} = \mathrm{i}\omega \operatorname{diag}(-K, \dots, -1, 0, 1, \dots, K)
```
"""

# ╔═╡ 59a429e2-9f06-4421-a803-8f0d1567f76c
Derivative(1) * Projection(Taylor(3))

# ╔═╡ 00000000-0000-4000-8000-00000000d001
Derivative(1) * Projection(Fourier(2, 1.0))

# ╔═╡ b4141537-c406-48ee-a49f-e10487619f70
md"""
``\mathcal{I} t^j = \tfrac{1}{j+1} t^{j+1}``, so the matrix is the **subdiagonal** and the
codomain **gains** an order

```math
\mathcal{I}
=
\begin{pmatrix}
0 &               &        &        \\
1 & 0             &        &        \\
  & \tfrac{1}{2}  & 0      &        \\
  &               & \ddots & \ddots \\
  &               &        & \tfrac{1}{K+1}
\end{pmatrix}
```
"""

# ╔═╡ e457400a-5c38-4b6f-8025-964da6e5a96a
Integral(1) * Projection(Taylor(3))

# ╔═╡ 7fa12213-e850-4e27-8693-271de78bc2a5
Projection(Taylor(3)) * Integral(1)

# ╔═╡ 60f3e232-dbad-4f26-8881-af7930cda082
OP = Projection(Chebyshev(3)) * Integral(1)

# ╔═╡ bd2f8181-e4a9-4fef-ba18-e9585612a9a3
OP * Projection(Chebyshev(5))

# ╔═╡ 2849dc80-d12b-49d5-b2f5-578edaaf1b85
md"""
#### Evaluation, Shift, Scale

**`Evaluation(τ)`** evaluates the series associated with the sequence

```math
\mathcal{E}_\tau = \begin{pmatrix} 1 & \tau & \tau^2 & \cdots & \tau^K \end{pmatrix}
\qquad \text{(Taylor)}
```
"""

# ╔═╡ 65bddf7d-05e8-4697-8024-497d88607320
Evaluation(0.1) * Projection(Taylor(2))

# ╔═╡ 17d83cde-f46e-4f35-a73d-175eaedc2279
md"""
**`Shift(τ)`** sends ``u(t) \mapsto u(t+\tau)`` and **`Scale(γ)`** sends ``u(t) \mapsto u(\gamma t)``

```math
\mathcal{S}_\tau = \operatorname{diag}\left(e^{\mathrm{i}\omega k \tau}\right)_{k=-K}^{K}
\quad \text{(Fourier)}
\qquad\qquad
\mathcal{G}_\gamma = \operatorname{diag}\left(\gamma^{\,j}\right)_{j=0}^{K}
\quad \text{(Taylor)}
```
"""

# ╔═╡ 1d8ad739-afc7-4ad5-8057-e0ec653ecf18
shift(Sequence(Fourier(1, 1.0), [0.5, 0.0, 0.5]), π)

# ╔═╡ 0a6181de-0f1e-4f9b-bd0b-7d4c68e56afd
md"""
# ⏸
"""

# ╔═╡ 8dd0675c-ec01-4a2f-9633-5829580347d6
md"""
# 4. Back to the proof
"""

# ╔═╡ ddd5258a-5b92-4867-9991-f8a4efbab9a1
md"""
## The Banach space

Taylor coefficients of functions analytic on ``[-\nu, \nu]``

```math
\mathcal{T}_\nu
\coloneqq
\Big\{
u = \sum_{k \ge 0} u_k t^k
\ : \
\|u\|_\nu \coloneqq \sum_{k \ge 0} |u_k| \nu^k < \infty
\Big\}
```

- **Banach algebra**: ``\|u * v\|_\nu \le \|u\|_\nu \|v\|_\nu``, so nonlinearities are estimable
- the integral operator is bounded: ``\|\mathcal{I}\|_\nu \le \nu``

Integrating the initial value problem turns it into a zero-finding problem on ``\mathcal{T}_\nu``

```math
F(u) \coloneqq u - \tfrac{1}{2} - \mathcal{I} \, g(u),
\qquad
g(u) \coloneqq u(1-u)
```
"""

# ╔═╡ efb51058-ab2c-46a4-8537-c8c72f461d4d
md"""
## The bounds

``A \coloneqq A_K \Pi_{\le K} + \Pi_{>K}`` approximates ``DF(\bar u)^{-1}``, hence ``\|A\|_\nu = \max(\|A_K\|_\nu, 1)``

```math
Y \ge \|A F(\bar u)\|_\nu
\qquad\qquad
Z_1 \ge \sup_{u \in B(\bar u, r_\star)} \|I - A \, DF(u)\|_\nu
```

``Z_1`` needs one extra step. Since ``DF(u) = I - \mathcal{I}\mathcal{M}(Dg(u))``, split ``Dg`` on the
ball into its finite part and a remainder, ``Dg(u) = w + e`` with ``\|e\|_\nu \le r_{Dg}``, and set
``B \coloneqq I - \mathcal{I}\mathcal{M}(w)``

```math
I - A \, DF(u) = (I - A B) + A \, \mathcal{I} \, \mathcal{M}(e)
```

One triangle inequality, and both pieces are computable

```math
Z_1
=
\underbrace{\|(I - A B) \Pi_{\le K+1}\|_\nu}_{\text{a finite matrix}}
\; + \;
\underbrace{\|A\|_\nu \, \nu \, r_{Dg}}_{\text{the ball}}
```

👉 `InfiniteSequence(u_i, X; total_error = r_star)` **is** the ball ``B(\bar u, r_\star)``, and
`Df(u_inf)` propagates its radius into ``r_{Dg}``
"""

# ╔═╡ 7d1171b7-1650-4cb5-842a-63f7746daae6
md"""
## Now read it again

Every piece of the validation has now been introduced:

| in the proof | comes from |
|--------------|------------|
| `Taylor(K)`, `zeros` | Framework (vector spaces) |
| `Ell1(GeometricWeight(ν))`, `norm` | Framework (norms) |
| `InfiniteSequence`, `total_error` | Framework (infinite sequences) |
| `u * (exact(1) - u)` | Operations (Banach algebra) |
| `Integral`, `Multiplication` | Linear operators |
| `Projection`, `opnorm` | Linear operators |

👉 two numbers are chosen: ``K`` and ``\nu``
"""

# ╔═╡ c1a24c97-e5db-4c1a-bef3-7e373ff11706
md"""
## Explore

Move ``K`` and ``\nu``, and watch the validation succeed or fail
"""

# ╔═╡ 25e44615-f9e4-4133-9873-0ee1995f27bc
md"""
K = $(@bind K_live Slider(4:1:36, default = 27, show_value = true))

ν = $(@bind ν_live Slider(1.0:0.25:4.0, default = 2.0, show_value = true))
"""

# ╔═╡ e51342a8-f0ab-4aff-9b6a-0d8553ffaef4
function run_validation(K, νv)
	u_bar, _ = newton(u -> (F(u, f(u)), DF(u, Df(u))), zeros(Taylor(K)); verbose = false)
	Π   = Projection(Taylor(K))
	A_finite = inv(Π * DF(u_bar, Df(u_bar)) * Π)
	ν   = interval(νv)
	X   = Ell1(GeometricWeight(ν))
	u_i = interval(u_bar)
	A_i = interval(A_finite) + (interval(I) - interval(Π))
	opnormA = max(opnorm(interval(A_finite), X), exact(1))
	Y   = norm(A_i * F(u_i, f(u_i)), X)
	r_s = 10sup(Y)
	u_inf  = InfiniteSequence(u_i, X; total_error = interval(r_s))
	Df_inf = Df(u_inf)
	Df_bar, r_Df = sequence(Df_inf), total_error(Df_inf)
	Π₊  = Projection(Taylor(K+1))
	Z₁  = opnorm((exact(I) - A_i * DF(u_i, Df_bar)) * Π₊, X) + opnormA * ν * r_Df
	ie, ok = interval_of_existence(Y, Z₁, r_s)
	return (Y = sup(Y), Z₁ = sup(Z₁), proved = ok, bound = ok ? inf(ie) : NaN)
end

# ╔═╡ e34f0f11-96ff-4e13-b9ea-3815251710af
live_result = run_validation(K_live, ν_live)

# ╔═╡ 6a92030b-700e-4a42-a4d6-4135c8b6d5cd
let r = live_result
	body = md"""
	`Y` = $(r.Y)   ·   `Z₁` = $(r.Z₁)
	"""
	if r.proved
		Markdown.MD(Markdown.Admonition("correct",
			"Proved. Error ≤ $(r.bound) on |t| ≤ $(ν_live)", [body]))
	else
		Markdown.MD(Markdown.Admonition("danger", "Not proved", [body,
			md"`Z₁ ≥ 1`: `A` is not a good enough inverse, raise `K`. A large `Y`: `ν` is past the radius of convergence."]))
	end
end

# ╔═╡ fa56ea3f-aaf8-4dd2-be22-4dfaeab2896b
md"""
# ありがとうございました

[github.com/OlivierHnt/RadiiPolynomial.jl](https://github.com/OlivierHnt/RadiiPolynomial.jl)
"""

# ╔═╡ 00384a51-226e-49b6-9760-a3266d535018
md"""
## Appendix: plotting helpers

Small dependency-free SVG routines, so this notebook needs no plotting library dependency.
"""

# ╔═╡ 0e263c8a-dcfb-41c6-b358-cd3d78a8a3b0
function _axes_svg(W, H, pad, xlo, xhi, ylo, yhi, xlab, ylab, xticks, yticks, body)
	sx(x) = pad + (x - xlo) / (xhi - xlo) * (W - 1.6pad)
	sy(y) = H - pad - (y - ylo) / (yhi - ylo) * (H - 1.8pad)
	io = IOBuffer()
	print(io, """<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 $W $H" style="max-width:100%;height:auto;font-family:ui-sans-serif,system-ui,sans-serif">""")
	for (xv, lab) in xticks
		x = sx(xv)
		print(io, """<line x1="$x" y1="$(sy(ylo))" x2="$x" y2="$(sy(yhi))" stroke="currentColor" stroke-opacity="0.10"/>""")
		print(io, """<text x="$x" y="$(H-pad+16)" font-size="11" fill="currentColor" fill-opacity="0.65" text-anchor="middle">$lab</text>""")
	end
	for (yv, lab) in yticks
		y = sy(yv)
		print(io, """<line x1="$(sx(xlo))" y1="$y" x2="$(sx(xhi))" y2="$y" stroke="currentColor" stroke-opacity="0.10"/>""")
		print(io, """<text x="$(pad-8)" y="$(y+4)" font-size="11" fill="currentColor" fill-opacity="0.65" text-anchor="end">$lab</text>""")
	end
	print(io, """<line x1="$(sx(xlo))" y1="$(sy(ylo))" x2="$(sx(xhi))" y2="$(sy(ylo))" stroke="currentColor" stroke-opacity="0.45"/>""")
	print(io, """<line x1="$(sx(xlo))" y1="$(sy(ylo))" x2="$(sx(xlo))" y2="$(sy(yhi))" stroke="currentColor" stroke-opacity="0.45"/>""")
	print(io, body(sx, sy))
	print(io, """<text x="$(W/2)" y="$(H-4)" font-size="12" fill="currentColor" fill-opacity="0.8" text-anchor="middle">$xlab</text>""")
	print(io, """<text x="14" y="$(H/2)" font-size="12" fill="currentColor" fill-opacity="0.8" text-anchor="middle" transform="rotate(-90 14 $(H/2))">$ylab</text>""")
	print(io, "</svg>")
	return String(take!(io))
end

# ╔═╡ a298d6f4-5a17-40ce-9fb9-46ff688d1883
function decayplot(a; rates = (), W = 640, H = 320, floor_exp = -18)
	c = abs.(mid.(coefficients(a)))
	ks = 0:(length(c)-1)
	lg = [x == 0 ? float(floor_exp) : max(log10(x), float(floor_exp)) for x in c]
	xhi = maximum(ks)
	ylo, yhi = float(floor_exp), max(1.0, ceil(maximum(lg)))
	xticks = [(k, string(k)) for k in 0:max(1, xhi ÷ 5):xhi]
	yticks = [(e, "1e$(Int(e))") for e in ylo:4:yhi]
	body = function (sx, sy)
		io = IOBuffer()
		for ν in rates
			pts = join(["$(sx(k)),$(sy(clamp(log10(abs(c[1])) - k*log10(ν), ylo, yhi)))" for k in ks], " ")
			print(io, """<polyline points="$pts" fill="none" stroke="#e0655a" stroke-width="1.5" stroke-dasharray="5 3" opacity="0.85"/>""")
		end
		for (k, y) in zip(ks, lg)
			print(io, """<circle cx="$(sx(k))" cy="$(sy(y))" r="3" fill="currentColor" fill-opacity="$(c[k+1] == 0 ? 0.2 : 0.95)"/>""")
		end
		String(take!(io))
	end
	return _axes_svg(W, H, 52, 0, xhi, ylo, yhi, "coefficient index k", "log10(|a_k|)", xticks, yticks, body)
end

# ╔═╡ dac919ef-b6ca-4a82-a2e1-ff9e2d1e3718
HTML(decayplot(u_bar; rates = (observed_rate,)))

# ╔═╡ 79325a46-213f-46a7-8a63-c040dd53d0f0
# u on the Bernstein ellipse of parameter r: the Laurent sum Σ a_|k| z^k
bernstein_image(u, r; n = 240) =
	[sum(k == 0 ? u[0] : u[k]*(z^k + z^(-k)) for k in 0:order(space(u)))
	 for z in (r*cispi(2*(j-1)/n) for j in 1:n)]

# ╔═╡ a7752b35-eb52-4f3e-b718-ef3a70728c8d
image_curves(u, ν_cheb) = [bernstein_image(u, r) for r in range(1.0, ν_cheb; length = 9)]

# ╔═╡ 8107a78a-8647-47e4-a34b-a186603804f0
function argandplot(curves, poles; W = 560, lim = 1.45)
	s(x) = W/2 + x * (W/2 - 30) / lim          # equal aspect, origin centred
	t(y) = W/2 - y * (W/2 - 30) / lim
	io = IOBuffer()
	print(io, """<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 $W $W" style="max-width:100%;height:auto;font-family:ui-sans-serif,system-ui,sans-serif">""")
	print(io, """<line x1="$(s(-lim))" y1="$(t(0))" x2="$(s(0))" y2="$(t(0))" stroke="#e0655a" stroke-width="7" opacity="0.30" stroke-linecap="round"/>""")
	print(io, """<line x1="$(s(-lim))" y1="$(t(0))" x2="$(s(lim))" y2="$(t(0))" stroke="currentColor" stroke-opacity="0.35"/>""")
	print(io, """<line x1="$(s(0))" y1="$(t(-lim))" x2="$(s(0))" y2="$(t(lim))" stroke="currentColor" stroke-opacity="0.35"/>""")
	print(io, """<circle cx="$(s(0))" cy="$(t(0))" r="$(s(1)-s(0))" fill="none" stroke="currentColor" stroke-opacity="0.20" stroke-dasharray="4 4"/>""")
	for (i, c) in enumerate(curves)
		pts = join(["$(s(real(z))),$(t(imag(z)))" for z in c], " ")
		op = round(0.25 + 0.65*(i-1)/max(length(curves)-1, 1), digits = 2)
		print(io, """<polyline points="$pts" fill="none" stroke="#3b82c4" stroke-width="1.4" opacity="$op"/>""")
	end
	for q in poles
		x, y, d = s(real(q)), t(imag(q)), 5
		print(io, """<path d="M$(x-d) $(y-d)L$(x+d) $(y+d)M$(x-d) $(y+d)L$(x+d) $(y-d)" stroke="#e0655a" stroke-width="2.4"/>""")
	end
	print(io, """<text x="$(s(lim)-8)" y="$(t(0)-8)" font-size="12" fill="currentColor" fill-opacity="0.6" text-anchor="end">Re</text>""")
	print(io, """<text x="$(s(0)+8)" y="$(t(lim)+14)" font-size="12" fill="currentColor" fill-opacity="0.6">Im</text>""")
	print(io, "</svg>")
	return String(take!(io))
end

# ╔═╡ 8a4c4377-ec44-477f-bb40-db310c21f7ea
HTML(argandplot(image_curves(u_demo, 2.0), pole_points))

# ╔═╡ 2bf3e044-5853-4080-ae36-c91b2885a003
function curveplot(series; W = 640, H = 320, xlab = "t", ylab = "u(t)")
	xlo = minimum(minimum(s[1]) for s in series); xhi = maximum(maximum(s[1]) for s in series)
	ylo = minimum(minimum(s[2]) for s in series); yhi = maximum(maximum(s[2]) for s in series)
	pad = (yhi - ylo) * 0.08; ylo -= pad; yhi += pad
	xticks = [(x, string(round(x, digits = 2))) for x in range(xlo, xhi; length = 5)]
	yticks = [(y, string(round(y, digits = 2))) for y in range(ylo, yhi; length = 5)]
	body = function (sx, sy)
		io = IOBuffer()
		for (n, s) in enumerate(series)
			xs, ys, lab, col = s
			pts = join(["$(sx(x)),$(sy(y))" for (x, y) in zip(xs, ys)], " ")
			dash = n == 1 ? "" : " stroke-dasharray=\"6 4\""
			print(io, """<polyline points="$pts" fill="none" stroke="$col" stroke-width="2"$dash/>""")
			print(io, """<text x="$(W-190)" y="$(46 + 16n)" font-size="12" fill="$col">■ $lab</text>""")
		end
		String(take!(io))
	end
	return _axes_svg(W, H, 52, xlo, xhi, ylo, yhi, xlab, ylab, xticks, yticks, body)
end

# ╔═╡ 838a1207-47a3-42d1-82d9-ccd725c9551d
let ts = range(-2, 2; length = 200)
	HTML(curveplot([
		(collect(ts), [evaluate(u_bar, t) for t in ts], "u_bar (validated)", "#3b82c4"),
		(collect(ts), [1/(1+exp(-t)) for t in ts], "1/(1+exp(-t))", "#e0655a")]))
end

# ╔═╡ 00000000-0000-0000-0000-000000000001
PLUTO_PROJECT_TOML_CONTENTS = """
[deps]
LinearAlgebra = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e"
PlutoUI = "7f904dfe-b85e-4ff6-b463-dae2292396a8"
RadiiPolynomial = "f2081a94-c849-46b6-8dc9-07bb90ed72a9"

[compat]
PlutoUI = "~0.7.83"
RadiiPolynomial = "~0.11.5"
"""

# ╔═╡ 00000000-0000-0000-0000-000000000002
PLUTO_MANIFEST_TOML_CONTENTS = """
# This file is machine-generated - editing it directly is not advised

julia_version = "1.12.7"
manifest_format = "2.0"
project_hash = "60c74f300b58440ab992962635fd1380313d7c61"

[[deps.AbstractPlutoDingetjes]]
git-tree-sha1 = "e71ee7b4aa06b045259a7d6101e1cb45ad140bce"
uuid = "6e696c72-6542-2067-7265-42206c756150"
version = "1.4.1"

[[deps.ArgTools]]
uuid = "0dad84c5-d112-42e6-8d28-ef12dabb789f"
version = "1.1.2"

[[deps.Artifacts]]
uuid = "56f22d72-fd6d-98f1-02f0-08ddc0907c33"
version = "1.11.0"

[[deps.Base64]]
uuid = "2a0f44e3-6c83-55bd-87e4-b1978d98bd5f"
version = "1.11.0"

[[deps.CRlibm]]
deps = ["CRlibm_jll"]
git-tree-sha1 = "66188d9d103b92b6cd705214242e27f5737a1e5e"
uuid = "96374032-68de-5a5b-8d9e-752f78720389"
version = "1.0.2"

[[deps.CRlibm_jll]]
deps = ["Artifacts", "JLLWrappers", "Libdl", "Pkg"]
git-tree-sha1 = "e329286945d0cfc04456972ea732551869af1cfc"
uuid = "4e9b3aee-d8a1-5a3d-ad8b-7d824db253f0"
version = "1.0.1+0"

[[deps.ColorTypes]]
deps = ["FixedPointNumbers", "Random"]
git-tree-sha1 = "67e11ee83a43eb71ddc950302c53bf33f0690dfe"
uuid = "3da002f7-5984-5a60-b8a6-cbb66c0b333f"
version = "0.12.1"
weakdeps = ["StyledStrings"]

    [deps.ColorTypes.extensions]
    StyledStringsExt = "StyledStrings"

[[deps.CompilerSupportLibraries_jll]]
deps = ["Artifacts", "Libdl"]
uuid = "e66e0078-7015-5450-92f7-15fbd957f2ae"
version = "1.3.1+2"

[[deps.CoreMath]]
deps = ["CoreMath_jll"]
git-tree-sha1 = "8c0480f92b1b1796239156a1b9b1bfb1b39499b4"
uuid = "b7a15901-be09-4a0e-87d2-2e66b0e09b5a"
version = "0.1.0"

[[deps.CoreMath_jll]]
deps = ["Artifacts", "JLLWrappers", "Libdl"]
git-tree-sha1 = "a692a4c1dc59a4b8bc0b6403876eb3250fde2bc3"
uuid = "a38c48d9-6df1-5ac9-9223-b6ada3b5572b"
version = "0.1.0+0"

[[deps.Dates]]
deps = ["Printf"]
uuid = "ade2ca70-3891-5945-98fb-dc099432e06a"
version = "1.11.0"

[[deps.Downloads]]
deps = ["ArgTools", "FileWatching", "LibCURL", "NetworkOptions"]
uuid = "f43a241f-c20a-4ad4-852c-f6b1247861c6"
version = "1.7.0"

[[deps.FileWatching]]
uuid = "7b1f6079-737a-58dc-b8bc-7a2ca5c1b5ee"
version = "1.11.0"

[[deps.FixedPointNumbers]]
deps = ["Random", "Statistics"]
git-tree-sha1 = "59af96b98217c6ef4ae0dfe065ac7c20831d1a84"
uuid = "53c48c17-4a7d-5ca2-90c5-79b7896eea93"
version = "0.8.6"

[[deps.Hyperscript]]
deps = ["Test"]
git-tree-sha1 = "179267cfa5e712760cd43dcae385d7ea90cc25a4"
uuid = "47d2ed2b-36de-50cf-bf87-49c2cf4b8b91"
version = "0.0.5"

[[deps.HypertextLiteral]]
deps = ["Tricks"]
git-tree-sha1 = "d1a86724f81bcd184a38fd284ce183ec067d71a0"
uuid = "ac1192a8-f4b3-4bfe-ba22-af5b92cd3ab2"
version = "1.0.0"

[[deps.IOCapture]]
deps = ["Logging", "Random"]
git-tree-sha1 = "0ee181ec08df7d7c911901ea38baf16f755114dc"
uuid = "b5f81e59-6552-4d32-b1f0-c071b021bf89"
version = "1.0.0"

[[deps.InteractiveUtils]]
deps = ["Markdown"]
uuid = "b77e0a4c-d291-57a0-90e8-8db25a27a240"
version = "1.11.0"

[[deps.IntervalArithmetic]]
deps = ["CRlibm", "CoreMath", "MacroTools", "OpenBLASConsistentFPCSR_jll", "Printf", "Random", "RoundingEmulator"]
git-tree-sha1 = "ff294afb9a15d31d8d7422da138844641a73135f"
uuid = "d1acc4aa-44c8-5952-acd4-ba5d80a2a253"
version = "1.0.11"

    [deps.IntervalArithmetic.extensions]
    IntervalArithmeticArblibExt = "Arblib"
    IntervalArithmeticDiffRulesExt = "DiffRules"
    IntervalArithmeticForwardDiffExt = "ForwardDiff"
    IntervalArithmeticIntervalSetsExt = "IntervalSets"
    IntervalArithmeticIrrationalConstantsExt = "IrrationalConstants"
    IntervalArithmeticLinearAlgebraExt = "LinearAlgebra"
    IntervalArithmeticRecipesBaseExt = "RecipesBase"
    IntervalArithmeticSparseArraysExt = "SparseArrays"

    [deps.IntervalArithmetic.weakdeps]
    Arblib = "fb37089c-8514-4489-9461-98f9c8763369"
    DiffRules = "b552c78f-8df3-52c6-915a-8e097449b14b"
    ForwardDiff = "f6369f11-7733-5829-9624-2563aa707210"
    IntervalSets = "8197267c-284f-5f27-9208-e0e47529a953"
    IrrationalConstants = "92d709cd-6900-40b7-9082-c6be49f344b6"
    LinearAlgebra = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e"
    RecipesBase = "3cdcf5f2-1ef4-517c-9805-6587b60abb01"
    SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf"

[[deps.JLLWrappers]]
deps = ["Artifacts", "Preferences"]
git-tree-sha1 = "7204148362dafe5fe6a273f855b8ccbe4df8173e"
uuid = "692b3bcd-3c85-4b1f-b108-f13ce0eb3210"
version = "1.8.0"

[[deps.JuliaSyntaxHighlighting]]
deps = ["StyledStrings"]
uuid = "ac6e5ff7-fb65-4e79-a425-ec3bc9c03011"
version = "1.12.0"

[[deps.LibCURL]]
deps = ["LibCURL_jll", "MozillaCACerts_jll"]
uuid = "b27032c2-a3e7-50c8-80cd-2d36dbcbfd21"
version = "0.6.4"

[[deps.LibCURL_jll]]
deps = ["Artifacts", "LibSSH2_jll", "Libdl", "OpenSSL_jll", "Zlib_jll", "nghttp2_jll"]
uuid = "deac9b47-8bc7-5906-a0fe-35ac56dc84c0"
version = "8.15.0+0"

[[deps.LibGit2]]
deps = ["LibGit2_jll", "NetworkOptions", "Printf", "SHA"]
uuid = "76f85450-5226-5b5a-8eaa-529ad045b433"
version = "1.11.0"

[[deps.LibGit2_jll]]
deps = ["Artifacts", "LibSSH2_jll", "Libdl", "OpenSSL_jll"]
uuid = "e37daf67-58a4-590a-8e99-b0245dd2ffc5"
version = "1.9.0+0"

[[deps.LibSSH2_jll]]
deps = ["Artifacts", "Libdl", "OpenSSL_jll"]
uuid = "29816b5a-b9ab-546f-933c-edad1886dfa8"
version = "1.11.3+1"

[[deps.Libdl]]
uuid = "8f399da3-3557-5675-b5ff-fb832c97cbdb"
version = "1.11.0"

[[deps.LinearAlgebra]]
deps = ["Libdl", "OpenBLAS_jll", "libblastrampoline_jll"]
uuid = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e"
version = "1.12.0"

[[deps.Logging]]
uuid = "56ddb016-857b-54e1-b83d-db4d58db5568"
version = "1.11.0"

[[deps.MIMEs]]
git-tree-sha1 = "c64d943587f7187e751162b3b84445bbbd79f691"
uuid = "6c6e2e6c-3030-632d-7369-2d6c69616d65"
version = "1.1.0"

[[deps.MacroTools]]
git-tree-sha1 = "1e0228a030642014fe5cfe68c2c0a818f9e3f522"
uuid = "1914dd2f-81c6-5fcd-8719-6d5c9610ff09"
version = "0.5.16"

[[deps.Markdown]]
deps = ["Base64", "JuliaSyntaxHighlighting", "StyledStrings"]
uuid = "d6f4376e-aef5-505a-96c1-9c027394607a"
version = "1.11.0"

[[deps.MozillaCACerts_jll]]
uuid = "14a3606d-f60d-562e-9121-12d972cd8159"
version = "2025.11.4"

[[deps.NetworkOptions]]
uuid = "ca575930-c2e3-43a9-ace4-1e988b2c1908"
version = "1.3.0"

[[deps.OpenBLASConsistentFPCSR_jll]]
deps = ["Artifacts", "CompilerSupportLibraries_jll", "JLLWrappers", "Libdl"]
git-tree-sha1 = "38a93f17e431141c6470bb67a88952a7c4f0e928"
uuid = "6cdc7f73-28fd-5e50-80fb-958a8875b1af"
version = "0.3.34+0"

[[deps.OpenBLAS_jll]]
deps = ["Artifacts", "CompilerSupportLibraries_jll", "Libdl"]
uuid = "4536629a-c528-5b80-bd46-f80d51c5b363"
version = "0.3.29+0"

[[deps.OpenSSL_jll]]
deps = ["Artifacts", "Libdl"]
uuid = "458c3c95-2e84-50aa-8efc-19380b2a3a95"
version = "3.5.6+0"

[[deps.Pkg]]
deps = ["Artifacts", "Dates", "Downloads", "FileWatching", "LibGit2", "Libdl", "Logging", "Markdown", "Printf", "Random", "SHA", "TOML", "Tar", "UUIDs", "p7zip_jll"]
uuid = "44cfe95a-1eb2-52ea-b672-e2afdf69b78f"
version = "1.12.1"

    [deps.Pkg.extensions]
    REPLExt = "REPL"

    [deps.Pkg.weakdeps]
    REPL = "3fa0cd96-eef1-5676-8a61-b3b8758bbffb"

[[deps.PlutoUI]]
deps = ["AbstractPlutoDingetjes", "Base64", "ColorTypes", "Dates", "Downloads", "FixedPointNumbers", "Hyperscript", "HypertextLiteral", "IOCapture", "InteractiveUtils", "Logging", "MIMEs", "Markdown", "Random", "Reexport", "URIs", "UUIDs"]
git-tree-sha1 = "e189d0623e7ce9c37389bac17e80aac3b0302e75"
uuid = "7f904dfe-b85e-4ff6-b463-dae2292396a8"
version = "0.7.83"

[[deps.PrecompileTools]]
deps = ["Preferences"]
git-tree-sha1 = "edbeefc7a4889f528644251bdb5fc9ab5348bc2c"
uuid = "aea7be01-6a6a-4083-8856-8a6e6704d82a"
version = "1.3.4"

[[deps.Preferences]]
deps = ["TOML"]
git-tree-sha1 = "8b770b60760d4451834fe79dd483e318eee709c4"
uuid = "21216c6a-2e73-6563-6e65-726566657250"
version = "1.5.2"

[[deps.Printf]]
deps = ["Unicode"]
uuid = "de0858da-6303-5e67-8744-51eddeeeb8d7"
version = "1.11.0"

[[deps.RadiiPolynomial]]
deps = ["IntervalArithmetic", "LinearAlgebra", "Printf", "Reexport", "StaticArrays"]
git-tree-sha1 = "a67b0f007b68e15a19e2061a9b348739596b7d56"
uuid = "f2081a94-c849-46b6-8dc9-07bb90ed72a9"
version = "0.11.5"

[[deps.Random]]
deps = ["SHA"]
uuid = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c"
version = "1.11.0"

[[deps.Reexport]]
git-tree-sha1 = "45e428421666073eab6f2da5c9d310d99bb12f9b"
uuid = "189a3867-3050-52da-a836-e630ba90ab69"
version = "1.2.2"

[[deps.RoundingEmulator]]
git-tree-sha1 = "40b9edad2e5287e05bd413a38f61a8ff55b9557b"
uuid = "5eaf0fd0-dfba-4ccb-bf02-d820a40db705"
version = "0.2.1"

[[deps.SHA]]
uuid = "ea8e919c-243c-51af-8825-aaa63cd721ce"
version = "0.7.0"

[[deps.Serialization]]
uuid = "9e88b42a-f829-5b0c-bbe9-9e923198166b"
version = "1.11.0"

[[deps.StaticArrays]]
deps = ["LinearAlgebra", "PrecompileTools", "Random", "StaticArraysCore"]
git-tree-sha1 = "e206cf4850fd7ac4255ffd2b98922f563e18ac53"
uuid = "90137ffa-7385-5640-81b9-e52037218182"
version = "1.9.20"

    [deps.StaticArrays.extensions]
    StaticArraysChainRulesCoreExt = "ChainRulesCore"
    StaticArraysStatisticsExt = "Statistics"

    [deps.StaticArrays.weakdeps]
    ChainRulesCore = "d360d2e6-b24c-11e9-a2a3-2a2ae2dbcce4"
    Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2"

[[deps.StaticArraysCore]]
git-tree-sha1 = "6ab403037779dae8c514bad259f32a447262455a"
uuid = "1e83bf80-4336-4d27-bf5d-d5a4f845583c"
version = "1.4.4"

[[deps.Statistics]]
deps = ["LinearAlgebra"]
git-tree-sha1 = "e2b53ce13a53367e96601081e33d34746b571bad"
uuid = "10745b16-79ce-11e8-11f9-7d13ad32a3b2"
version = "1.11.5"

    [deps.Statistics.extensions]
    SparseArraysExt = ["SparseArrays"]

    [deps.Statistics.weakdeps]
    SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf"

[[deps.StyledStrings]]
uuid = "f489334b-da3d-4c2e-b8f0-e476e12c162b"
version = "1.11.0"

[[deps.TOML]]
deps = ["Dates"]
uuid = "fa267f1f-6049-4f14-aa54-33bafae1ed76"
version = "1.0.3"

[[deps.Tar]]
deps = ["ArgTools", "SHA"]
uuid = "a4e569a6-e804-4fa4-b0f3-eef7a1d5b13e"
version = "1.10.0"

[[deps.Test]]
deps = ["InteractiveUtils", "Logging", "Random", "Serialization"]
uuid = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
version = "1.11.0"

[[deps.Tricks]]
git-tree-sha1 = "311349fd1c93a31f783f977a71e8b062a57d4101"
uuid = "410a4b4d-49e4-4fbc-ab6d-cb71b17b3775"
version = "0.1.13"

[[deps.URIs]]
git-tree-sha1 = "908fec9df6c5de98548ead82a468c95ccf6cd263"
uuid = "5c2747f8-b7ea-4ff2-ba2e-563bfd36b1d4"
version = "1.7.0"

[[deps.UUIDs]]
deps = ["Random", "SHA"]
uuid = "cf7118a7-6976-5b1a-9a39-7adc72f591a4"
version = "1.11.0"

[[deps.Unicode]]
uuid = "4ec0a83e-493e-50e2-b9ac-8f72acf5a8f5"
version = "1.11.0"

[[deps.Zlib_jll]]
deps = ["Libdl"]
uuid = "83775a58-1f1d-513f-b197-d71354ab007a"
version = "1.3.1+2"

[[deps.libblastrampoline_jll]]
deps = ["Artifacts", "Libdl"]
uuid = "8e850b90-86db-534c-a0d3-1478176c7d93"
version = "5.15.0+0"

[[deps.nghttp2_jll]]
deps = ["Artifacts", "Libdl"]
uuid = "8e850ede-7688-5339-a07c-302acd2aaf8d"
version = "1.64.0+1"

[[deps.p7zip_jll]]
deps = ["Artifacts", "CompilerSupportLibraries_jll", "Libdl"]
uuid = "3f19e933-33d8-53b3-aaab-bd5110c3b7a0"
version = "17.7.0+0"
"""

# ╔═╡ Cell order:
# ╟─d8fb42e3-9375-4384-ade4-b9696bdc602f
# ╟─4831623b-fa2d-4be3-b2bd-9b12345a940c
# ╠═48796a9c-7802-4a7f-90cd-f46c3d907739
# ╠═31cd8c18-c40d-4485-858f-29458fd460c4
# ╟─e2d66180-59da-4717-8a00-0ac0f98ffe72
# ╟─079a81d9-311f-4e73-b0a4-6d2014704db9
# ╟─0bb7d68c-9a0e-4bc5-a6bd-1f260abbe716
# ╠═fa137974-b3e7-4b5b-8161-466dd182d991
# ╠═294a9cc3-9b81-466a-8c05-7d4d7a33aa1c
# ╠═ba6bb7cb-1f4c-42ac-aa69-dfd41647fbbe
# ╟─2acd5716-1526-4b14-87f7-fad3ca5f909c
# ╠═425d72ea-cdbe-4e84-8fcb-45f33c1c0d9c
# ╠═f46e0154-bdfd-4571-b403-01a5bc6422bb
# ╠═3084e068-167c-48e3-9d82-0b37e774c5ab
# ╟─9585eb68-632f-495a-b8c2-5a302683af5f
# ╟─f1cb2d7d-3b57-41fe-9af5-2ab3d17ff559
# ╠═77e6f495-37c1-4d84-a211-405343866518
# ╠═d2c3b4de-044b-4398-b7b2-8ade6b8de82e
# ╠═82855ad9-8ef4-47db-b2f0-ec8531ff810f
# ╟─1ca187f3-2124-4ef9-ba24-e9622e89980e
# ╟─24298937-2f40-4819-bde2-a2c867c26c97
# ╠═89e1d6f0-c97e-4c66-8b97-3b288017e013
# ╠═1fff7ef6-f3fa-475b-a68d-2df824a61d35
# ╟─57792c0a-c9ab-4ab9-a4a1-4792db07122a
# ╠═bcf6acba-683c-4d55-a2e0-66611e2f1539
# ╟─ee701aaa-c54a-4801-abeb-8a858cbc80a1
# ╟─838a1207-47a3-42d1-82d9-ccd725c9551d
# ╟─69de5796-ee5b-4d02-9ad3-3076d962f59e
# ╟─8010d077-9436-437c-aaa1-fe8eb7fb8d09
# ╟─5693d21a-8975-4737-863b-102833bf5c83
# ╟─46e107b0-a942-4d71-ab78-a723cbfb8861
# ╠═350c9e95-ce2a-46fe-ab9e-d498fa8b9bf8
# ╟─679a5aae-fc60-4dbc-8314-3cb0d58b27af
# ╠═348d5df8-b567-476a-beb1-fe6e939abd93
# ╟─12fca3d3-810a-4b66-9921-a6738c832d4f
# ╠═322aab35-dd31-4494-9924-f1d4fb48106d
# ╟─cc6f0c84-3013-4d21-b804-d9eb8a69c7f8
# ╠═04249be4-7b62-4300-9404-18e46cd73ef0
# ╠═e6257c2e-036e-4cff-be55-dcb9a45c2f93
# ╠═2aa5793f-bf8a-433e-a927-6a2711449d41
# ╠═e0ee8939-4765-499a-98af-5fa5d84df524
# ╟─7aab7c62-3527-485e-90e5-d2c0bbb383b2
# ╠═544c84f4-a782-4e2e-8acb-efb405a138b0
# ╠═7e985c90-b7d9-4678-a2d0-f72e52b9436b
# ╠═85fd0164-0ee5-42ed-a8ea-1a40d8aa9f83
# ╠═ef39921e-ff8e-4c3f-ab63-2d2ed6960e81
# ╟─4709ca0f-075a-4aab-9322-45fdc383af60
# ╠═ab6c4925-5fa4-45ab-939e-b9765856b8df
# ╠═69bf6a13-7b7a-4fd6-8fe2-ef3c7aa40aa1
# ╟─baeec1a6-890f-4c3c-8c9e-4b05a357267b
# ╠═ef944a89-309d-431f-8f93-fa5d8bd5f57f
# ╠═7717fa25-187d-4c73-a081-9d3d430b0a77
# ╟─9b04ae37-695a-4962-8f7c-8b96f8716aa8
# ╠═66f645f9-9e95-43ba-ad40-731638036b87
# ╟─89a357c1-1035-4c0a-8a9f-cc2af519edb6
# ╠═f6477d9f-3653-4efd-acab-8032db5cc412
# ╟─73f000f1-a046-453c-a7d2-abbfe6531972
# ╟─dac919ef-b6ca-4a82-a2e1-ff9e2d1e3718
# ╟─0121e789-66c7-431d-a332-02fdfb3f101e
# ╠═e12188ba-5b8a-4107-ba99-b8514409f70d
# ╠═ccca795a-1fc1-466c-90e9-6e63d617bd26
# ╠═06e2a684-1d2e-42c3-8929-240d035f9d01
# ╠═583ee905-b0c1-4056-8c5b-33ea844472a9
# ╟─22bbf71a-0cbd-464e-83dc-21ec8eb75ea1
# ╟─ec5c92d6-9328-44c0-937c-6d365d93d85c
# ╟─0acf47ec-2403-43ef-b47e-236763e46fac
# ╠═2c80e517-170b-4d97-83a8-d8de893341ab
# ╟─f8fda321-500d-4c06-9f2a-5428428d480e
# ╠═22a27c6b-16d7-41de-879e-1cdd17546c53
# ╠═fdffe33e-7f1f-447f-8271-e3699c73384f
# ╠═6551cdb1-6395-463f-b78d-2a1b1c92335e
# ╠═f7bb08b1-b2ca-4792-bdef-5fc6602abcf6
# ╠═63bb01a1-6b07-4c42-80a2-54708d1d10ae
# ╟─a90b7ff4-1938-4c04-837f-34a3b66074ae
# ╠═fa908908-7044-4f5b-8325-410cb97d257b
# ╠═a70dabf1-d319-4a4a-8a09-4432f2c67019
# ╟─6af0eebf-0e57-468b-a1ee-b42a0410aa5f
# ╟─6653119f-3930-41d3-b666-b0260b67f521
# ╠═d2ff3f2a-6f30-4874-9c0d-d0509102d68c
# ╠═4f7d9e2f-b7dd-4ed6-b7a4-c70a9e0b16dd
# ╟─e8fbddb2-fbdb-4a10-83fc-6df516e1dc74
# ╠═a1a32931-96fd-414d-815d-757927b27210
# ╟─48f1b71c-93a6-4d4e-af2f-3b681b8f0c45
# ╠═13d250b3-53b2-4496-aa33-83b1a930a07b
# ╟─8a4c4377-ec44-477f-bb40-db310c21f7ea
# ╟─a15b44b5-2823-4814-b3d9-be67043c88b0
# ╠═8dc53841-1ba1-4268-ad95-90fc703e6274
# ╟─1f0a5954-a288-435a-8401-aa5c7171c3de
# ╟─401a60c2-b074-46e6-8512-16792d68f4e8
# ╟─75b7bb66-fa09-4f01-95bd-2220feb6c07e
# ╠═910e4b97-ef29-4725-86b3-91b35671d740
# ╠═68def751-770d-4ef6-acff-26ab9363740e
# ╠═09a0c075-b082-455a-8005-6bfec753cae9
# ╟─7af86038-572d-4787-957c-87515090f4d5
# ╠═064ef2c0-6725-47d1-bfe3-1528370cf97c
# ╠═87f850d0-7e3c-4203-8019-5b226f41e397
# ╟─25af025f-608b-4b0b-b3cb-006e8b625a69
# ╟─ee8ec795-99e4-445c-bd53-e7e7b43b2c85
# ╠═a90b3b8f-a249-430e-9afc-e6f611efd5ec
# ╠═3998ef6c-7695-4338-8c5d-eae1b4403002
# ╟─a69d7624-0397-4e07-ac17-a336ff4bfac0
# ╠═8feaf874-7f8c-4405-994e-aeada1d61658
# ╠═aa72aef9-5f57-4dfb-945d-9f848c850cd4
# ╟─4a7e7ff3-b8f3-4aeb-8828-6edf027676a2
# ╠═f16decea-2303-42e8-a845-5ba8169667f8
# ╠═634e84da-2c95-459e-be0e-b3dd37c2c7d3
# ╟─674b7796-4755-4ed7-9a85-274938adb926
# ╠═59a429e2-9f06-4421-a803-8f0d1567f76c
# ╠═00000000-0000-4000-8000-00000000d001
# ╟─b4141537-c406-48ee-a49f-e10487619f70
# ╠═e457400a-5c38-4b6f-8025-964da6e5a96a
# ╠═7fa12213-e850-4e27-8693-271de78bc2a5
# ╠═60f3e232-dbad-4f26-8881-af7930cda082
# ╠═bd2f8181-e4a9-4fef-ba18-e9585612a9a3
# ╟─2849dc80-d12b-49d5-b2f5-578edaaf1b85
# ╠═65bddf7d-05e8-4697-8024-497d88607320
# ╟─17d83cde-f46e-4f35-a73d-175eaedc2279
# ╠═1d8ad739-afc7-4ad5-8057-e0ec653ecf18
# ╟─0a6181de-0f1e-4f9b-bd0b-7d4c68e56afd
# ╟─8dd0675c-ec01-4a2f-9633-5829580347d6
# ╟─ddd5258a-5b92-4867-9991-f8a4efbab9a1
# ╟─efb51058-ab2c-46a4-8537-c8c72f461d4d
# ╟─7d1171b7-1650-4cb5-842a-63f7746daae6
# ╟─c1a24c97-e5db-4c1a-bef3-7e373ff11706
# ╟─25e44615-f9e4-4133-9873-0ee1995f27bc
# ╟─e51342a8-f0ab-4aff-9b6a-0d8553ffaef4
# ╠═e34f0f11-96ff-4e13-b9ea-3815251710af
# ╟─6a92030b-700e-4a42-a4d6-4135c8b6d5cd
# ╟─fa56ea3f-aaf8-4dd2-be22-4dfaeab2896b
# ╟─00384a51-226e-49b6-9760-a3266d535018
# ╟─0e263c8a-dcfb-41c6-b358-cd3d78a8a3b0
# ╟─a298d6f4-5a17-40ce-9fb9-46ff688d1883
# ╟─79325a46-213f-46a7-8a63-c040dd53d0f0
# ╟─a7752b35-eb52-4f3e-b718-ef3a70728c8d
# ╟─8107a78a-8647-47e4-a34b-a186603804f0
# ╟─2bf3e044-5853-4080-ae36-c91b2885a003
# ╟─00000000-0000-0000-0000-000000000001
# ╟─00000000-0000-0000-0000-000000000002