Skip to content

Commit

Permalink
bump mathlib
Browse files Browse the repository at this point in the history 
fix some Lean definitions, some blueprint typos, and add a leanok
  • Loading branch information
@fpvandoorn
fpvandoorn committed Jun 25, 2024
1 parent a25d65f commit da09006
Show file tree
Hide file tree
Showing 5 changed files with 37 additions and 62 deletions.
4 changes: 2 additions & 2 deletions Carleson/Defs.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -315,8 +315,8 @@ end ProofData
class ProofData {X : Type*} (a q : outParam ℝ) (K : outParam (X → X → ℂ))
(σ₁ σ₂ : outParam (X → ℤ)) (F G : outParam (Set X)) [PseudoMetricSpace X]
extends PreProofData a q K σ₁ σ₂ F G where
F_subset : F ⊆ ball (cancelPt X) (defaultD a ^ S X)
G_subset : G ⊆ ball (cancelPt X) (defaultD a ^ S X)
F_subset : F ⊆ ball (cancelPt X) (defaultD a ^ S X / 4)
G_subset : G ⊆ ball (cancelPt X) (defaultD a ^ S X / 4)


namespace ShortVariables
Expand Down
2 changes: 1 addition & 1 deletion Carleson/GridStructure.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ class GridStructure
ball_subset_𝓓 {i} : ball (c i) (D ^ s i / 4) ⊆ coe𝓓 i --2.0.10
𝓓_subset_ball {i} : coe𝓓 i ⊆ ball (c i) (4 * D ^ s i) --2.0.10
small_boundary {i} {t : ℝ} (ht : D ^ (- S - s i) ≤ t) :
volume.real { x ∈ coe𝓓 i | infDist x (coe𝓓 i)ᶜ ≤ t * D ^ s i } ≤ D * t ^ κ * volume.real (coe𝓓 i)
volume.real { x ∈ coe𝓓 i | infDist x (coe𝓓 i)ᶜ ≤ t * D ^ s i } ≤ 2 * t ^ κ * volume.real (coe𝓓 i)

export GridStructure (range_s_subset 𝓓_subset_biUnion ball_subset_𝓓 𝓓_subset_ball small_boundary
topCube s_topCube c_topCube subset_topCube) -- should `X` be explicit in topCube?
Expand Down
56 changes: 20 additions & 36 deletions blueprint/src/chapter/main.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,6 +146,8 @@ \chapter{Introduction}
$1<q<2$.
\begin{theorem}[metric space Carleson]
\label{metric-space-Carleson}
\leanok
\lean{metric_carleson}
\uses{R-truncation}
For all integers $a \ge 4$ and real numbers $1<q\le 2$
the following holds.
Expand All @@ -161,7 +163,7 @@ \chapter{Introduction}
$|f|\le \mathbf{1}_F$, we have, with $T$ defined in \eqref{def-main-op},
\begin{equation}
\label{resweak}
\left|\int_{G} T f \, \mathrm{d}\mu\right| \leq \frac{2^{450a^3}}{(q-1)^5} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}}\, .
\left|\int_{G} T f \, \mathrm{d}\mu\right| \leq \frac{2^{450a^3}}{(q-1)^6} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}}\, .
\end{equation}
\end{theorem}

Expand Down Expand Up @@ -264,7 +266,7 @@ \chapter{Proof of Metric Space Carleson, overview}
\end{equation*}
\begin{equation}
\label{eq-linearized}
\le \frac{2^{440a^3}}{(q-1)^4} \mu(G)^{1-\frac{1}{q}}
\le \frac{2^{440a^3}}{(q-1)^5} \mu(G)^{1-\frac{1}{q}}
\mu(F)^{\frac 1 q}\,.
\end{equation}
\end{proposition}
Expand Down Expand Up @@ -301,7 +303,7 @@ \chapter{Proof of Metric Space Carleson, overview}
%\begin{equation}\label{coverball}
% B(o, \frac{1}{4} D^{S}) \subset I\,,
%\end{equation}
and for all cubes $J \in \mathcal{D}$, we have
and for all cubes $J \in \mathcal{D}$, we have
\begin{equation}\label{subsetmaxcube}
J \subset I_0\,.
\end{equation}
Expand All @@ -314,25 +316,11 @@ \chapter{Proof of Metric Space Carleson, overview}
For any dyadic cube $I$ and any $t$ with $tD^{s(I)} \ge D^{-S}$,
\begin{equation}
\label{eq-small-boundary}
% fixme(Georges Gonthier): (not necessary) The D in the RHS can be replaced by 2.
% We can do the same in the statement and proof of {boundary-measure}.
% Done in Tex, ToDo: Change in Lean.
\mu(\{x \in I \ : \ \rho(x, X \setminus I) \leq t D^{s(I)}\}) \le 2 t^\kappa \mu(I)\,.
\end{equation}





