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:20260404T095849Z
UID:CRM-CAMP/1
DESCRIPTION:Title: Stable periodic patterns in 3D for the Ohta-Kawasaki problem\n
by Jan Bouwe van den Berg (VU Amsterdam) as part of CRM CAMP (Computer-Ass
isted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nIn this ta
lk we discuss a mathematically rigorous computational method to compare lo
cal minimizers of the Ohta-Kawasaki free energy\, describing diblock copol
ymer melts. This energy incorporates a nonlocal term to take into account
the bond between the monomers.\nWorking within an arbitrary space group sy
mmetry\, we explore the phase space\, computing candidates both with and w
ithout experimentally observed symmetries. We validate the phase diagram\,
identifying regions of parameter space where different spatially periodic
structures have the lowest energy. These patterns may be lamellar layers\
, hexagonally packed cylinders\, body-centered or close-packed spheres\, a
s well as double gyroids and 'O70' arrangements. Each computation is valid
ated by a mathematical theorem\, where we bound the truncation errors and
apply a fixed point argument to establish a computer-assisted proof. The m
ethod can be applied more generally to symmetric space-time periodic solut
ion of many partial differential equations.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jonathan Jaquette (Boston University)
DTSTART:20200630T140000Z
DTEND:20200630T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/2
DESCRIPTION:Title: An overabundance of breathers in a nonlinear Schrödinger equation
without gauge invariance\nby Jonathan Jaquette (Boston University) as
part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Ana
lysis\n\n\nAbstract\nIn this talk we study the nonlinear Schrödinger equa
tion $i u_t + \\triangle u + u^2 = 0$ posed on the 1-torus. Based on their
numerics\, Cho\, Okamoto\, & Shōji conjectured in their 2016 paper that:
(C1) any singularity in the complex plane of time arising from inhomogene
ous initial data is a branch singularity\, and (C2) real initial data will
exist globally in real time. If true\, Conjecture 1 would suggest a stron
g incompatibility with the Painlevé property\, a property closely associa
ted with integrable systems. While Masuda proved (C1) in 1983 for close-to
-constant initial data\, a generalization to other initial data is not kno
wn. Using computer assisted proofs we establish a branch singularity in th
e complex plane of time for specific\, large initial data which is not clo
se-to-constant.\n\nConcerning (C2)\, we demonstrate an open set of initial
data which is homoclinic to the 0-homogeneous-equilibrium\, proving (C2)
for close-to-constant initial data. This proof is then extended to a broad
er class of nonlinear Schrödinger equation without gauge invariance\, and
then used to prove the non-existence of any real-analytic conserved quant
ities. Indeed\, while numerical evidence suggests that most initial data i
s homoclinic to the 0-equilibrium\, there is more than meets the eye. Usin
g computer assisted proofs\, we establish an infinite family of unstable n
onhomogeneous equilibria\, as well as heteroclinic orbits traveling betwee
n these nonhomogeneous equilibria and the 0-equilibrium.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Michael Plum (Karlsruhe Institute of Technology)
DTSTART:20200707T140000Z
DTEND:20200707T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/3
DESCRIPTION:Title: Computer-assisted existence and multiplicity proofs for semilinear
elliptic problems on bounded and unbounded domains\nby Michael Plum (
Karlsruhe Institute of Technology) as part of CRM CAMP (Computer-Assisted
Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nMany boundary va
lue problems for semilinear elliptic partial differential equations allow
very stable numerical computations of approximate solutions\, but are stil
l lacking analytical existence proofs. In this lecture\, we propose a meth
od which exploits the knowledge of a "good" numerical approximate solution
\, in order to provide a rigorous proof of existence of an exact solution
close to the approximate one. This goal is achieved by a fixed-point argum
ent which takes all numerical errors into account\, and thus gives a mathe
matical proof which is not "worse" than any purely analytical one. A cruci
al part of the proof consists of the computation of eigenvalue bounds for
the linearization of the given problem at the approximate solution. The me
thod is used to prove existence and multiplicity statements for some speci
fic examples\, including cases where purely analytical methods had not bee
n successful.\n
LOCATION:https://stable.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:20260404T095849Z
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 (
Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract
\nWhitham’s equation of shallow water waves is a non-homogeneous non-loc
al dispersive equation. As in the case of the Stokes wave for the Euler eq
uation\, non-smooth traveling waves with greatest height between crest and
trough have been shown to exist. In this talk I will discuss uniqueness o
f solutions to the Whitham equation and show that there exists a unique\,
even and 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://stable.researchseminars.org/talk/CRM-CAMP/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nilima Nigam (Simon Fraser University)
DTSTART:20200728T140000Z
DTEND:20200728T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/5
DESCRIPTION:Title: A modification of Schiffer's conjecture\, and a proof via finite e
lements\nby Nilima Nigam (Simon Fraser University) as part of CRM CAMP
(Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstra
ct\nApproximations via conforming and non-conforming finite elements can b
e used to construct validated and computable bounds on eigenvalues for the
Dirichlet Laplacian in certain domains. If these are to be used as part o
f a proof\, care must be taken to ensure each step of the computation is v
alidated and verifiable. In this talk we present a long-standing conjectur
e in spectral geometry\, and its resolution using validated finite element
computations. Schiffer’s conjecture states that if a bounded domain Ω
in R^n has any nontrivial Neumann eigenfunction which is a constant on th
e boundary\, then Ω must be a ball. This conjecture is open. A modificati
on of Schiffer’s conjecture is: for regular polygons of at least 5 sides
\, we can demonstrate the existence of a Neumann eigenfunction which does
not change sign on the boundary. In this talk\, we provide a recent proof
using finite element calculations for the regular pentagon. The strategy i
nvolves iteratively bounding eigenvalues for a sequence of polygonal subdo
mains of the triangle with mixed Dirichlet and Neumann boundary conditions
. We use a learning algorithm to find and optimize this sequence of subdom
ains\, and use non-conforming linear FEM to compute validated lower bounds
for the lowest eigenvalue in each of these domains. The linear algebra is
performed within interval arithmetic. This is joint work with Bartlomiej
Siudeja and Ben Green at University of Oregon.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniel Wilczak (Jagiellonian University)
DTSTART:20200804T140000Z
DTEND:20200804T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/6
DESCRIPTION:Title: Rigorous numerical investigation of chaos and stability of periodi
c orbits in the Kuramoto-Sivashinsky PDE\nby Daniel Wilczak (Jagiellon
ian University) as part of CRM CAMP (Computer-Assisted Mathematical Proofs
) in Nonlinear Analysis\n\n\nAbstract\nWe give a computer-assisted proof o
f the existence of symbolic dynamics for a certain Poincaré map in the on
e-dimensional Kuramoto-Sivashinsky PDE. In particular\, we show the existe
nce of infinitely many (countably) periodic orbits (POs) of arbitrary larg
e principal periods. We provide also a study of the stability type of some
POs. The proof utilizes pure topological results (variant of the method o
f covering relations on compact absolute neighbourhood retracts) with rigo
rous integration 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. Zglic
zyński. A geometric method for infinite-dimensional chaos: symbolic dynam
ics for the Kuramoto-Sivashinsky PDE on the line\, Journal of Differential
Equations\, 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 on automatic differentiation and the Taylor method\, in preparation.
\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Renato Calleja (UNAM\, Mexico)
DTSTART:20200811T140000Z
DTEND:20200811T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/7
DESCRIPTION:Title: Torus knot choreographies in the n-body problem\nby Renato Cal
leja (UNAM\, Mexico) as part of CRM CAMP (Computer-Assisted Mathematical P
roofs) in Nonlinear Analysis\n\n\nAbstract\nn-body choreographies are peri
odic solutions to the n-body equations in which equal masses chase each ot
her around a fixed closed curve. In this talk I will present a systematic
approach for proving the existence of spatial choreographies in the gravit
ational body problem with the help of the digital computer. These arise fr
om the polygonal system of bodies in a rotating frame of reference. In rot
ating coordinates\, after exploiting the symmetries\, the equation of a ch
oreographic configuration is reduced to a delay differential equation (DDE
) describing the position and velocity of a single body. We prove that a d
ense set of Lyapunov orbits\, with frequencies satisfying a Diophantine eq
uation\, correspond to choreographies.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Xuefeng Liu (Niigata University\, Japan)
DTSTART:20200721T140000Z
DTEND:20200721T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/8
DESCRIPTION:Title: Solution verification for the stationary Navier-Stokes equation ov
er bounded non-convex 3D domains\nby Xuefeng Liu (Niigata University\,
Japan) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Non
linear Analysis\n\n\nAbstract\nWe consider the solution verification for t
he stationary Navier-Stokes equation over a bounded non-convex 3D domain
Ω. In 1999\, M.T. Nakao\, et al.\, reported a solution existence verifica
tion example for the 2D square domain. However\, it has been a difficult
problem to deal with general 2D domains and 3D domains\, due to the bottle
neck problem in the a priori error estimation for the linearized NS equat
ion. Recently\, by extending the hypercircle method (Prage-Synge's theorem
) to deal with the divergence-free condition in the Stokes equation\, the
explicit error estimation is constructed successfully based on a conformin
g finite element approach [arXiv:2006.02952]. Further\, we succeeded in t
he solution existence verification for the stationary NS equation in sever
al nonconvex 3D domains. In this talk\, I will show the latest progress o
n this topic\, including the rigorous estimation of the eigenvalue of Stok
es operator in 3D domains.\n
LOCATION:https://stable.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:20260404T095849Z
UID:CRM-CAMP/9
DESCRIPTION:Title: Computer-assisted proof of shear-induced chaos in stochastically p
erturbed Hopf systems\nby Maxime Breden & Maximilian Engel (École Pol
ytechnique\, France & Freie Universität Berlin\, Germany) as part of CRM
CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAb
stract\nIn this talk\, we discuss a long-standing conjecture concerning sh
ear-induced chaos in stochastically perturbed systems exhibiting a Hopf bi
furcation. Using the recently developed theory of conditioned Lyapunov exp
onents on bounded domains\, we reformulate the problem into the rigorous c
omputation of eigenvectors of some elliptic PDEs\, namely the Kolmogorov/F
okker-Planck equations describing distributions of the underlying stochast
ic process\, and are thus able to prove that the first Lyapunov exponent
is positive for certain parameter regimes.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Caroline Wormell (University of Sydney\, Australia)
DTSTART:20200818T140000Z
DTEND:20200818T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/10
DESCRIPTION:Title: Rigorously validated estimation of statistical properties of expa
nding maps\nby Caroline Wormell (University of Sydney\, Australia) as
part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Anal
ysis\n\nAbstract: TBA\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Akitoshi Takayasu (University of Tsukuba\, Japan)
DTSTART:20201006T140000Z
DTEND:20201006T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/11
DESCRIPTION:Title: Computer-assisted proofs for finding the monodromy of hypergeomet
ric differential equations\nby Akitoshi Takayasu (University of Tsukub
a\, Japan) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in
Nonlinear Analysis\n\n\nAbstract\nIn this talk\, we introduce a numerical
method for rigorously finding the monodromy matrix of hypergeometric diffe
rential equations. From a base point defined by fundamental solutions\, we
analytically continue the solution on a contour around a singular point o
f the differential equation using a rigorous integrator. Depending on the
contour we obtain the monodromy representation of fundamental solutions\,
which represents the fundamental group of the equation. As an application
of this method\, we consider a Picard-Fuchs type hypergeometric differenti
al equation arising from a polarized K3 surface. The monodromy matrix show
s a deformation of homologically independent 2-cycles for the surface alon
g the contour\, which is regarded as a change of characterization for the
K3 surface. This is joint work with Naoya Inoue (University of Tsukuba) an
d Toshimasa Ishige (Chiba University).\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Evelyn Sander (George Mason University\, USA)
DTSTART:20201027T140000Z
DTEND:20201027T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/12
DESCRIPTION:Title: Equilibrium validation in models for pattern formation based on S
obolev embeddings\nby Evelyn Sander (George Mason University\, USA) as
part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Ana
lysis\n\n\nAbstract\nIn this talk\, I describe a method of computer-assist
ed proof focused on continuation of solutions depending on a parameter. Th
ese techniques are applied to the Ohta-Kawasaki model for the dynamics of
diblock copolymers in dimensions one\, two\, and three. The functional ana
lytic approach and techniques can be generalized to other parabolic partia
l differential equations. This is joint work with Thomas Wanner (George Ma
son University).\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Blake Barker (Brigham Young University\, USA)
DTSTART:20201110T150000Z
DTEND:20201110T160000Z
DTSTAMP:20260404T095849Z
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
(Brigham Young University\, USA) as part of CRM CAMP (Computer-Assisted Ma
thematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nWe discuss recent
progress developing and applying rigorous computation to prove stability o
f traveling waves in the 1D Navier-Stokes equation. In particular\, we tal
k about rigorous computation of the Evans function\, an analytic function
whose zeros correspond to eigenvalues of the linearized PDE problem. Nonli
near stability results by Zumbrun and collaborators show that the underlyi
ng traveling waves are stable if there are no eigenvalues in the right hal
f of the complex plane. Thus one may use rigorous computation of the Evans
function to prove nonlinear-orbital stability of traveling waves.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/13/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gary Froyland (University of New South Wales\, Australia)
DTSTART:20201103T210000Z
DTEND:20201103T220000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/14
DESCRIPTION:Title: Stability and approximation of statistical limit laws\nby Gar
y Froyland (University of New South Wales\, Australia) as part of CRM CAMP
(Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstra
ct\nThe unpredictability of chaotic nonlinear dynamics leads naturally to
statistical descriptions\, including probabilistic limit laws such as the
central limit theorem and large deviation principle. A key tool in the Nag
aev-Guivarc'h spectral method for establishing statistical limit theorems
is a "twisted" transfer operator. We prove stability of the variance in th
e central limit theorem and the rate\nfunction from a large deviation prin
ciple with respect to deterministic and stochastic perturbations of the dy
namics and perturbations induced by numerical schemes. We then apply these
results to piecewise expanding maps in one and multiple dimensions. This
theory can be extended to uniformly hyperbolic maps and in this setting we
develop two new Fourier-analytic methods to provide the first rigorous es
timates of the variance and rate function for Anosov maps. This is joint
work with Harry Crimmins.\n
LOCATION:https://stable.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:20260404T095849Z
UID:CRM-CAMP/15
DESCRIPTION:Title: Computer assisted proofs of Arnold Diffusion\nby Maciej Capi
ński (AGH University of Science and Technology\, Poland) as part of CRM C
AMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbs
tract\nWe will present three methods that can be used for computer assiste
d proofs of Arnold diffusion in Hamiltonian systems. The first is the clas
sical Melnikov method\; the second is based a shadowing lemma in the setti
ng of the scattering map theory\; the last is based on topological shadowi
ng using correctly aligned windows and cones. We will also discuss an appl
ication in the setting of the Planar Elliptic Restricted Three Body Proble
m.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Elena Queirolo (Rutgers University\, USA)
DTSTART:20200915T140000Z
DTEND:20200915T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/16
DESCRIPTION:Title: Validating Hopf bifurcations in the Kuramoto-Sivashinsky PDE\
nby Elena Queirolo (Rutgers University\, USA) as part of CRM CAMP (Compute
r-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nWe pr
ove the existence of a Hopf bifurcation in the Kuramoto–Sivashinsky PDE.
For this\, we rewrite the Kuramoto–Sivashinsky equation into a desingul
arized formulation near the Hopf point via a blow-up approach and we apply
the radii polynomial approach to validate a solution branch of periodic s
olutions. Then this solution branch includes the Hopf bifurcation point.\n
LOCATION:https://stable.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:20260404T095849Z
UID:CRM-CAMP/17
DESCRIPTION:Title: A proof of Noise Induced Order in the BZ map\, and some remarks o
n the phenomenon\nby Isaia Nisoli (Universidade Federal do Rio de Jane
iro\, Brazil) as part of CRM CAMP (Computer-Assisted Mathematical Proofs)
in Nonlinear Analysis\n\n\nAbstract\nIn this talk I will present a Compute
r Aided Proof of Noise Induced Order (NIO) in a model associated with the
Belousov-Zhabotinsky reaction: when studying the random dynamical system w
ith additive noise associated to the BZ map\, as the noise amplitude incre
ases the Lyapunov exponent of the model transitions from positive to negat
ive. The proof is obtained through rigorous approximation of the stationar
y measure using Ulam method.\nI will also show a sufficient condition for
the existence of NIO in a wide family of one-dimensional examples.\n[1] S.
Galatolo\, M. Monge\, I. Nisoli "Existence of Noise Induced Order: a comp
uter aided proof"\, Nonlinearity 33(9)\n[2] I. Nisoli "Sufficient Conditio
ns for Noise Induced Order in 1-dimensional systems"\, arXiv:2003.08422\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Shane Kepley (Rutgers University\, USA)
DTSTART:20200922T140000Z
DTEND:20200922T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/18
DESCRIPTION:Title: Computing and validating collisions\, ejections\, and homoclinics
for the three body problem\nby Shane Kepley (Rutgers University\, USA
) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear
Analysis\n\n\nAbstract\nUnderstanding connecting and collision/ejection o
rbits is central to the study of transport in Celestial Mechanics. The atl
as algorithm combines the parameterization method with rigorous numerical
techniques for solving initial value problems in order to find and validat
e connecting orbits. However\, difficulties arise when parameterizing orbi
ts passing near a singularity such as “near miss” homoclinics or eject
ion/collision orbits. In this talk we present a method of overcoming this
obstacle based on rigorous Levi-Civita regularization which desingularizes
the vector field near the primaries. This regularization is performed dyn
amically allowing invariant manifolds to be parameterized globally\, even
near singularities.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Piotr Nowak (Polish Academy of Sciences\, Poland)
DTSTART:20200929T140000Z
DTEND:20200929T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/19
DESCRIPTION:Title: A computer-assisted proof of Kazhdan’s property (T) for automor
phism groups of free groups\nby Piotr Nowak (Polish Academy of Science
s\, Poland) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in
Nonlinear Analysis\n\n\nAbstract\nProperty (T) was introduced in 1967 by
Kazhdan and is an important rigidity property of groups. The most elementa
ry way to define it is through a fixed point property: a group G has prope
rty (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 rigidi
ty of actions and operator algebras associated to the group\, construction
s of expander graphs or constructions of counterexamples to Baum-Connes-ty
pe conjectures. \n\nIn this talk I will give a brief introduction to prope
rty (T) and explain the necessary group-theoretic background in order to p
resent a computer-assisted approach to proving property (T) by showing tha
t the Laplacian on the group has a spectral gap. This approach allowed us
show that Aut(F_n)\, the group of automorphisms of the free group F_n on n
generators\, has property (T) when n is at least 5: the case n=5 is joint
work with Marek Kaluba and Narutaka Ozawa\, and the case of n at least 6
is joint work with Kaluba and Dawid Kielak. Important aspects of our metho
ds include passing from a computational result to a rigorous proof and lat
er obtaining the result for an infinite family of groups using a single co
mputation. I will present an overview of these arguments.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Assia Mahboubi (Inria\, France & VU Amsterdam\, Netherlands)
DTSTART:20201020T140000Z
DTEND:20201020T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/20
DESCRIPTION:Title: Formally verified computer-assisted mathematical proofs\nby A
ssia Mahboubi (Inria\, France & VU Amsterdam\, Netherlands) as part of CRM
CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nA
bstract\nProof assistants are pieces of software designed for defining for
mally mathematical objects\, statement and proofs. In particular\, such a
formalization reduces the verification of proofs to a purely mechanical
well-formedness check. Since the early 70s\, proof\nassistants have been
extensively used for applications in program verification\, notably for s
ecurity-related issues. They have also been used to verify landmark resul
ts in mathematics\, including theorems with a computational proof\, like
the Four Colour Theorem (Appel and Haken\, 1977) or Hales and Ferguson's
proof of the Kepler conjecture (2005). This talk will discuss what are fo
rmalized mathematics and formal proofs\, and sketch the architecture of m
odern proof assistants. It will also showcase a few applications in forma
lly verified rigorous computation.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/20/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ferenc Bartha (Szeged University\, Hungary)
DTSTART:20201117T150000Z
DTEND:20201117T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/21
DESCRIPTION:Title: Stable periodic orbits for the Mackey-Glass equation\nby Fere
nc Bartha (Szeged University\, Hungary) as part of CRM CAMP (Computer-Assi
sted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nWe consider
the classical Mackey-Glass delay differential equation. By letting n go t
o infinity in the part encapsulating the delayed term\, we obtain a limiti
ng hybrid delay equation. We investigate how periodic solutions of this li
miting equation are related to periodic solutions of the original MG equat
ion for large n. Then\, we establish a procedure for constructing such per
iodic solutions via forward time integration. Finally\, we use rigorous nu
merics to establish the existence of stable periodic orbits for various pa
rameters of the MG equation. We note that some of these solutions exhibit
seemingly complicated dynamics\, yet they are stable periodic orbits.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Arnd Scheel (University of Minnesota\, USA)
DTSTART:20201201T150000Z
DTEND:20201201T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/22
DESCRIPTION:Title: Future Directions Series: Defect and front dynamics: analysis and
computation\nby Arnd Scheel (University of Minnesota\, USA) as part o
f CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n
\n\nAbstract\nThis will be a personal selection of results and related ope
n problems in dissipative spatially extended systems. I will focus on simp
le\, sometimes universal models such as the complex Ginzburg-Landau\, the
Swift-Hohenberg\, and extended KPP equations and attempts to describe thei
r dynamics based on coherent structures. I will present "conceptual' analy
tical results\, and describe gaps that rigorous computations may be able t
o close. Topics include invasion fronts\, defects in one- and two-dimensio
nal oscillatory media\, and point defects in striped phases.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/22/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gianni Arioli (Politecnico di Milano\, Italy)
DTSTART:20201124T150000Z
DTEND:20201124T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/23
DESCRIPTION:Title: Symmetry breaking and Hopf bifurcations for the planar Navier-Sto
kes equation\nby Gianni Arioli (Politecnico di Milano\, Italy) as part
of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis
\n\n\nAbstract\nWe consider the Navier-Stokes equation for an incompressib
le viscous fluid on a square\, satisfying Navier boundary conditions and b
eing subjected to a time-independent force. The uniqueness of stationary s
olutions is studied in dependence of the kinematic viscosity. For some par
ticular forcing\, it is shown that uniqueness persists on some continuous
branch of stationary solutions\, when the viscosity becomes arbitrarily sm
all. On the other hand\, for a different forcing\, a branch of symmetric s
olutions is shown to bifurcate\, giving rise to a secondary branch of nons
ymmetric 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
solution. Our proof is constructive and uses computer-assisted estimates.\
n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/23/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kevin Church (McGill University\, Canada)
DTSTART:20201013T140000Z
DTEND:20201013T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/24
DESCRIPTION:Title: Rigorous computation of periodic solutions and Floquet multiplier
s in delay differential equations with time-forced discontinuities\nby
Kevin Church (McGill University\, Canada) as part of CRM CAMP (Computer-A
ssisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nI will p
resent some recent work on rigorous computation of periodic solutions for
delay differential equations with impulse effects. At fixed moments in tim
e\, the state of such a system is reset and solutions become discontinuous
. Once a periodic solution of such a system has been computed\, its Floque
t spectrum can be rigorously computed by discretization of the monodromy o
perator (period map) and some technical error estimates. As an application
\, we compute a branch of periodic solutions in the pulse-harvested Hutchi
nson equation and examine its stability.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/24/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jean-Pierre Eckmann (University of Geneva\, Switzerland)
DTSTART:20201208T150000Z
DTEND:20201208T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/25
DESCRIPTION:Title: CRM-CAMP Colloquium\nby Jean-Pierre Eckmann (University of Ge
neva\, Switzerland) as part of CRM CAMP (Computer-Assisted Mathematical Pr
oofs) in Nonlinear Analysis\n\nAbstract: TBA\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/25/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nicolas Brisebarre (ENS Lyon\, France)
DTSTART:20210119T150000Z
DTEND:20210119T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/26
DESCRIPTION:Title: Correct rounding for transcendental functions\nby Nicolas Bri
sebarre (ENS Lyon\, France) as part of CRM CAMP (Computer-Assisted Mathema
tical Proofs) in Nonlinear Analysis\n\n\nAbstract\nOn a computer\, real nu
mbers are usually represented by a finite set of numbers called floating-p
oint numbers. When one performs an operation on these numbers\, such as an
evaluation by a function\, one returns a floating-point number\, hopefull
y close to the mathematical result of the operation. Ideally\, the returne
d result should be the exact rounding of this mathematical value. If we’
re only allowed a unique and fast evaluation (a constraint often met in pr
actice)\, one knows how to guarantee such a quality of results for arithme
tical operations like +\,−\,x\,/ and square root but\, as of today\, it
is still an issue when it comes to evaluate an elementary function such as
cos\, exp\, cube root for instance. This problem\, called Table Maker’s
Dilemma\, is actually a diophantine approximation problem. It was tackled
\, over the last fifteen years\, by V. Lefèvre\, J.M. Muller\, D. Stehlé
\, A. Tisserand and P. Zimmermann (LIP\, ÉNS Lyon and LORIA\, Nancy)\, us
ing tools from algorithmic number theory. Their work made it possible to p
artially solve this question but it remains an open problem. In this talk\
, I will present a joint work with Guillaume Hanrot (ÉNS Lyon\, LIP\, Ari
C) that improve on a part of the existing results.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/26/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robert Szczelina (Jagiellonian University\, Poland)
DTSTART:20210112T150000Z
DTEND:20210112T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/27
DESCRIPTION:Title: A computer assisted proof of chaos in a delayed perturbation of c
haotic ODE\nby Robert Szczelina (Jagiellonian University\, Poland) as
part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Anal
ysis\n\n\nAbstract\nWe will discuss some recent developments to the Taylor
method for forward in time rigorous integration of Delay Differential Equ
ations (DDEs) with constant delays. We briefly discuss how to generalize m
ethod of the paper "Algorithm for rigorous integration of Delay Differenti
al Equations and the computer-assisted proof of periodic orbits in the Mac
key-Glass equation\, Found. Comp. Math.\, 18 (6)\, 1299-1332\, 2018" to in
corporate multiple lags\, multiple variables (systems of equations) and ho
w to utilize "smoothing of solutions" to produce results of a far greater
accuracy\, especially when computing Poincaré maps between local sections
. We will apply this method to validate some covering relations between ca
refully selected sets under Poincaré maps defined with a flow associated
to a DDE. Together with standard topological arguments for compact maps it
will prove existence of a chaotic dynamics\, in particular the existence
of infinite (countable) number of periodic orbits. The DDE under considera
tion is a toy example made by adding a delayed term to the Rössler ODE un
der parameters for which chaotic attractor exists. The delayed term is sma
ll in amplitude\, but the lag time is macroscopic (not small). This is a j
oint work with Piotr Zgliczyński.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/27/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Anna Gierzkiewicz (University of Agriculture in Krakow\, Poland)
DTSTART:20210126T150000Z
DTEND:20210126T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/28
DESCRIPTION:Title: Periodic orbits in Roessler system\nby Anna Gierzkiewicz (Uni
versity of Agriculture in Krakow\, Poland) as part of CRM CAMP (Computer-A
ssisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nIn a joi
nt work with Piotr Zgliczynski\, we study the Roessler system with an attr
acting periodic orbit\, for two sets of parameters. In both cases the attr
actor on a Poincare section seems to be almost one-dimensional and therefo
re we apply the methods for two-dimensional perturbations of an interval's
self-map introduced by Zgliczynski in Multidimensional perturbations of o
ne-dimensional maps and stability of Sharkovskii ordering in 1999. We prov
e the existence of p-periodic orbits for almost all natural p with compute
r assistance: by interval Newton method and covering relations.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/28/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hans Koch (University of Texas at Austin\, USA)
DTSTART:20210202T150000Z
DTEND:20210202T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/29
DESCRIPTION:Title: Golden mean renormalization for the almost Mathieu operator and r
elated skew products\nby Hans Koch (University of Texas at Austin\, US
A) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinea
r Analysis\n\n\nAbstract\nWe renormalize SL(2\,R) skew-product maps over c
ircle rotations. Such maps arise e.g. in the spectral analysis of the Ho
fstadter Hamiltonian and the almost Mathieu operator. For rotations by th
e inverse golden mean\, we prove the existence of two renormalization-per
iodic orbits. We conjecture that there are infinitely many such orbits\,
and that the associated universal constants describe local scaling prop
erties of the Hofstadter spectrum and of the corresponding generalized ei
genvectors. Some recent results on trigonometric skew-product maps will
be described as well. This is joint work with Saša Kocić (UT Austin\, U
SA).\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/29/
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Sanders (Universidad Nacional Autonoma de Mexico\, Mexico)
DTSTART:20210209T150000Z
DTEND:20210209T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/30
DESCRIPTION:Title: Interval methods with Julia: Finding one million roots in one sec
ond\nby David Sanders (Universidad Nacional Autonoma de Mexico\, Mexic
o) as part of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinea
r Analysis\n\n\nAbstract\nThe Julia language provides a remarkably product
ive environment for scientific computing\, with a unique combination of in
teractivity and speed\, and is particularly suitable for defining operatio
ns on new mathematical objects\, such as intervals.\nI will present our fr
ee / open-source packages for interval arithmetic and interval methods (ju
liaintervals.github.io)\, written in pure Julia and comparable to state-of
-the-art libraries. They use the composability coming from Julia's "multip
le-dispatch"-based design and generic programming to integrate with other
packages in the "ecosystem"\, including linear algebra\, automatic differe
ntiation\, and plotting.\nThe foundation is IntervalArithmetic.jl \, which
is almost compliant with the IEEE-1788 standard. Applications currently i
mplemented include root finding\, global optimization\, constraint program
ming\, Taylor models\, and validated integration of ODEs.\nI will also sho
w how Julia's facilities for parallel computing allow us to create user-de
fined objects on GPUs and manipulate them using the same Julia code. As an
example benchmark\, we find and verify one million stationary points of t
he two-dimensional transcendental Griewank function in under one second.\n
Joint work with Luis Benet (ICF-UNAM).\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/30/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Konstantin Mischaikow (Rutgers University\, USA)
DTSTART:20210216T150000Z
DTEND:20210216T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/31
DESCRIPTION:Title: CRM-CAMP COLLOQUIUM: Wherefore computer assisted proofs in dynami
cs?\nby Konstantin Mischaikow (Rutgers University\, USA) as part of CR
M CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\n
Abstract\nOver the past few decades the topic of computer assisted proofs
in nonlinear dynamics has blossomed and is well on the way to becoming a s
tandard part of the field. So perhaps it is worth reflecting on some high
level topics. With this in mind I will discuss\, from an admittedly biased
personal perspective\, several questions:\nWhy do computer assisted proof
s?\nWhere do computer assisted proofs in dynamics as currently being done
lie in the bigger scheme of formal proof systems?\nWhat new perspective ab
out nonlinear dynamics can we extract from computer assisted proofs?\nHow
should we resolve the dichotomy between precision and accuracy?\nWhat role
do computer assisted proofs have to play as we move into an era of data d
riven science and machine learning?\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/31/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Florent Bréhard (Uppsala University\, Sweden)
DTSTART:20210223T150000Z
DTEND:20210223T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/32
DESCRIPTION:Title: Beyond Exponential Complexity of Newton-Galerkin Validation Metho
ds: A Polynomial-Time Newton-Picard Validation Algorithm for linear ODEs\nby Florent Bréhard (Uppsala University\, Sweden) as part of CRM CAMP
(Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstrac
t\nA wide range of techniques have been developed to compute validated num
erical solutions to various kind of equations (e.g.\, ODE\, PDE\, DDE) ari
sing in computer-assisted proofs. Among them are Newton-Galerkin a posteri
ori validation techniques\, which provide error bounds for approximate sol
utions by using the contraction map principle in a suitable coefficient sp
ace (e.g.\, Fourier or Chebyshev). More precisely\, a contracting Newton-l
ike operator is constructed by truncating and inverting the inverse Jacobi
an of the equation.\nWhile these techniques were extensively used in cutti
ng-edge works in the community\, we show that they suffer from an exponent
ial running time w.r.t. the input equation. We illustrate this shortcoming
s on simple linear ODEs\, where a "large" parameter in the equation leads
to an intractable instance for Newton-Galerkin validation algorithms.\nFro
m this observation\, we build a new validation scheme\, called Newton-Pica
rd\, which breaks this complexity barrier. The key idea consists in replac
ing the inverse Jacobian not by a finite-dimensional truncated matrix as i
n Newton-Galerkin\, but by an integral operator with a polynomial approxim
ation of the so-called resolvent kernel. Moreover\, this method is also le
ss basis-dependent and more suitable to be formalized in a computer proof
assistant towards a fully certified implementation in the future.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/32/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alessandra Celletti (University of Rome Tor Vergata\, Italy)
DTSTART:20210309T150000Z
DTEND:20210309T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/33
DESCRIPTION:Title: KAM (computer-assisted) results in Celestial Mechanics: the dissi
pative spin-orbit problem\nby Alessandra Celletti (University of Rome
Tor Vergata\, Italy) as part of CRM CAMP (Computer-Assisted Mathematical P
roofs) in Nonlinear Analysis\n\n\nAbstract\nThe existence of invariant tor
i through Kolmogorov-Arnold-Moser (KAM) theory has been proven in several
models of Celestial Mechanics through dedicated analytical proofs combined
with computer-assisted techniques. After reviewing some of such results\,
obtained in conservative frameworks\, we present a recent result on the e
xistence of invariant attractors for a dissipative model: the spin-orbit p
roblem with tidal torque. This model belongs to the class of conformally s
ymplectic systems\, which are characterized by the property that they tran
sform the symplectic form into a multiple of itself. Finding the solution
of such systems requires to add a drift parameter.\n\nWe describe a KAM th
eorem for conformally symplectic systems in an a-posteriori format: assumi
ng the existence of an approximate solution\, satisfying the invariance eq
uation up to an error term - small enough with respect to explicit conditi
on numbers\, - then we can prove the existence of a solution nearby. The t
heorem\, which does not assume that the system is close to integrable\, yi
elds an efficient algorithm to construct invariant attractors for the spin
-orbit problem and it provides accurate estimates of the breakdown thresho
ld of the invariant attractor.\n\nThis talk refers to joint works with R.
Calleja\, J. Gimeno\, and R. de la Llave.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/33/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Shin'ichi Oishi (Waseda University\, Japan)
DTSTART:20210316T140000Z
DTEND:20210316T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/34
DESCRIPTION:Title: Computer assisted existence proof of complicated dynamics in forc
ed delay action oscillator modelling El Nino phenomena\nby Shin'ichi O
ishi (Waseda University\, Japan) as part of CRM CAMP (Computer-Assisted Ma
thematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nA computer assiste
d proof is presented for the existence of various periodic solutions for f
orced Suarez-Schopf's equation\, which are delay differential equations mo
deling El Nino. Tight inclusions of periodic solutions are calculated thro
ugh numerical verification method by utilizing a structure of Galerkin's e
quation for forced Suarez-Schopf's equation effectively. The existence of
various periodic solutions has been proved via computer assisted proofs in
cluding various subharmonics. Especially\, coexistence of several subharmo
nics are proved and numerical simulations are presented suggesting an appe
arance of chaos.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/34/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Piotr Kalita (Jagiellonian University\, Poland)
DTSTART:20210406T140000Z
DTEND:20210406T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/36
DESCRIPTION:Title: Rigorous FEM based forward in time integration of dissipative PDE
s\nby Piotr Kalita (Jagiellonian University\, Poland) as part of CRM C
AMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbs
tract\nWe present the technique for computer assisted rigorous forward in
time integration of problems governed by dissipative PDEs. The approach is
based on the Finite Element Method. The key concepts lie in the propagati
on of the a priori energy estimates needed to bound the infinite dimension
al remainder and in rigorous integration of differential inclusions. The t
echnique is illustrated by the computer assisted construction of the time
periodic solution for periodically forced one-dimensional Burgers equation
with homogeneous Dirichlet boundary conditions. Talk is based on joint wo
rk with Piotr Zgliczyński.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/36/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Warwick Tucker (Monash University\, Australia)
DTSTART:20210413T140000Z
DTEND:20210413T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/37
DESCRIPTION:Title: Relative equilibria for the n-body problem\nby Warwick Tucker
(Monash University\, Australia) as part of CRM CAMP (Computer-Assisted Ma
thematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nWe will discuss th
e classical problem from celestial mechanics of determining the number of
relative equilibria a set of planets can display. Several already establis
hed results 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 possi
ble extensions to harder instances of the general problem. This is joint w
ork with Piotr Zgliczynski and Jordi-Lluis Figueras.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/37/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alberto Bressan (Penn State University\, USA)
DTSTART:20210420T140000Z
DTEND:20210420T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/38
DESCRIPTION:Title: Non-uniqueness and error bounds for fluid flow\nby Alberto Br
essan (Penn State University\, USA) as part of CRM CAMP (Computer-Assisted
Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nFor hyperbolic
systems of conservation laws in one space dimension\, a general existence
-uniqueness theory is now available\, for entropy weak solutions with boun
ded variation. In several space dimensions\, however\, it seems unlikely
that a similar theory can be achieved.\n\nFor the 2-D Euler equations\, i
n this talk I shall discuss the simplest possible examples of Cauchy pro
blems admitting multiple solutions. Several numerical simulations will be
presented\, for incompressible as well as compressible flow\, indicatin
g the existence of two distinct solutions for the same initial data. Typi
cally\, one of the solutions contains a single spiraling vortex\, while th
e other solution contains two vortices.\n\nSome theoretical work\, aimed a
t validating the numerical results\, will also be discussed.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/38/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kaname Matsue (Kyushu University\, Japan)
DTSTART:20210504T140000Z
DTEND:20210504T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/39
DESCRIPTION:Title: Rigorous numerics of blow-up solutions for autonomous ODEs\nb
y Kaname Matsue (Kyushu University\, Japan) as part of CRM CAMP (Computer-
Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nHere I
talk about the recent studies concerning rigorous numerics of blow-up solu
tions for autonomous ODEs in a systematic way under a mild assumption of v
ector fields. The fundamental tools used here are “compactifications”
of phase spaces which map the infinity to the boundary of transformed ph
ase spaces (the “horizon”)\, and “time-scale desingularizations dete
rmined by the original vector fields”. Blow-up solutions are then essen
tially transformed into solutions on stable manifolds of invariant sets on
the horizon. In particular\, rigorous enclosures of blow-up solutions an
d their blow-up times can be validated by means of standard machineries of
dynamical systems such as ODE integrators\, locally defined Lyapunov func
tions and parameterization of invariant manifolds. Dynamical system appro
ach shown here reveals many quantitative and qualitative nature of blow-up
behavior for various concrete dynamical systems. A series of works prese
nted in the present talk (involving rigorous numerics) are based on joint
works with Profs. Akitoshi Takayasu\, Nobito Yamamoto and Jean-Philippe Le
ssard.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/39/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Thomas Wanner (George Mason University\, USA)
DTSTART:20210518T140000Z
DTEND:20210518T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/40
DESCRIPTION:Title: Bifurcation Points in the Ohta-Kawasaki Model\nby Thomas Wann
er (George Mason University\, USA) as part of CRM CAMP (Computer-Assisted
Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nDiblock copolyme
rs are a class of materials formed by the reaction of two linear polymers.
The different structures taken on by these polymers grant them special pr
operties\, which can prove useful in applications such as the development
of new adhesives and asphalt additives. We consider a model for the format
ion of diblock copolymers first proposed by Ohta and Kawasaki\, which is a
Cahn-Hilliard-like equation together with a nonlocal term. Unlike the Cah
n-Hilliard model\, even on one-dimensional spatial domains the steady stat
e bifurcation diagram of the Ohta-Kawasaki model is still not fully unders
tood. We therefore present computer-assisted proof techniques which can be
used to validate and continue its bifurcation points. This includes not o
nly fold points\, but also pitchfork bifurcations which are the result of
a cyclic group action beyond forcing through Z_2 symmetries.\n
LOCATION:https://stable.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:20260404T095849Z
UID:CRM-CAMP/41
DESCRIPTION:Title: Chaos in the Chua's circuit\nby Zbigniew Galias (AGH Universi
ty of Science and Technology\, Poland) as part of CRM CAMP (Computer-Assis
ted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nSeveral resu
lts on the existence of chaos in the Chua's circuit with piesewise linear
and cubic nonlinearities will be presented.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/41/
END:VEVENT
BEGIN:VEVENT
SUMMARY:J.D. Mireles James (Florida Atlantic University\, USA)
DTSTART:20210302T150000Z
DTEND:20210302T160000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/42
DESCRIPTION:Title: Boundary value problems and transversality in conservative system
s: computer assisted proofs of connection and collision orbits\nby J.D
. Mireles James (Florida Atlantic University\, USA) as part of CRM CAMP (C
omputer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\
nI'll discuss a framework for two-point boundary value problems in conserv
ative systems which detects transversality\, allows for the possibility of
multiple changes of coordinates\, and leads naturally to computer assiste
d proofs. The set-up applies to dynamical problems in the level set like
finding connecting orbits between hyperbolic invariant objects and collisi
ons. The main technical difficulty is that the conserved quantity leads t
o overdetermined systems of equations. This problem can be overcome in a
number of different ways\, including elimination of an equation\, by explo
iting discrete symmetries (if any)\, or by introducing a new variable call
ed an unfolding parameter. I'll look at two common ways of defining unfo
lding parameters and show that they don't disrupt the transversality prope
rties of the BVP. I'll also illustrate some applications of this setup to
computer assisted proofs of connecting orbits and collisions in the circu
lar restricted three body problem. This is joint work with Shane Kepley a
nd Maciej Capinski.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/42/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jean-Philippe Lessard (McGill University\, Canada)
DTSTART:20210330T140000Z
DTEND:20210330T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/43
DESCRIPTION:Title: Computer-assisted proofs for Cauchy problems of delay equations a
nd PDEs via Chebyshev series\nby Jean-Philippe Lessard (McGill Univers
ity\, Canada) as part of CRM CAMP (Computer-Assisted Mathematical Proofs)
in Nonlinear Analysis\n\n\nAbstract\nIn this talk we introduce recent gene
ral methods to rigorously compute solutions of infinite dimensional Cauchy
problems. The idea is to expand the solutions in time using Chebyshev se
ries and use the contraction mapping theorem to construct a neighbourhood
about an approximate solution which contains the exact solution of the Cau
chy problem. We apply the methods to delay differential equations and to s
emi-linear parabolic partial differential equations.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/43/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Antoine Zurek (Technische Universität Wien\, Austria)
DTSTART:20210323T140000Z
DTEND:20210323T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/44
DESCRIPTION:Title: Existence of traveling wave solutions for the Diffusion Poisson C
oupled Model: a computer-assisted proof\nby Antoine Zurek (Technische
Universität Wien\, Austria) as part of CRM CAMP (Computer-Assisted Mathem
atical Proofs) in Nonlinear Analysis\n\n\nAbstract\nIn France one option u
nder study for the storage of high-level radioactive waste is based on an
underground repository. More precisely\, the waste shall be confined in a
glass matrix and then placed into cylindrical steel canisters. These conta
iners shall be placed into micro-tunnels in the highly impermeable Callovo
-Oxfordian claystone layer at a depth of several hundred meters. The Diffu
sion Poisson Coupled Model (DPCM) aims to investigate the safety of such l
ong term repository concept by describing the corrosion processes appearin
g at the surface of carbon steel canisters in contact with a claystone for
mation. It involves drift-diffusion equations on the density of species (e
lectrons\, ferric cations and oxygen vacancies)\, coupled with a Poisson e
quation on the electrostatic potential and with moving boundary equations.
So far\, no theoretical results giving a precise description of the solut
ions\, or at least under which conditions the solutions may exist\, are av
alaible in the literature. However\, a finite volume scheme has been devel
oped to approximate the equations of the DPCM model. In particular\, it wa
s observed numerically the existence of traveling wave solutions for the D
PCM model. These solutions are defined by stationary profiles on a fixed s
ize domain with interfaces moving at the same velocity. The main objective
of this talk is to present how we apply a computer-assisted method in ord
er to prove the existence of such traveling wave solutions for the system.
This approach allows us to obtain for the first time a precise and certif
ied description of some solutions. \nThis work is in collaboration with Ma
xime Breden and Claire Chainais-Hillairet.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/44/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Charles Fefferman (Princeton University\, USA)
DTSTART:20210601T140000Z
DTEND:20210601T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/45
DESCRIPTION:Title: CRM CAMP Colloquium: Encounters with Computer-Assisted Proofs in
Early Days\nby Charles Fefferman (Princeton University\, USA) as part
of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\
n\n\nAbstract\nThe talk recounts how computer-assisted proofs came into tw
o theorems on the quantum mechanics of Coulomb systems during the 1980's.\
n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/45/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joel Dahne (Uppsala University\, Sweden)
DTSTART:20210427T140000Z
DTEND:20210427T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/46
DESCRIPTION:Title: A computer assisted counterexample to Payne’s nodal line conjec
ture with few holes\nby Joel Dahne (Uppsala University\, Sweden) as pa
rt of CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analys
is\n\n\nAbstract\nPayne conjectured in 1967 that the nodal line of the sec
ond Dirichlet eigenfunction must touch the boundary of the domain. In thei
r 1997 breakthrough paper\, Hoffmann-Ostenhof\, Hoffmann-Ostenhof and Nadi
rashvili proved this to be false by constructing a counterexample in the p
lane with an unspecified\, but large\, number of holes and raised the ques
tion of the minimum number of holes a counterexample can have. In this tal
k I will present a computer assisted counter example with 6 holes. This is
joint work with Javier Gómez-Serrano and Kimberly Hou.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/46/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Marian Mrozek (Jagiellonian University\, Poland)
DTSTART:20210622T140000Z
DTEND:20210622T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/47
DESCRIPTION:Title: Combinatorial Topological Dynamics\nby Marian Mrozek (Jagiell
onian University\, Poland) as part of CRM CAMP (Computer-Assisted Mathemat
ical Proofs) in Nonlinear Analysis\n\n\nAbstract\nSince the publication in
1998 of the seminal work by Robin Forman on combinatorial Morse theory th
ere has been growing interest in dynamical systems on finite spaces. The m
ain motivation to study combinatorial dynamics comes from data science. Bu
t\, they also provide very concise models of dynamical phenomena and show
some potential in certain computer assisted proofs in dynamics.\n\nIn the
talk I will present the basic ideas of Conley theory for combinatorial dyn
amical system\, particularly for a combinatorial multivector field which i
s a generalization of combinatorial vector field introduced by Forman. The
theory is based on concepts which are analogous to the concepts of classi
cal theory: isolating neighborhood\, isolated invariant set\, index pair\,
Conley index\, Morse decomposition\, connection matrix. The concepts are
analogous but in some cases surprisingly different in details. This may be
explained by the non-Hausdorff nature of combinatorial topological spaces
.\n\nDespite the differences there seem to be strong formal ties between t
he combinatorial and classical dynamics on topological level. A Morse deco
mposition of a combinatorial vector field on an abstract simplicial comple
x induces a semiflow on the geometric realization of the complex with a Mo
rse decomposition exhibiting the same Conley-Morse graph. Actually\, this
correspondence of Morse decompositions and Conley-Morse graphs applies to
every semiflow which is transversal to the boundaries of top dimensional c
ells of a certain cellular decomposition of the phase space associated wit
h the combinatorial vector field.\n\nThere is also a formal relation in th
e opposite direction. Given a smooth flow and a cellular decomposition of
its phase space which is transversal to the flow\, there is an induced com
binatorial multivector field on the cellular structure of the phase space.
Moreover\, if the induced combinatorial multivector field admits a period
ic trajectory with an appropriate Conley index\, a periodic orbit exists a
lso for the original smooth flow.\n\nThe formal ties seem to provide a nat
ural framework for a rigorous global analysis of the dynamics of a flow: t
he decomposition into the gradient and recurrent part together with the co
mputation of the Conley-Morse graph\, connection matrix and revealing the
internal structure of the recurrent part.\n\nBased on joint work with J. B
armak\, T. Dey\, M. Juda\, T. Kaczynski\, T. Kapela\, J. Kubica\, M. Lip
iński R. Slechta\, R. Srzednicki\, J. Thorpe and Th. Wanner.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/47/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Vladimir Sverak (University of Minnesota)
DTSTART:20210608T140000Z
DTEND:20210608T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/48
DESCRIPTION:Title: OPEN PROBLEMS SERIES: Some conjectures that seem difficult to pro
ve\nby Vladimir Sverak (University of Minnesota) as part of CRM CAMP (
Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract
\nIn many cases\, numerics and/or heuristics provide compelling evidence f
or statements that we have trouble proving rigorously. I will discuss some
examples\, mostly inspired by fluid flows.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/48/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jonathan Jaquette (Boston University\, USA)
DTSTART:20210511T140000Z
DTEND:20210511T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/49
DESCRIPTION:Title: A computer assisted proof of Wright's conjecture: counting and di
scounting slowly oscillating periodic solutions to a DDE\nby Jonathan
Jaquette (Boston University\, USA) as part of CRM CAMP (Computer-Assisted
Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\nA classical exam
ple 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 attracto
r for all $\\alpha \\in ( 0 \, \\pi/2]$\; and Jones' conjecture\, which s
tates that there is a unique slowly oscillating periodic solution for $\\a
lpha > \\pi /2 $. \n\nTo prove Wright's conjecture our approach relies on
a careful investigation of the neighborhood of the Hopf bifurcation occurr
ing at $\\alpha = \\pi/ 2$. Using a rigorous numerical integrator we chara
cterize slowly oscillating periodic solutions and calculate their stabilit
y\, proving Jones' conjecture for $\\alpha \\in [1.9\,6.0]$ and thereby al
l $\\alpha \\geq 1.9$. We complete the proof of Jones conjecture using glo
bal optimization methods\, extended to treat infinite dimensional problems
.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/49/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrew Burbanks (University of Portsmouth\, UK)
DTSTART:20210629T140000Z
DTEND:20210629T150000Z
DTSTAMP:20260404T095849Z
UID:CRM-CAMP/50
DESCRIPTION:Title: Computer-assisted proofs for renormalisation fixed-points and eig
enfunctions for period-doubling universality in maps of the interval\n
by Andrew Burbanks (University of Portsmouth\, UK) as part of CRM CAMP (Co
mputer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract\n
We prove the existence of a fixed point to the renormalisation operator fo
r period doubling in maps of even degree at the critical point. We work wi
th a modified operator that encodes the action of the renormalisation oper
ator on even functions. Building on previous work\, our proof uses rigorou
s computer-assisted means to bound operations in a space of analytic funct
ions and hence to show that a quasi-Newton operator for the fixed-point pr
oblem is a contraction map on a suitable ball.\n\nWe bound the spectrum of
the Frechet derivative of the renormalisation operator at the fixed point
\, establishing the hyperbolic structure\, in which the presence of a sing
le essential expanding eigenvalue explains the universal asymptotically se
lf-similar bifurcation structure observed in the iterations of families of
maps lying in the relevant universality class.\n\nBy recasting the eigenp
roblem for the Frechet derivative in a particular nonlinear form\, we agai
n use the contraction mapping principle to gain rigorous bounds on eigenfu
nctions and their corresponding eigenvalues. In particular\, we gain tight
bounds on the eigenfunction corresponding to the essential expanding eige
nvalue delta. We adapt the procedure to the eigenproblem for the scaling o
f added uncorrelated noise.\n\nOur computations use multi-precision interv
al arithmetic with rigorous directed rounding modes to bound tightly the c
oefficients of the relevant power series and their high-order terms\, and
the corresponding universal constants.\n
LOCATION:https://stable.researchseminars.org/talk/CRM-CAMP/50/
END:VEVENT
END:VCALENDAR