BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Jan Bouwe van den Berg (VU Amsterdam)
DTSTART:20200623T140000Z
DTEND:20200623T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/1
DESCRIPTION:Title: Stable periodic patterns in 3D for the Ohta-Kawasaki problem\nby Jan
Bouwe van den Berg (VU Amsterdam) as part of CRM CAMP (Computer-Assisted M
athematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nIn this talk we d
iscuss a mathematically rigorous computational method to compare local min
imizers of the Ohta-Kawasaki free energy\, describing diblock copolymer me
lts. This energy incorporates a nonlocal term to take into account the bon
d between the monomers.\nWorking within an arbitrary space group symmetry\
, we explore the phase space\, computing candidates both with and without
experimentally observed symmetries. We validate the phase diagram\, identi
fying regions of parameter space where different spatially periodic struct
ures have the lowest energy. These patterns may be lamellar layers\, hexag
onally packed cylinders\, body-centered or close-packed spheres\, as well
as double gyroids and 'O70' arrangements. Each computation is validated by
a mathematical theorem\, where we bound the truncation errors and apply a
fixed point argument to establish a computer-assisted proof. The method c
an be applied more generally to symmetric space-time periodic solution of
many partial differential equations.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jonathan Jaquette (Boston University)
DTSTART:20200630T140000Z
DTEND:20200630T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/2
DESCRIPTION:Title: An overabundance of breathers in a nonlinear Schrödinger equation withou
t gauge invariance\nby Jonathan Jaquette (Boston University) as part o
f CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n
\n\nAbstract\nIn this talk we study the nonlinear Schrödinger equation $i
u_t + \\triangle u + u^2 = 0$ posed on the 1-torus. Based on their numeri
cs\, Cho\, Okamoto\, & Shōji conjectured in their 2016 paper that: (C1) a
ny singularity in the complex plane of time arising from inhomogeneous ini
tial data is a branch singularity\, and (C2) real initial data will exist
globally in real time. If true\, Conjecture 1 would suggest a strong incom
patibility with the Painlevé property\, a property closely associated wit
h integrable systems. While Masuda proved (C1) in 1983 for close-to-consta
nt initial data\, a generalization to other initial data is not known. Usi
ng computer assisted proofs we establish a branch singularity in the compl
ex plane of time for specific\, large initial data which is not close-to-c
onstant.\n\nConcerning (C2)\, we demonstrate an open set of initial data w
hich is homoclinic to the 0-homogeneous-equilibrium\, proving (C2) for clo
se-to-constant initial data. This proof is then extended to a broader clas
s of nonlinear Schrödinger equation without gauge invariance\, and then u
sed to prove the non-existence of any real-analytic conserved quantities.
Indeed\, while numerical evidence suggests that most initial data is homoc
linic to the 0-equilibrium\, there is more than meets the eye. Using compu
ter assisted proofs\, we establish an infinite family of unstable nonhomog
eneous equilibria\, as well as heteroclinic orbits traveling between these
nonhomogeneous equilibria and the 0-equilibrium.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Michael Plum (Karlsruhe Institute of Technology)
DTSTART:20200707T140000Z
DTEND:20200707T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/3
DESCRIPTION:Title: Computer-assisted existence and multiplicity proofs for semilinear ellipt
ic problems on bounded and unbounded domains\nby Michael Plum (Karlsru
he Institute of Technology) as part of CRM CAMP (Computer-Assisted Mathema
tical Proofs) in Nonlinear Analysis\n\n\nAbstract\nMany boundary value pro
blems for semilinear elliptic partial differential equations allow very st
able numerical computations of approximate solutions\, but are still lacki
ng analytical existence proofs. In this lecture\, we propose a method whic
h exploits the knowledge of a "good" numerical approximate solution\, in o
rder to provide a rigorous proof of existence of an exact solution close t
o the approximate one. This goal is achieved by a fixed-point argument whi
ch takes all numerical errors into account\, and thus gives a mathematical
proof which is not "worse" than any purely analytical one. A crucial part
of the proof consists of the computation of eigenvalue bounds for the lin
earization of the given problem at the approximate solution. The method is
used to prove existence and multiplicity statements for some specific exa
mples\, including cases where purely analytical methods had not been succe
ssful.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Javier Gómez-Serrano (Brown University & University of Barcelona)
DTSTART:20200714T140000Z
DTEND:20200714T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/4
DESCRIPTION:Title: Uniqueness of Whitham's highest cusped wave\nby Javier Gómez-Serrano
(Brown University & University of Barcelona) as part of CRM CAMP (Compute
r-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nWhith
am’s equation of shallow water waves is a non-homogeneous non-local disp
ersive equation. As in the case of the Stokes wave for the Euler equation\
, non-smooth traveling waves with greatest height between crest and trough
have been shown to exist. In this talk I will discuss uniqueness of solut
ions to the Whitham equation and show that there exists a unique\, even an
d periodic traveling wave of greatest height\, that moreover has a convex
profile between consecutive stagnation points\, at which there is a cusp.
Joint work with Alberto Enciso and Bruno Vergara.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nilima Nigam (Simon Fraser University)
DTSTART:20200728T140000Z
DTEND:20200728T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/5
DESCRIPTION:Title: A modification of Schiffer's conjecture\, and a proof via finite elements
\nby Nilima Nigam (Simon Fraser University) as part of CRM CAMP (Compu
ter-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nApp
roximations via conforming and non-conforming finite elements can be used
to construct validated and computable bounds on eigenvalues for the Dirich
let Laplacian in certain domains. If these are to be used as part of a pro
of\, care must be taken to ensure each step of the computation is validate
d and verifiable. In this talk we present a long-standing conjecture in sp
ectral geometry\, and its resolution using validated finite element comput
ations. Schiffer’s conjecture states that if a bounded domain Ω in R^n
has any nontrivial Neumann eigenfunction which is a constant on the bound
ary\, then Ω must be a ball. This conjecture is open. A modification of S
chiffer’s conjecture is: for regular polygons of at least 5 sides\, we c
an demonstrate the existence of a Neumann eigenfunction which does not cha
nge sign on the boundary. In this talk\, we provide a recent proof using f
inite element calculations for the regular pentagon. The strategy involves
iteratively bounding eigenvalues for a sequence of polygonal subdomains o
f the triangle with mixed Dirichlet and Neumann boundary conditions. We us
e a learning algorithm to find and optimize this sequence of subdomains\,
and use non-conforming linear FEM to compute validated lower bounds for th
e lowest eigenvalue in each of these domains. The linear algebra is perfor
med within interval arithmetic. This is joint work with Bartlomiej Siudeja
and Ben Green at University of Oregon.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniel Wilczak (Jagiellonian University)
DTSTART:20200804T140000Z
DTEND:20200804T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/6
DESCRIPTION:Title: Rigorous numerical investigation of chaos and stability of periodic orbit
s in the Kuramoto-Sivashinsky PDE\nby Daniel Wilczak (Jagiellonian Uni
versity) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in No
nlinear Analysis\n\n\nAbstract\nWe give a computer-assisted proof of the e
xistence of symbolic dynamics for a certain Poincaré map in the one-dimen
sional Kuramoto-Sivashinsky PDE. In particular\, we show the existence of
infinitely many (countably) periodic orbits (POs) of arbitrary large princ
ipal periods. We provide also a study of the stability type of some POs. T
he proof utilizes pure topological results (variant of the method of cover
ing relations on compact absolute neighbourhood retracts) with rigorous in
tegration of the PDE and the associated variational equation. This talk is
based on the recent results [1\,2].\n\n[1] D. Wilczak and P. Zgliczyński
. A geometric method for infinite-dimensional chaos: symbolic dynamics for
the Kuramoto-Sivashinsky PDE on the line\, Journal of Differential Equati
ons\, Vol. 269 No. 10 (2020)\, 8509-8548.\n\n[2] D. Wilczak and P. Zgliczy
ński. A rigorous C1-algorithm for integration of dissipative PDEs based o
n automatic differentiation and the Taylor method\, in preparation.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Renato Calleja (UNAM\, Mexico)
DTSTART:20200811T140000Z
DTEND:20200811T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/7
DESCRIPTION:Title: Torus knot choreographies in the n-body problem\nby Renato Calleja (U
NAM\, Mexico) as part of CRM CAMP (Computer-Assisted Mathematical Proofs)
in Nonlinear Analysis\n\n\nAbstract\nn-body choreographies are periodic so
lutions to the n-body equations in which equal masses chase each other aro
und a fixed closed curve. In this talk I will present a systematic approac
h for proving the existence of spatial choreographies in the gravitational
body problem with the help of the digital computer. These arise from the
polygonal system of bodies in a rotating frame of reference. In rotating c
oordinates\, after exploiting the symmetries\, the equation of a choreogra
phic configuration is reduced to a delay differential equation (DDE) descr
ibing the position and velocity of a single body. We prove that a dense se
t of Lyapunov orbits\, with frequencies satisfying a Diophantine equation\
, correspond to choreographies.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Xuefeng Liu (Niigata University\, Japan)
DTSTART:20200721T140000Z
DTEND:20200721T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/8
DESCRIPTION:Title: Solution verification for the stationary Navier-Stokes equation over boun
ded non-convex 3D domains\nby Xuefeng Liu (Niigata University\, Japan)
as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear
Analysis\n\n\nAbstract\nWe consider the solution verification for the stat
ionary Navier-Stokes equation over a bounded non-convex 3D domain Ω. In 1
999\, M.T. Nakao\, et al.\, reported a solution existence verification exa
mple for the 2D square domain. However\, it has been a difficult problem
to deal with general 2D domains and 3D domains\, due to the bottleneck pro
blem in the a priori error estimation for the linearized NS equation. Rec
ently\, by extending the hypercircle method (Prage-Synge's theorem) to dea
l with the divergence-free condition in the Stokes equation\, the explicit
error estimation is constructed successfully based on a conforming finite
element approach [arXiv:2006.02952]. Further\, we succeeded in the solut
ion existence verification for the stationary NS equation in several nonco
nvex 3D domains. In this talk\, I will show the latest progress on this t
opic\, including the rigorous estimation of the eigenvalue of Stokes opera
tor in 3D domains.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Maxime Breden & Maximilian Engel (École Polytechnique\, France &
Freie Universität Berlin\, Germany)
DTSTART:20200825T140000Z
DTEND:20200825T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/9
DESCRIPTION:Title: Computer-assisted proof of shear-induced chaos in stochastically perturbe
d Hopf systems\nby Maxime Breden & Maximilian Engel (École Polytechni
que\, France & Freie Universität Berlin\, Germany) as part of CRM CAMP (C
omputer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\
nIn this talk\, we discuss a long-standing conjecture concerning shear-ind
uced chaos in stochastically perturbed systems exhibiting a Hopf bifurcati
on. Using the recently developed theory of conditioned Lyapunov exponents
on bounded domains\, we reformulate the problem into the rigorous computat
ion of eigenvectors of some elliptic PDEs\, namely the Kolmogorov/Fokker-P
lanck equations describing distributions of the underlying stochastic proc
ess\, and are thus able to prove that the first Lyapunov exponent is posi
tive for certain parameter regimes.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Caroline Wormell (University of Sydney\, Australia)
DTSTART:20200818T140000Z
DTEND:20200818T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/10
DESCRIPTION:Title: Rigorously validated estimation of statistical properties of expanding m
aps\nby Caroline Wormell (University of Sydney\, Australia) as part of
CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Akitoshi Takayasu (University of Tsukuba\, Japan)
DTSTART:20201006T140000Z
DTEND:20201006T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/11
DESCRIPTION:Title: Computer-assisted proofs for finding the monodromy of hypergeometric dif
ferential equations\nby Akitoshi Takayasu (University of Tsukuba\, Jap
an) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonline
ar Analysis\n\n\nAbstract\nIn this talk\, we introduce a numerical method
for rigorously finding the monodromy matrix of hypergeometric differential
equations. From a base point defined by fundamental solutions\, we analyt
ically continue the solution on a contour around a singular point of the d
ifferential equation using a rigorous integrator. Depending on the contour
we obtain the monodromy representation of fundamental solutions\, which r
epresents the fundamental group of the equation. As an application of this
method\, we consider a Picard-Fuchs type hypergeometric differential equa
tion arising from a polarized K3 surface. The monodromy matrix shows a def
ormation of homologically independent 2-cycles for the surface along the c
ontour\, which is regarded as a change of characterization for the K3 surf
ace. This is joint work with Naoya Inoue (University of Tsukuba) and Toshi
masa Ishige (Chiba University).\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Evelyn Sander (George Mason University\, USA)
DTSTART:20201027T140000Z
DTEND:20201027T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/12
DESCRIPTION:Title: Equilibrium validation in models for pattern formation based on Sobolev
embeddings\nby Evelyn Sander (George Mason University\, USA) as part o
f CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n
\n\nAbstract\nIn this talk\, I describe a method of computer-assisted proo
f focused on continuation of solutions depending on a parameter. These tec
hniques are applied to the Ohta-Kawasaki model for the dynamics of diblock
copolymers in dimensions one\, two\, and three. The functional analytic a
pproach and techniques can be generalized to other parabolic partial diffe
rential equations. This is joint work with Thomas Wanner (George Mason Uni
versity).\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Blake Barker (Brigham Young University\, USA)
DTSTART:20201110T150000Z
DTEND:20201110T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/13
DESCRIPTION:Title: Recent progress in proving stability of traveling waves in the 1D Navier
-Stokes equations using rigorous computations\nby Blake Barker (Brigha
m Young University\, USA) as part of CRM CAMP (Computer-Assisted Mathemati
cal Proofs) in Nonlinear Analysis\n\n\nAbstract\nWe discuss recent progres
s developing and applying rigorous computation to prove stability of trave
ling waves in the 1D Navier-Stokes equation. In particular\, we talk about
rigorous computation of the Evans function\, an analytic function whose z
eros correspond to eigenvalues of the linearized PDE problem. Nonlinear st
ability results by Zumbrun and collaborators show that the underlying trav
eling waves are stable if there are no eigenvalues in the right half of th
e complex plane. Thus one may use rigorous computation of the Evans functi
on to prove nonlinear-orbital stability of traveling waves.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/13/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gary Froyland (University of New South Wales\, Australia)
DTSTART:20201103T210000Z
DTEND:20201103T220000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/14
DESCRIPTION:Title: Stability and approximation of statistical limit laws\nby Gary Froyl
and (University of New South Wales\, Australia) as part of CRM CAMP (Compu
ter-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nThe
unpredictability of chaotic nonlinear dynamics leads naturally to statist
ical descriptions\, including probabilistic limit laws such as the central
limit theorem and large deviation principle. A key tool in the Nagaev-Gui
varc'h spectral method for establishing statistical limit theorems is a "t
wisted" transfer operator. We prove stability of the variance in the centr
al limit theorem and the rate\nfunction from a large deviation principle w
ith respect to deterministic and stochastic perturbations of the dynamics
and perturbations induced by numerical schemes. We then apply these result
s to piecewise expanding maps in one and multiple dimensions. This theory
can be extended to uniformly hyperbolic maps and in this setting we develo
p two new Fourier-analytic methods to provide the first rigorous estimates
of the variance and rate function for Anosov maps. This is joint work wi
th Harry Crimmins.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Maciej Capiński (AGH University of Science and Technology\, Polan
d)
DTSTART:20200901T140000Z
DTEND:20200901T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/15
DESCRIPTION:Title: Computer assisted proofs of Arnold Diffusion\nby Maciej Capiński (A
GH University of Science and Technology\, Poland) as part of CRM CAMP (Com
puter-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nW
e will present three methods that can be used for computer assisted proofs
of Arnold diffusion in Hamiltonian systems. The first is the classical Me
lnikov method\; the second is based a shadowing lemma in the setting of th
e scattering map theory\; the last is based on topological shadowing using
correctly aligned windows and cones. We will also discuss an application
in the setting of the Planar Elliptic Restricted Three Body Problem.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Elena Queirolo (Rutgers University\, USA)
DTSTART:20200915T140000Z
DTEND:20200915T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/16
DESCRIPTION:Title: Validating Hopf bifurcations in the Kuramoto-Sivashinsky PDE\nby Ele
na Queirolo (Rutgers University\, USA) as part of CRM CAMP (Computer-Assis
ted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nWe prove the
existence of a Hopf bifurcation in the Kuramoto–Sivashinsky PDE. For th
is\, we rewrite the Kuramoto–Sivashinsky equation into a desingularized
formulation near the Hopf point via a blow-up approach and we apply the ra
dii polynomial approach to validate a solution branch of periodic solution
s. Then this solution branch includes the Hopf bifurcation point.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Isaia Nisoli (Universidade Federal do Rio de Janeiro\, Brazil)
DTSTART:20200908T140000Z
DTEND:20200908T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/17
DESCRIPTION:Title: A proof of Noise Induced Order in the BZ map\, and some remarks on the p
henomenon\nby Isaia Nisoli (Universidade Federal do Rio de Janeiro\, B
razil) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonl
inear Analysis\n\n\nAbstract\nIn this talk I will present a Computer Aided
Proof of Noise Induced Order (NIO) in a model associated with the Belouso
v-Zhabotinsky reaction: when studying the random dynamical system with add
itive noise associated to the BZ map\, as the noise amplitude increases th
e Lyapunov exponent of the model transitions from positive to negative. Th
e proof is obtained through rigorous approximation of the stationary measu
re using Ulam method.\nI will also show a sufficient condition for the exi
stence of NIO in a wide family of one-dimensional examples.\n[1] S. Galato
lo\, M. Monge\, I. Nisoli "Existence of Noise Induced Order: a computer ai
ded proof"\, Nonlinearity 33(9)\n[2] I. Nisoli "Sufficient Conditions for
Noise Induced Order in 1-dimensional systems"\, arXiv:2003.08422\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Shane Kepley (Rutgers University\, USA)
DTSTART:20200922T140000Z
DTEND:20200922T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/18
DESCRIPTION:Title: Computing and validating collisions\, ejections\, and homoclinics for th
e three body problem\nby Shane Kepley (Rutgers University\, USA) as pa
rt of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analys
is\n\n\nAbstract\nUnderstanding connecting and collision/ejection orbits i
s central to the study of transport in Celestial Mechanics. The atlas algo
rithm combines the parameterization method with rigorous numerical techniq
ues for solving initial value problems in order to find and validate conne
cting orbits. However\, difficulties arise when parameterizing orbits pass
ing near a singularity such as “near miss” homoclinics or ejection/col
lision orbits. In this talk we present a method of overcoming this obstacl
e based on rigorous Levi-Civita regularization which desingularizes the ve
ctor field near the primaries. This regularization is performed dynamicall
y allowing invariant manifolds to be parameterized globally\, even near si
ngularities.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Piotr Nowak (Polish Academy of Sciences\, Poland)
DTSTART:20200929T140000Z
DTEND:20200929T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/19
DESCRIPTION:Title: A computer-assisted proof of Kazhdan’s property (T) for automorphism g
roups of free groups\nby Piotr Nowak (Polish Academy of Sciences\, Pol
and) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlin
ear Analysis\n\n\nAbstract\nProperty (T) was introduced in 1967 by Kazhdan
and is an important rigidity property of groups. The most elementary way
to define it is through a fixed point property: a group G has property (T)
if every action of G by affine isometries on a Hilbert space has a fixed
point. Property (T) has numerous applications in the form of rigidity of a
ctions and operator algebras associated to the group\, constructions of ex
pander graphs or constructions of counterexamples to Baum-Connes-type conj
ectures. \n\nIn this talk I will give a brief introduction to property (T)
and explain the necessary group-theoretic background in order to present
a computer-assisted approach to proving property (T) by showing that the L
aplacian on the group has a spectral gap. This approach allowed us show th
at Aut(F_n)\, the group of automorphisms of the free group F_n on n genera
tors\, has property (T) when n is at least 5: the case n=5 is joint work w
ith Marek Kaluba and Narutaka Ozawa\, and the case of n at least 6 is join
t work with Kaluba and Dawid Kielak. Important aspects of our methods incl
ude passing from a computational result to a rigorous proof and later obta
ining the result for an infinite family of groups using a single computati
on. I will present an overview of these arguments.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Assia Mahboubi (Inria\, France & VU Amsterdam\, Netherlands)
DTSTART:20201020T140000Z
DTEND:20201020T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/20
DESCRIPTION:Title: Formally verified computer-assisted mathematical proofs\nby Assia Ma
hboubi (Inria\, France & VU Amsterdam\, Netherlands) as part of CRM CAMP (
Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract
\nProof assistants are pieces of software designed for defining formally
mathematical objects\, statement and proofs. In particular\, such a forma
lization reduces the verification of proofs to a purely mechanical well-f
ormedness check. Since the early 70s\, proof\nassistants have been extensi
vely used for applications in program verification\, notably for security
-related issues. They have also been used to verify landmark results in m
athematics\, including theorems with a computational proof\, like the Fou
r Colour Theorem (Appel and Haken\, 1977) or Hales and Ferguson's proof o
f the Kepler conjecture (2005). This talk will discuss what are formalize
d mathematics and formal proofs\, and sketch the architecture of modern p
roof assistants. It will also showcase a few applications in formally ve
rified rigorous computation.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/20/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ferenc Bartha (Szeged University\, Hungary)
DTSTART:20201117T150000Z
DTEND:20201117T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/21
DESCRIPTION:Title: Stable periodic orbits for the Mackey-Glass equation\nby Ferenc Bart
ha (Szeged University\, Hungary) as part of CRM CAMP (Computer-Assisted Ma
thematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nWe consider the cl
assical Mackey-Glass delay differential equation. By letting n go to infin
ity in the part encapsulating the delayed term\, we obtain a limiting hybr
id delay equation. We investigate how periodic solutions of this limiting
equation are related to periodic solutions of the original MG equation for
large n. Then\, we establish a procedure for constructing such periodic s
olutions via forward time integration. Finally\, we use rigorous numerics
to establish the existence of stable periodic orbits for various parameter
s of the MG equation. We note that some of these solutions exhibit seeming
ly complicated dynamics\, yet they are stable periodic orbits.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Arnd Scheel (University of Minnesota\, USA)
DTSTART:20201201T150000Z
DTEND:20201201T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/22
DESCRIPTION:Title: Future Directions Series: Defect and front dynamics: analysis and comput
ation\nby Arnd Scheel (University of Minnesota\, USA) as part of CRM C
AMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbs
tract\nThis will be a personal selection of results and related open probl
ems in dissipative spatially extended systems. I will focus on simple\, so
metimes universal models such as the complex Ginzburg-Landau\, the Swift-H
ohenberg\, and extended KPP equations and attempts to describe their dynam
ics based on coherent structures. I will present "conceptual' analytical r
esults\, and describe gaps that rigorous computations may be able to close
. Topics include invasion fronts\, defects in one- and two-dimensional osc
illatory media\, and point defects in striped phases.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/22/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gianni Arioli (Politecnico di Milano\, Italy)
DTSTART:20201124T150000Z
DTEND:20201124T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/23
DESCRIPTION:Title: Symmetry breaking and Hopf bifurcations for the planar Navier-Stokes equ
ation\nby Gianni Arioli (Politecnico di Milano\, Italy) as part of CRM
CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nA
bstract\nWe consider the Navier-Stokes equation for an incompressible visc
ous fluid on a square\, satisfying Navier boundary conditions and being su
bjected to a time-independent force. The uniqueness of stationary solution
s is studied in dependence of the kinematic viscosity. For some particular
forcing\, it is shown that uniqueness persists on some continuous branch
of stationary solutions\, when the viscosity becomes arbitrarily small. On
the other hand\, for a different forcing\, a branch of symmetric solution
s is shown to bifurcate\, giving rise to a secondary branch of nonsymmetri
c stationary solutions. Furthermore\, as the kinematic viscosity is varied
\, the branch of symmetric stationary solutions is shown to undergo a Hopf
bifurcation\, where a periodic cycle branches from the stationary solutio
n. Our proof is constructive and uses computer-assisted estimates.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/23/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kevin Church (McGill University\, Canada)
DTSTART:20201013T140000Z
DTEND:20201013T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/24
DESCRIPTION:Title: Rigorous computation of periodic solutions and Floquet multipliers in de
lay differential equations with time-forced discontinuities\nby Kevin
Church (McGill University\, Canada) as part of CRM CAMP (Computer-Assisted
Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nI will present
some recent work on rigorous computation of periodic solutions for delay d
ifferential equations with impulse effects. At fixed moments in time\, the
state of such a system is reset and solutions become discontinuous. Once
a periodic solution of such a system has been computed\, its Floquet spect
rum can be rigorously computed by discretization of the monodromy operator
(period map) and some technical error estimates. As an application\, we c
ompute a branch of periodic solutions in the pulse-harvested Hutchinson eq
uation and examine its stability.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/24/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jean-Pierre Eckmann (University of Geneva\, Switzerland)
DTSTART:20201208T150000Z
DTEND:20201208T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/25
DESCRIPTION:Title: CRM-CAMP Colloquium\nby Jean-Pierre Eckmann (University of Geneva\,
Switzerland) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) i
n Nonlinear Analysis\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/25/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nicolas Brisebarre (ENS Lyon\, France)
DTSTART:20210119T150000Z
DTEND:20210119T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/26
DESCRIPTION:Title: Correct rounding for transcendental functions\nby Nicolas Brisebarre
(ENS Lyon\, France) as part of CRM CAMP (Computer-Assisted Mathematical P
roofs) in Nonlinear Analysis\n\n\nAbstract\nOn a computer\, real numbers a
re usually represented by a finite set of numbers called floating-point nu
mbers. When one performs an operation on these numbers\, such as an evalua
tion by a function\, one returns a floating-point number\, hopefully close
to the mathematical result of the operation. Ideally\, the returned resul
t should be the exact rounding of this mathematical value. If we’re only
allowed a unique and fast evaluation (a constraint often met in practice)
\, one knows how to guarantee such a quality of results for arithmetical o
perations like +\,−\,x\,/ and square root but\, as of today\, it is stil
l an issue when it comes to evaluate an elementary function such as cos\,
exp\, cube root for instance. This problem\, called Table Maker’s Dilemm
a\, is actually a diophantine approximation problem. It was tackled\, over
the last fifteen years\, by V. Lefèvre\, J.M. Muller\, D. Stehlé\, A. T
isserand and P. Zimmermann (LIP\, ÉNS Lyon and LORIA\, Nancy)\, using too
ls from algorithmic number theory. Their work made it possible to partiall
y solve this question but it remains an open problem. In this talk\, I wil
l present a joint work with Guillaume Hanrot (ÉNS Lyon\, LIP\, AriC) that
improve on a part of the existing results.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/26/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robert Szczelina (Jagiellonian University\, Poland)
DTSTART:20210112T150000Z
DTEND:20210112T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/27
DESCRIPTION:Title: A computer assisted proof of chaos in a delayed perturbation of chaotic
ODE\nby Robert Szczelina (Jagiellonian University\, Poland) as part of
CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\
n\nAbstract\nWe will discuss some recent developments to the Taylor method
for forward in time rigorous integration of Delay Differential Equations
(DDEs) with constant delays. We briefly discuss how to generalize method o
f the paper "Algorithm for rigorous integration of Delay Differential Equa
tions and the computer-assisted proof of periodic orbits in the Mackey-Gla
ss equation\, Found. Comp. Math.\, 18 (6)\, 1299-1332\, 2018" to incorpora
te multiple lags\, multiple variables (systems of equations) and how to ut
ilize "smoothing of solutions" to produce results of a far greater accurac
y\, especially when computing Poincaré maps between local sections. We wi
ll apply this method to validate some covering relations between carefully
selected sets under Poincaré maps defined with a flow associated to a DD
E. Together with standard topological arguments for compact maps it will p
rove existence of a chaotic dynamics\, in particular the existence of infi
nite (countable) number of periodic orbits. The DDE under consideration is
a toy example made by adding a delayed term to the Rössler ODE under par
ameters for which chaotic attractor exists. The delayed term is small in a
mplitude\, but the lag time is macroscopic (not small). This is a joint wo
rk with Piotr Zgliczyński.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/27/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Anna Gierzkiewicz (University of Agriculture in Krakow\, Poland)
DTSTART:20210126T150000Z
DTEND:20210126T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/28
DESCRIPTION:Title: Periodic orbits in Roessler system\nby Anna Gierzkiewicz (University
of Agriculture in Krakow\, Poland) as part of CRM CAMP (Computer-Assisted
Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nIn a joint work
with Piotr Zgliczynski\, we study the Roessler system with an attracting
periodic orbit\, for two sets of parameters. In both cases the attractor o
n a Poincare section seems to be almost one-dimensional and therefore we a
pply the methods for two-dimensional perturbations of an interval's self-m
ap introduced by Zgliczynski in Multidimensional perturbations of one-dime
nsional maps and stability of Sharkovskii ordering in 1999. We prove the e
xistence of p-periodic orbits for almost all natural p with computer assis
tance: by interval Newton method and covering relations.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/28/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hans Koch (University of Texas at Austin\, USA)
DTSTART:20210202T150000Z
DTEND:20210202T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/29
DESCRIPTION:Title: Golden mean renormalization for the almost Mathieu operator and related
skew products\nby Hans Koch (University of Texas at Austin\, USA) as p
art of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analy
sis\n\n\nAbstract\nWe renormalize SL(2\,R) skew-product maps over circle r
otations. Such maps arise e.g. in the spectral analysis of the Hofstadte
r Hamiltonian and the almost Mathieu operator. For rotations by the inver
se golden mean\, we prove the existence of two renormalization-periodic o
rbits. We conjecture that there are infinitely many such orbits\, and th
at the associated universal constants describe local scaling properties o
f the Hofstadter spectrum and of the corresponding generalized eigenvecto
rs. Some recent results on trigonometric skew-product maps will be descr
ibed as well. This is joint work with Saša Kocić (UT Austin\, USA).\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/29/
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Sanders (Universidad Nacional Autonoma de Mexico\, Mexico)
DTSTART:20210209T150000Z
DTEND:20210209T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/30
DESCRIPTION:Title: Interval methods with Julia: Finding one million roots in one second
\nby David Sanders (Universidad Nacional Autonoma de Mexico\, Mexico) as p
art of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analy
sis\n\n\nAbstract\nThe Julia language provides a remarkably productive env
ironment for scientific computing\, with a unique combination of interacti
vity and speed\, and is particularly suitable for defining operations on n
ew mathematical objects\, such as intervals.\nI will present our free / op
en-source packages for interval arithmetic and interval methods (juliainte
rvals.github.io)\, written in pure Julia and comparable to state-of-the-ar
t libraries. They use the composability coming from Julia's "multiple-disp
atch"-based design and generic programming to integrate with other package
s in the "ecosystem"\, including linear algebra\, automatic differentiatio
n\, and plotting.\nThe foundation is IntervalArithmetic.jl \, which is alm
ost compliant with the IEEE-1788 standard. Applications currently implemen
ted include root finding\, global optimization\, constraint programming\,
Taylor models\, and validated integration of ODEs.\nI will also show how J
ulia's facilities for parallel computing allow us to create user-defined o
bjects on GPUs and manipulate them using the same Julia code. As an exampl
e benchmark\, we find and verify one million stationary points of the two-
dimensional transcendental Griewank function in under one second.\nJoint w
ork with Luis Benet (ICF-UNAM).\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/30/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Konstantin Mischaikow (Rutgers University\, USA)
DTSTART:20210216T150000Z
DTEND:20210216T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/31
DESCRIPTION:Title: CRM-CAMP COLLOQUIUM: Wherefore computer assisted proofs in dynamics?
\nby Konstantin Mischaikow (Rutgers University\, USA) as part of CRM CAMP
(Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstrac
t\nOver the past few decades the topic of computer assisted proofs in nonl
inear dynamics has blossomed and is well on the way to becoming a standard
part of the field. So perhaps it is worth reflecting on some high level t
opics. With this in mind I will discuss\, from an admittedly biased person
al perspective\, several questions:\nWhy do computer assisted proofs?\nWhe
re do computer assisted proofs in dynamics as currently being done lie in
the bigger scheme of formal proof systems?\nWhat new perspective about non
linear dynamics can we extract from computer assisted proofs?\nHow should
we resolve the dichotomy between precision and accuracy?\nWhat role do com
puter assisted proofs have to play as we move into an era of data driven s
cience and machine learning?\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/31/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Florent Bréhard (Uppsala University\, Sweden)
DTSTART:20210223T150000Z
DTEND:20210223T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/32
DESCRIPTION:Title: Beyond Exponential Complexity of Newton-Galerkin Validation Methods: A P
olynomial-Time Newton-Picard Validation Algorithm for linear ODEs\nby
Florent Bréhard (Uppsala University\, Sweden) as part of CRM CAMP (Comput
er-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nA wi
de range of techniques have been developed to compute validated numerical
solutions to various kind of equations (e.g.\, ODE\, PDE\, DDE) arising in
computer-assisted proofs. Among them are Newton-Galerkin a posteriori val
idation techniques\, which provide error bounds for approximate solutions
by using the contraction map principle in a suitable coefficient space (e.
g.\, Fourier or Chebyshev). More precisely\, a contracting Newton-like ope
rator is constructed by truncating and inverting the inverse Jacobian of t
he equation.\nWhile these techniques were extensively used in cutting-edge
works in the community\, we show that they suffer from an exponential run
ning time w.r.t. the input equation. We illustrate this shortcomings on si
mple linear ODEs\, where a "large" parameter in the equation leads to an i
ntractable instance for Newton-Galerkin validation algorithms.\nFrom this
observation\, we build a new validation scheme\, called Newton-Picard\, wh
ich breaks this complexity barrier. The key idea consists in replacing the
inverse Jacobian not by a finite-dimensional truncated matrix as in Newto
n-Galerkin\, but by an integral operator with a polynomial approximation o
f the so-called resolvent kernel. Moreover\, this method is also less basi
s-dependent and more suitable to be formalized in a computer proof assista
nt towards a fully certified implementation in the future.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/32/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alessandra Celletti (University of Rome Tor Vergata\, Italy)
DTSTART:20210309T150000Z
DTEND:20210309T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/33
DESCRIPTION:Title: KAM (computer-assisted) results in Celestial Mechanics: the dissipative
spin-orbit problem\nby Alessandra Celletti (University of Rome Tor Ver
gata\, Italy) as part of CRM CAMP (Computer-Assisted Mathematical Proofs)
in Nonlinear Analysis\n\n\nAbstract\nThe existence of invariant tori throu
gh Kolmogorov-Arnold-Moser (KAM) theory has been proven in several models
of Celestial Mechanics through dedicated analytical proofs combined with c
omputer-assisted techniques. After reviewing some of such results\, obtain
ed in conservative frameworks\, we present a recent result on the existenc
e of invariant attractors for a dissipative model: the spin-orbit problem
with tidal torque. This model belongs to the class of conformally symplect
ic systems\, which are characterized by the property that they transform t
he symplectic form into a multiple of itself. Finding the solution of such
systems requires to add a drift parameter.\n\nWe describe a KAM theorem f
or conformally symplectic systems in an a-posteriori format: assuming the
existence of an approximate solution\, satisfying the invariance equation
up to an error term - small enough with respect to explicit condition numb
ers\, - then we can prove the existence of a solution nearby. The theorem\
, which does not assume that the system is close to integrable\, yields an
efficient algorithm to construct invariant attractors for the spin-orbit
problem and it provides accurate estimates of the breakdown threshold of t
he invariant attractor.\n\nThis talk refers to joint works with R. Calleja
\, J. Gimeno\, and R. de la Llave.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/33/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Shin'ichi Oishi (Waseda University\, Japan)
DTSTART:20210316T140000Z
DTEND:20210316T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/34
DESCRIPTION:Title: Computer assisted existence proof of complicated dynamics in forced dela
y action oscillator modelling El Nino phenomena\nby Shin'ichi Oishi (W
aseda University\, Japan) as part of CRM CAMP (Computer-Assisted Mathemati
cal Proofs) in Nonlinear Analysis\n\n\nAbstract\nA computer assisted proof
is presented for the existence of various periodic solutions for forced S
uarez-Schopf's equation\, which are delay differential equations modeling
El Nino. Tight inclusions of periodic solutions are calculated through num
erical verification method by utilizing a structure of Galerkin's equation
for forced Suarez-Schopf's equation effectively. The existence of various
periodic solutions has been proved via computer assisted proofs including
various subharmonics. Especially\, coexistence of several subharmonics ar
e proved and numerical simulations are presented suggesting an appearance
of chaos.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/34/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Piotr Kalita (Jagiellonian University\, Poland)
DTSTART:20210406T140000Z
DTEND:20210406T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/36
DESCRIPTION:Title: Rigorous FEM based forward in time integration of dissipative PDEs\n
by Piotr Kalita (Jagiellonian University\, Poland) as part of CRM CAMP (Co
mputer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\n
We present the technique for computer assisted rigorous forward in time in
tegration of problems governed by dissipative PDEs. The approach is based
on the Finite Element Method. The key concepts lie in the propagation of t
he a priori energy estimates needed to bound the infinite dimensional rema
inder and in rigorous integration of differential inclusions. The techniqu
e is illustrated by the computer assisted construction of the time periodi
c solution for periodically forced one-dimensional Burgers equation with h
omogeneous Dirichlet boundary conditions. Talk is based on joint work with
Piotr Zgliczyński.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/36/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Warwick Tucker (Monash University\, Australia)
DTSTART:20210413T140000Z
DTEND:20210413T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/37
DESCRIPTION:Title: Relative equilibria for the n-body problem\nby Warwick Tucker (Monas
h University\, Australia) as part of CRM CAMP (Computer-Assisted Mathemati
cal Proofs) in Nonlinear Analysis\n\n\nAbstract\nWe will discuss the class
ical problem from celestial mechanics of determining the number of relativ
e equilibria a set of planets can display. Several already established res
ults will be presented\, as well as a new contribution (in terms of a new
proof) for the restricted 4-body problem. We will discuss its possible ext
ensions to harder instances of the general problem. This is joint work wit
h Piotr Zgliczynski and Jordi-Lluis Figueras.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/37/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alberto Bressan (Penn State University\, USA)
DTSTART:20210420T140000Z
DTEND:20210420T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/38
DESCRIPTION:Title: Non-uniqueness and error bounds for fluid flow\nby Alberto Bressan (
Penn State University\, USA) as part of CRM CAMP (Computer-Assisted Mathem
atical Proofs) in Nonlinear Analysis\n\n\nAbstract\nFor hyperbolic systems
of conservation laws in one space dimension\, a general existence-unique
ness theory is now available\, for entropy weak solutions with bounded var
iation. In several space dimensions\, however\, it seems unlikely that a
similar theory can be achieved.\n\nFor the 2-D Euler equations\, in this
talk I shall discuss the simplest possible examples of Cauchy problems a
dmitting multiple solutions. Several numerical simulations will be presen
ted\, for incompressible as well as compressible flow\, indicating the e
xistence of two distinct solutions for the same initial data. Typically\,
one of the solutions contains a single spiraling vortex\, while the other
solution contains two vortices.\n\nSome theoretical work\, aimed at valid
ating the numerical results\, will also be discussed.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/38/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kaname Matsue (Kyushu University\, Japan)
DTSTART:20210504T140000Z
DTEND:20210504T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/39
DESCRIPTION:Title: Rigorous numerics of blow-up solutions for autonomous ODEs\nby Kanam
e Matsue (Kyushu University\, Japan) as part of CRM CAMP (Computer-Assiste
d Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nHere I talk ab
out the recent studies concerning rigorous numerics of blow-up solutions f
or autonomous ODEs in a systematic way under a mild assumption of vector f
ields. The fundamental tools used here are “compactifications” of pha
se spaces which map the infinity to the boundary of transformed phase spa
ces (the “horizon”)\, and “time-scale desingularizations determined
by the original vector fields”. Blow-up solutions are then essentially
transformed into solutions on stable manifolds of invariant sets on the ho
rizon. In particular\, rigorous enclosures of blow-up solutions and their
blow-up times can be validated by means of standard machineries of dynami
cal systems such as ODE integrators\, locally defined Lyapunov functions a
nd parameterization of invariant manifolds. Dynamical system approach sho
wn here reveals many quantitative and qualitative nature of blow-up behavi
or for various concrete dynamical systems. A series of works presented in
the present talk (involving rigorous numerics) are based on joint works w
ith Profs. Akitoshi Takayasu\, Nobito Yamamoto and Jean-Philippe Lessard.\
n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/39/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Thomas Wanner (George Mason University\, USA)
DTSTART:20210518T140000Z
DTEND:20210518T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/40
DESCRIPTION:Title: Bifurcation Points in the Ohta-Kawasaki Model\nby Thomas Wanner (Geo
rge Mason University\, USA) as part of CRM CAMP (Computer-Assisted Mathema
tical Proofs) in Nonlinear Analysis\n\n\nAbstract\nDiblock copolymers are
a class of materials formed by the reaction of two linear polymers. The di
fferent structures taken on by these polymers grant them special propertie
s\, which can prove useful in applications such as the development of new
adhesives and asphalt additives. We consider a model for the formation of
diblock copolymers first proposed by Ohta and Kawasaki\, which is a Cahn-H
illiard-like equation together with a nonlocal term. Unlike the Cahn-Hilli
ard model\, even on one-dimensional spatial domains the steady state bifur
cation diagram of the Ohta-Kawasaki model is still not fully understood. W
e therefore present computer-assisted proof techniques which can be used t
o validate and continue its bifurcation points. This includes not only fol
d points\, but also pitchfork bifurcations which are the result of a cycli
c group action beyond forcing through Z_2 symmetries.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/40/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Zbigniew Galias (AGH University of Science and Technology\, Poland
)
DTSTART:20210615T140000Z
DTEND:20210615T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/41
DESCRIPTION:Title: Chaos in the Chua's circuit\nby Zbigniew Galias (AGH University of S
cience and Technology\, Poland) as part of CRM CAMP (Computer-Assisted Mat
hematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nSeveral results on
the existence of chaos in the Chua's circuit with piesewise linear and cub
ic nonlinearities will be presented.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/41/
END:VEVENT
BEGIN:VEVENT
SUMMARY:J.D. Mireles James (Florida Atlantic University\, USA)
DTSTART:20210302T150000Z
DTEND:20210302T160000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/42
DESCRIPTION:Title: Boundary value problems and transversality in conservative systems: comp
uter assisted proofs of connection and collision orbits\nby J.D. Mirel
es James (Florida Atlantic University\, USA) as part of CRM CAMP (Computer
-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nI'll d
iscuss a framework for two-point boundary value problems in conservative s
ystems which detects transversality\, allows for the possibility of multip
le changes of coordinates\, and leads naturally to computer assisted proof
s. The set-up applies to dynamical problems in the level set like finding
connecting orbits between hyperbolic invariant objects and collisions. T
he main technical difficulty is that the conserved quantity leads to overd
etermined systems of equations. This problem can be overcome in a number
of different ways\, including elimination of an equation\, by exploiting d
iscrete symmetries (if any)\, or by introducing a new variable called an u
nfolding parameter. I'll look at two common ways of defining unfolding p
arameters and show that they don't disrupt the transversality properties o
f the BVP. I'll also illustrate some applications of this setup to comput
er assisted proofs of connecting orbits and collisions in the circular res
tricted three body problem. This is joint work with Shane Kepley and Maci
ej Capinski.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/42/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jean-Philippe Lessard (McGill University\, Canada)
DTSTART:20210330T140000Z
DTEND:20210330T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/43
DESCRIPTION:Title: Computer-assisted proofs for Cauchy problems of delay equations and PDEs
via Chebyshev series\nby Jean-Philippe Lessard (McGill University\, C
anada) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonl
inear Analysis\n\n\nAbstract\nIn this talk we introduce recent general met
hods to rigorously compute solutions of infinite dimensional Cauchy proble
ms. The idea is to expand the solutions in time using Chebyshev series an
d use the contraction mapping theorem to construct a neighbourhood about a
n approximate solution which contains the exact solution of the Cauchy pro
blem. We apply the methods to delay differential equations and to semi-lin
ear parabolic partial differential equations.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/43/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Antoine Zurek (Technische Universität Wien\, Austria)
DTSTART:20210323T140000Z
DTEND:20210323T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/44
DESCRIPTION:Title: Existence of traveling wave solutions for the Diffusion Poisson Coupled
Model: a computer-assisted proof\nby Antoine Zurek (Technische Univers
ität Wien\, Austria) as part of CRM CAMP (Computer-Assisted Mathematical
Proofs) in Nonlinear Analysis\n\n\nAbstract\nIn France one option under st
udy for the storage of high-level radioactive waste is based on an undergr
ound repository. More precisely\, the waste shall be confined in a glass m
atrix and then placed into cylindrical steel canisters. These containers s
hall be placed into micro-tunnels in the highly impermeable Callovo-Oxford
ian claystone layer at a depth of several hundred meters. The Diffusion Po
isson Coupled Model (DPCM) aims to investigate the safety of such long ter
m repository concept by describing the corrosion processes appearing at th
e surface of carbon steel canisters in contact with a claystone formation.
It involves drift-diffusion equations on the density of species (electron
s\, ferric cations and oxygen vacancies)\, coupled with a Poisson equation
on the electrostatic potential and with moving boundary equations. So far
\, no theoretical results giving a precise description of the solutions\,
or at least under which conditions the solutions may exist\, are avalaible
in the literature. However\, a finite volume scheme has been developed to
approximate the equations of the DPCM model. In particular\, it was obser
ved numerically the existence of traveling wave solutions for the DPCM mod
el. These solutions are defined by stationary profiles on a fixed size dom
ain with interfaces moving at the same velocity. The main objective of thi
s talk is to present how we apply a computer-assisted method in order to p
rove the existence of such traveling wave solutions for the system. This a
pproach allows us to obtain for the first time a precise and certified des
cription of some solutions. \nThis work is in collaboration with Maxime Br
eden and Claire Chainais-Hillairet.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/44/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Charles Fefferman (Princeton University\, USA)
DTSTART:20210601T140000Z
DTEND:20210601T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/45
DESCRIPTION:Title: CRM CAMP Colloquium: Encounters with Computer-Assisted Proofs in Early D
ays\nby Charles Fefferman (Princeton University\, USA) as part of CRM
CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAb
stract\nThe talk recounts how computer-assisted proofs came into two theor
ems on the quantum mechanics of Coulomb systems during the 1980's.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/45/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joel Dahne (Uppsala University\, Sweden)
DTSTART:20210427T140000Z
DTEND:20210427T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/46
DESCRIPTION:Title: A computer assisted counterexample to Payne’s nodal line conjecture wi
th few holes\nby Joel Dahne (Uppsala University\, Sweden) as part of C
RM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\
nAbstract\nPayne conjectured in 1967 that the nodal line of the second Dir
ichlet eigenfunction must touch the boundary of the domain. In their 1997
breakthrough paper\, Hoffmann-Ostenhof\, Hoffmann-Ostenhof and Nadirashvil
i proved this to be false by constructing a counterexample in the plane wi
th an unspecified\, but large\, number of holes and raised the question of
the minimum number of holes a counterexample can have. In this talk I wil
l present a computer assisted counter example with 6 holes. This is joint
work with Javier Gómez-Serrano and Kimberly Hou.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/46/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Marian Mrozek (Jagiellonian University\, Poland)
DTSTART:20210622T140000Z
DTEND:20210622T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/47
DESCRIPTION:Title: Combinatorial Topological Dynamics\nby Marian Mrozek (Jagiellonian U
niversity\, Poland) as part of CRM CAMP (Computer-Assisted Mathematical Pr
oofs) in Nonlinear Analysis\n\n\nAbstract\nSince the publication in 1998 o
f the seminal work by Robin Forman on combinatorial Morse theory there has
been growing interest in dynamical systems on finite spaces. The main mot
ivation to study combinatorial dynamics comes from data science. But\, the
y also provide very concise models of dynamical phenomena and show some po
tential in certain computer assisted proofs in dynamics.\n\nIn the talk I
will present the basic ideas of Conley theory for combinatorial dynamical
system\, particularly for a combinatorial multivector field which is a gen
eralization of combinatorial vector field introduced by Forman. The theory
is based on concepts which are analogous to the concepts of classical the
ory: isolating neighborhood\, isolated invariant set\, index pair\, Conley
index\, Morse decomposition\, connection matrix. The concepts are analogo
us but in some cases surprisingly different in details. This may be explai
ned by the non-Hausdorff nature of combinatorial topological spaces.\n\nDe
spite the differences there seem to be strong formal ties between the comb
inatorial and classical dynamics on topological level. A Morse decompositi
on of a combinatorial vector field on an abstract simplicial complex induc
es a semiflow on the geometric realization of the complex with a Morse dec
omposition exhibiting the same Conley-Morse graph. Actually\, this corresp
ondence of Morse decompositions and Conley-Morse graphs applies to every s
emiflow which is transversal to the boundaries of top dimensional cells of
a certain cellular decomposition of the phase space associated with the c
ombinatorial vector field.\n\nThere is also a formal relation in the oppos
ite direction. Given a smooth flow and a cellular decomposition of its pha
se space which is transversal to the flow\, there is an induced combinator
ial multivector field on the cellular structure of the phase space. Moreov
er\, if the induced combinatorial multivector field admits a periodic traj
ectory with an appropriate Conley index\, a periodic orbit exists also for
the original smooth flow.\n\nThe formal ties seem to provide a natural fr
amework for a rigorous global analysis of the dynamics of a flow: the deco
mposition into the gradient and recurrent part together with the computati
on of the Conley-Morse graph\, connection matrix and revealing the interna
l structure of the recurrent part.\n\nBased on joint work with J. Barmak\,
T. Dey\, M. Juda\, T. Kaczynski\, T. Kapela\, J. Kubica\, M. Lipiński
R. Slechta\, R. Srzednicki\, J. Thorpe and Th. Wanner.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/47/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Vladimir Sverak (University of Minnesota)
DTSTART:20210608T140000Z
DTEND:20210608T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/48
DESCRIPTION:Title: OPEN PROBLEMS SERIES: Some conjectures that seem difficult to prove\
nby Vladimir Sverak (University of Minnesota) as part of CRM CAMP (Compute
r-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nIn ma
ny cases\, numerics and/or heuristics provide compelling evidence for stat
ements that we have trouble proving rigorously. I will discuss some exampl
es\, mostly inspired by fluid flows.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/48/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jonathan Jaquette (Boston University\, USA)
DTSTART:20210511T140000Z
DTEND:20210511T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/49
DESCRIPTION:Title: A computer assisted proof of Wright's conjecture: counting and discounti
ng slowly oscillating periodic solutions to a DDE\nby Jonathan Jaquett
e (Boston University\, USA) as part of CRM CAMP (Computer-Assisted Mathema
tical Proofs) in Nonlinear Analysis\n\n\nAbstract\nA classical example of
a nonlinear delay differential equation is Wright's equation: $y'(t) = −
\\alpha y(t − 1)[1 + y(t)]$\, considering $\\alpha > 0$ and $y(t) > -1$.
This talk discusses two conjectures associated with this equation: Wright
's conjecture\, which states that the origin is the global attractor for a
ll $\\alpha \\in ( 0 \, \\pi/2]$\; and Jones' conjecture\, which states t
hat there is a unique slowly oscillating periodic solution for $\\alpha >
\\pi /2 $. \n\nTo prove Wright's conjecture our approach relies on a caref
ul investigation of the neighborhood of the Hopf bifurcation occurring at
$\\alpha = \\pi/ 2$. Using a rigorous numerical integrator we characterize
slowly oscillating periodic solutions and calculate their stability\, pro
ving Jones' conjecture for $\\alpha \\in [1.9\,6.0]$ and thereby all $\\al
pha \\geq 1.9$. We complete the proof of Jones conjecture using global opt
imization methods\, extended to treat infinite dimensional problems.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/49/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrew Burbanks (University of Portsmouth\, UK)
DTSTART:20210629T140000Z
DTEND:20210629T150000Z
DTSTAMP:20260422T212747Z
UID:CRM-CAMP/50
DESCRIPTION:Title: Computer-assisted proofs for renormalisation fixed-points and eigenfunct
ions for period-doubling universality in maps of the interval\nby Andr
ew Burbanks (University of Portsmouth\, UK) as part of CRM CAMP (Computer-
Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nWe prov
e the existence of a fixed point to the renormalisation operator for perio
d doubling in maps of even degree at the critical point. We work with a mo
dified operator that encodes the action of the renormalisation operator on
even functions. Building on previous work\, our proof uses rigorous compu
ter-assisted means to bound operations in a space of analytic functions an
d hence to show that a quasi-Newton operator for the fixed-point problem i
s a contraction map on a suitable ball.\n\nWe bound the spectrum of the Fr
echet derivative of the renormalisation operator at the fixed point\, esta
blishing the hyperbolic structure\, in which the presence of a single esse
ntial expanding eigenvalue explains the universal asymptotically self-simi
lar bifurcation structure observed in the iterations of families of maps l
ying in the relevant universality class.\n\nBy recasting the eigenproblem
for the Frechet derivative in a particular nonlinear form\, we again use t
he contraction mapping principle to gain rigorous bounds on eigenfunctions
and their corresponding eigenvalues. In particular\, we gain tight bounds
on the eigenfunction corresponding to the essential expanding eigenvalue
delta. We adapt the procedure to the eigenproblem for the scaling of added
uncorrelated noise.\n\nOur computations use multi-precision interval arit
hmetic with rigorous directed rounding modes to bound tightly the coeffici
ents of the relevant power series and their high-order terms\, and the cor
responding universal constants.\n
LOCATION:https://researchseminars.org/talk/CRM-CAMP/50/
END:VEVENT
END:VCALENDAR