% fixme (simplification):
% We can make \mathcal(Q) take values Q(X), and still cover all of Q(X).
% We can do this by making \mathcal{Z} a subset of Q(X) satisfying 4.2.2.
% This would remove the need for Lemma 2.1.1 for the definition of \mathcal{Z} in Section 4.2, since it will be automatically finite, since Q(X) is finite.
% This condition is already implicitly used in the proof of Lemma 6.1.6 when using (2.0.13)

%Done in tex


A tile structure $(\fP,\scI,\fc,\fcc,\pc,\ps)$
for a given grid structure $(\mathcal{D}, c, s)$
is a finite set $\fP$ of elements called tiles with five maps
Expand Down Expand Up @@ -657,7 +645,7 @@ \section{Auxiliary lemmas}
\begin{lemma}[monotone cube metrics]
\label{monotone-cube-metrics}
\leanok
\lean{��.dist_mono, ��.dist_strictMono}
\lean{𝓓.dist_mono, 𝓓.dist_strictMono} % Overleaf might scramble these characters (`\MCD`)
Let $(\mathcal{D}, c, s)$ be a grid structure. Denote for cubes $I \in \mathcal{D}$
$$
I^\circ := B(c(I), \frac{1}{4} D^{s(I)})\,.
Expand Down Expand Up @@ -779,7 +767,7 @@ \chapter{Proof of Metric Space Carleson}
\left| T_{R_1,R_2,\mfa} \mathbf{1}_{F}(x) \right|\, d\mu(x)
$$
\begin{equation} \label{Rcut}
\leq \frac{2^{450a^3}}{(q-1)^5} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}},
\leq \frac{2^{450a^3}}{(q-1)^6} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}},
\end{equation}
where
\begin{equation}\label{TRR}
Expand Down Expand Up @@ -818,7 +806,7 @@ \chapter{Proof of Metric Space Carleson}
\left| T_{1, s_1,s_2,\mfa} \mathbf{1}_{F}(x) \right|\, d\mu(x)
$$
\begin{equation} \label{Scut}
\leq \frac{2^{446a^3}}{(q-1)^5} \mu(G)^{1 - \frac{1}{q}} \mu(F)^{\frac{1}{q}},
\leq \frac{2^{446a^3}}{(q-1)^6} \mu(G)^{1 - \frac{1}{q}} \mu(F)^{\frac{1}{q}},
\end{equation}
where $T_{1, s_1,s_2,\mfa}$ is defined in \eqref{middles}.
\end{lemma}
Expand Down Expand Up @@ -849,7 +837,7 @@ \chapter{Proof of Metric Space Carleson}
\left| T_{1, s_1,s_2,\mfa} \mathbf{1}_{F}(x) \right|\, d\mu(x)
$$
\begin{equation} \label{Sqcut}
\leq \frac{2^{445a^3}}{(q-1)^5} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}}\,.
\leq \frac{2^{445a^3}}{(q-1)^6} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}}\,.
\end{equation}
\end{lemma}

Expand Down Expand Up @@ -907,7 +895,7 @@ \chapter{Proof of Metric Space Carleson}
\end{align*}
Combining this with \Cref{finitary-S-truncation} and the fact that
\begin{align*}
\frac{2^{102 a^3+4a}q}{q-1}\leq \frac{2^{445a^3}}{(q-1)^5}
\frac{2^{102 a^3+4a}q}{q-1}\leq \frac{2^{445a^3}}{(q-1)^6}
\end{align*}
proves \Cref{S-truncation}.

Expand All @@ -923,7 +911,7 @@ \chapter{Proof of Metric Space Carleson}
\begin{equation} \label{Sqlin}
\int \mathbf{1}_{G}(x)
\left| {T}_{2,\sigma_1,\sigma_2,\tQ}\mathbf{1}_F(x)\right|\, d\mu(x)
\le \frac{2^{445a^3}}{(q-1)^5} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}},
\le \frac{2^{445a^3}}{(q-1)^6} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}},
\end{equation}
with
\begin{equation}\label{middles1}
Expand Down Expand Up @@ -973,13 +961,13 @@ \chapter{Proof of Metric Space Carleson}
\left| {T}_{2,\sigma_1,\sigma_2, \tQ} \mathbf{1}_{F}(x) \right|\, d\mu(x)
\end{equation*}
\begin{equation}
\le \frac{2^{440a^3}}{(q-1)^4} \mu(G_n)^{1 - \frac{1}{q}} \mu(F)^{\frac{1}{q}},
\le \frac{2^{440a^3}}{(q-1)^5} \mu(G_n)^{1 - \frac{1}{q}} \mu(F)^{\frac{1}{q}},
\end{equation}
Adding the first $n$ of these inequalities, we obtain by bounding a geometric series
\begin{equation} \label{Sqcut2}
\int \mathbf{1}_{G\setminus G_{n}}(x)
\left| {T}_{2,\sigma_1,\sigma_2, \tQ}\mathbf{1}_F(x) \right|\, d\mu(x)
\le \frac{2^{445a^3}}{(q-1)^5} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}}.
\le \frac{2^{445a^3}}{(q-1)^6} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}}.
\end{equation}
As the integrand is bounded by
\begin{equation}\mathbf{1}_{G\setminus G_{n}}(x)
Expand All @@ -990,7 +978,7 @@ \chapter{Proof of Metric Space Carleson}
\begin{equation} \label{Sqcut3}
\int \mathbf{1}_{G}(x)
\left| {T}_{2,\sigma_1,\sigma_2, \tQ}\mathbf{1}_F(x) \right|\, d\mu(x)
\le \frac{2^{445a^3}}{(q-1)^5} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}}.
\le \frac{2^{445a^3}}{(q-1)^6} \mu(G)^{1-\frac{1}{q}} \mu(F)^{\frac{1}{q}}.
\end{equation}


Expand Down Expand Up @@ -1088,7 +1076,7 @@ \chapter{Proof of Finitary Carleson}
\end{equation}
\begin{equation}
=\int_{G \setminus G'} \left|\sum_{\fp\in \fP}T_{\fp} f(x)\right| \mathrm{d}\mu(x)
\le \frac{2^{440a^3}}{(q-1)^4} \mu(G)^{1 - \frac{1}{q}} \mu(F)^{\frac{1}{q}} \,.
\le \frac{2^{440a^3}}{(q-1)^5} \mu(G)^{1 - \frac{1}{q}} \mu(F)^{\frac{1}{q}} \,.
\end{equation}
This proves \eqref{eq-linearized} for the chosen set $G'$ and arbitrary $f$ and thus completes the proof of Proposition
\ref{finitary-Carleson}.
Expand Down Expand Up @@ -1496,10 +1484,10 @@ \section{Proof of Grid Existence Lemma}
We first show that $(\tilde{\mathcal{D}},c,s)$ satisfies properties \eqref{coverdyadic}, \eqref{dyadicproperty}, \eqref{eq-vol-sp-cube} and \eqref{eq-small-boundary}. Property \eqref{eq-vol-sp-cube}
follows from \eqref{squeezedyadic}, while \eqref{eq-small-boundary} follows from \Cref{boundary-measure}.

Let $x\in B(o, D^S)$.
Let $x\in B(o, D^S)$.
We show properties
\eqref{coverdyadic} and
\eqref{dyadicproperty}
\eqref{dyadicproperty}
for $(\tilde{\mathcal{D}},c,s)$ and $x$.

We first show \eqref{coverdyadic} for $(\tilde{\mathcal{D}},c,s)$ by contradiction. Then there is an $I$ violating the conclusion of
Expand All @@ -1521,7 +1509,7 @@ \section{Proof of Grid Existence Lemma}
we have $K\subset J$. By minimality of $s(J)$, we have $I\subset K$.
This proves $I\subset J$ and thus \eqref{dyadicproperty}.

Now note that properties \eqref{dyadicproperty}, \eqref{eq-vol-sp-cube} and \eqref{eq-small-boundary} immediately carry over to $(\mathcal{D},c, s)$ by restriction. \eqref{subsetmaxcube} is true for $(\mathcal{D}, c, s)$ by definition, and \eqref{coverdyadic} follows from \eqref{coverdyadic} and \eqref{dyadicproperty} for $(\tilde{\mathcal{D}}, c, s)$.
Now note that properties \eqref{dyadicproperty}, \eqref{eq-vol-sp-cube} and \eqref{eq-small-boundary} immediately carry over to $(\mathcal{D},c, s)$ by restriction. \eqref{subsetmaxcube} is true for $(\mathcal{D}, c, s)$ by definition, and \eqref{coverdyadic} follows from \eqref{coverdyadic} and \eqref{dyadicproperty} for $(\tilde{\mathcal{D}}, c, s)$.
\end{proof}

\section{Proof of Tile Structure Lemma}
Expand Down Expand Up @@ -2901,11 +2889,7 @@ \section{Proof of the Forest Complement Lemma}
&\quad\cup \bigcup_{k \ge 0} \bigcup_{n \ge k}\bigcup_{0 \le j \le 2n+3} \bigcup_{0 \le l \le Z(n+1)} \fL_3(k,n,j,l)\cap \fP_{G \setminus G'}\,.
\end{align}
\end{lemma}
% fixme(Georges Gonthier): the second sentence of this proof is not technically true

% Or alternatively, redefine \MfP_{X \ G'} to be the p s.t. I(p) \cap (G \ G') has nonzero measure.

% done as suggested in tex, changed \fP_{X \setminus G'} to \fP_{G \setminus G'}.
\begin{proof}
Let $\fp \in \fP_2 \cap \fP_{G \setminus G'}$. Clearly, for every cube $J = \sc(\fp)$ with $\fp \in \fP_{G \setminus G'}$ there exists some $k \ge 0$ such that \eqref{muhj1} holds, and for no cube $J \in \mathcal{D}$ and no $k < 0$ does \eqref{muhj2} hold. Thus $\fp \in \fP(k)$ for some $k \ge 0$.

Expand Down Expand Up @@ -2941,7 +2925,7 @@ \section{Proof of the Forest Complement Lemma}
By assumption \eqref{thirddb} on $\Theta$, this ball can be covered with
$$
2^{a\lceil \log_2(\lambda+1.2) + \log_2(5)\rceil} \le 2^{a(\log_2(\lambda) + 4)} = 2^{4a}\lambda^a
$$
$$
many $d_{\fp'}$-balls of radius $0.2$. Here we have used that for $\lambda \ge 2$
$$
\lceil \log_2(\lambda + 1.2) + \log_2(5) \rceil \le 1+ \log_2(1.6 \lambda) + \log_2(5) = 4 + \log_2(\lambda)\,.
Expand Down Expand Up @@ -3368,7 +3352,7 @@ \section{The density arguments}\label{sec-TT*-T*T}
\end{lemma}

The following lemma will be proved in \Cref{subsec-geolem}.
\begin{lemma}[antichain tile count]
\begin{lemma}[antichain tile count]
\label{antichain-tile-count}
\uses{global-antichain-density}
Set $p:=4a^4$ and let $p'$ be the dual exponent of $p$, that is $1/p+1/p'=1$.
Expand Down
35 changes: 13 additions & 22 deletions lake-manifest.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,28 +4,28 @@
[{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"rev": "af2dda22771c59db026c48ac0aabc73b72b7a4de",
"rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"rev": "44f57616b0d9b8f9e5606f2c58d01df54840eba7",
"rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "f744aab6fc4e06553464e6ae66730a3b14b8e615",
"rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
Expand All @@ -49,7 +49,7 @@
{"url": "https://github.com/leanprover-community/import-graph.git",
"type": "git",
"subDir": null,
"rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
"rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -58,43 +58,34 @@
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"rev": "dd36c71ca810923613cae217af028ee54aaff1e3",
"rev": "7e4afad324f0ef8bd76e01d86296e8663ae8ac1f",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/xubaiw/CMark.lean",
{"url": "https://github.com/acmepjz/md4lean",
"type": "git",
"subDir": null,
"rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
"name": "CMark",
"rev": "9148a0a7506099963925cf239c491fcda5ed0044",
"name": "MD4Lean",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
"type": "git",
"subDir": null,
"rev": "ef8b0ae5d48e7d5f5d538bf8d66f6cdc7daba296",
"rev": "87791b59c53be80a9a000eb2bcbf61f60a27b334",
"name": "UnicodeBasic",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/hargonix/LeanInk",
"type": "git",
"subDir": null,
"rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
"name": "leanInk",
"manifestFile": "lake-manifest.json",
"inputRev": "doc-gen",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/doc-gen4",
"type": "git",
"subDir": null,
"rev": "4e570fed8c4147bdafbd5eada08503ed307252e0",
"rev": "1f51169609a3a7c448558c3d3eb353fb355c7025",
"name": "«doc-gen4»",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.9.0-rc1
leanprover/lean4:v4.9.0-rc3

0 comments on commit da09006

Please sign in to comment.