Merge pull request #4 from kkytola/main

Blueprint of the playable part so far and some streamlining of the game levels.

Polya/RegularizedOccupation.lean

@@ -1,6 +1,5 @@
 import Mathlib
-import Polya.MiscLemmas -- Someting in the repository setup makes this fail for me...
--- We should fix the setup so that others can have a functioning repository as well.
+import Polya.MiscLemmas
 
 open MeasureTheory Topology Filter
 open ENNReal NNReal
@@ -76,7 +75,7 @@ lemma walkRegularizedOccupation_mono (walk : (t : ℕ) → Grid d) :
   sorry
 
 /-- Regularized occupation of any walk with regularization `r` is at most `(1-r)⁻¹`. -/
-def walkRegularizedOccupation_le (walk : (t : ℕ) → Grid d) (r : ℝ≥0∞) (x : Grid d) :
+lemma walkRegularizedOccupation_le (walk : (t : ℕ) → Grid d) (r : ℝ≥0∞) (x : Grid d) :
     walkRegularizedOccupation walk r x ≤ (1 - r)⁻¹ := by
 -- Remark by Kalle: It is "funny" (and convenient) that here we do not need to assume `r<1`,
 -- which is usually needed for the convergence of the geometric series. That is because in `ℝ≥0∞`
@@ -155,20 +154,26 @@ lemma tsum_indicator_walk_position_eq (X : (t : ℕ) → Ω → Grid d)
     ∑' x, Set.indicator ((X t) ⁻¹' {x}) (fun _ ↦ c) ω = c := by
   apply tsum_indicator_singleton_eq
 
+/-- A walk is always somewhere, so it is easy to calculate the sum over positions
+of the regularized occupations at those positions. -/
+lemma tsum_walkRegularizedOccupation_eq_geom_series (walk : (t : ℕ) → Grid d) (r : ℝ≥0∞) :
+    ∑' x, walkRegularizedOccupation walk r x = ∑' (t : ℕ), r ^ t := by
+-- Instead of literal Fubini's theorem (for counting measures), here it is better to use
+-- the version `ENNReal.tsum_comm`.
+  sorry
+
 /-- A random walk is always somewhere, so it is easy to calculate the sum over positions
 of the regularized occupations at those positions. -/
 lemma tsum_regularizedOccupation_eq_geom_series (X : (t : ℕ) → Ω → Grid d) (r : ℝ≥0∞) :
     ∑' x, regularizedOccupation X r x = fun _ ↦ (∑' (t : ℕ), r ^ t):= by
--- Instead of literal Fubini's theorem (for counting measures), here it is better to use
--- the version `ENNReal.tsum_comm`.
   sorry
 
 /-- A walk is always somewhere, so it is easy to calculate the sum over positions
 of the regularized occupations at those positions. -/
 lemma tsum_toReal_walkRegularizedOccupation_eq_geom_series (walk : (t : ℕ) → Grid d)
     {r : ℝ≥0} (r_lt_one : r < 1) :
     ∑' x, (walkRegularizedOccupation walk r x).toReal = (∑' (t : ℕ), r.toReal ^ t):= by
--- To get to use the standard Fubili's theorem `lintegral_lintegral_swap`, one can first
+-- To get to use the standard Fubini's theorem `lintegral_lintegral_swap`, one can first
 -- rewrite the sums as integrals (w.r.t. counting measures) with `lintegral_count`.
   sorry
 
@@ -180,6 +185,15 @@ lemma tsum_toReal_regularizedOccupation_eq_geom_series (X : (t : ℕ) → Ω →
 -- This is easy with the previous one!
   sorry
 
+/-- A random walk is always somewhere, so it is easy to calculate the sum over positions
+of the regularized occupations at those positions. When `r < 1`, the infinite sums are
+convergent and the calculation yields an equality in `ℝ`. -/
+lemma tsum_toReal_regularizedOccupation_eq (X : (t : ℕ) → Ω → Grid d)
+    {r : ℝ≥0} (r_lt_one : r < 1) (ω : Ω) :
+    ∑' x, (regularizedOccupation X r x ω).toReal = (1 - r)⁻¹ := by
+-- This is the previous one conbined with a convergent geometric series.
+  sorry
+
 /-- The sum over points of the expected value of the regularized occupation is a
 geometric series with the ratio given by the regularization. -/
 lemma tsum_lintegral_norm_regularizedOccupation_eq_geom_series
@@ -219,7 +233,7 @@ def regularizedG (X : (t : ℕ) → Ω → Grid d) (r : ℝ≥0∞) (x : Grid d)
 
 /-- An auxiliary step: one can interchange a sum and expected value for `regularizedG` summed over
 all grid points. -/
-lemma tsum_regularizedG_eq_tsum'' {X : (t : ℕ) → Ω → Grid d}
+lemma tsum_regularizedG_eq_lintegral_tsum {X : (t : ℕ) → Ω → Grid d}
     {r : ℝ≥0} (r_lt_one : r < 1) (X_mble : ∀ t, Measurable (X t)) :
     ∑' x, regularizedG P X r x
       = (∫ ω, ∑' x, ∑' t,
@@ -248,16 +262,6 @@ lemma summable_regularized_occupation {walk : (t : ℕ) → Grid d} {r : ℝ≥0
 -- The idea is to get this from the slightly generalized version `summable_weighted_occupation`.
   sorry
 
-/-- A further auxiliary step: one can interchange two sums and an expected value for
-`regularizedG` summed over all grid points. -/
-lemma tsum_regularizedG_eq_tsum''' {X : (t : ℕ) → Ω → Grid d}
-    {r : ℝ≥0} (r_lt_one : r < 1) (X_mble : ∀ t, Measurable (X t)) :
-    ∑' x, regularizedG P X r x
-      = (∫ ω, ∑' t, ∑' x, Set.indicator ((X t) ⁻¹' {x}) (fun _ ↦ (r : ℝ) ^ t) ω ∂P) := by
--- For this one, `tsum_comm` looks like the best version of Fubini's theorem, once one
--- has applied the earlier auxiliary `tsum_regularizedG_eq_tsum''`.
-  sorry
-
 lemma tsum_regularizedG_eq {X : (t : ℕ) → Ω → Grid d}
     {r : ℝ≥0} (r_lt_one : r < 1) (X_mble : ∀ t, Measurable (X t)) :
     ∑' x, regularizedG P X r x = (1 - r)⁻¹ := by

blueprint/src/content.tex

@@ -6,13 +6,21 @@
 % the current file can be a simple sequence of \input. Otherwise It
 % can start with a \section or \chapter for instance.
 
-\newtheorem{theorem}{Theorem}
+%\newtheorem{theorem}{Theorem}
 
-\begin{theorem}
-  \label{tt:test}
-  Test
-\end{theorem}
+\input{occupation.tex}
 
-\begin{proof}
-test
-\end{proof}
+% \begin{definition}
+%   \label{def:deftest}
+%   \lean{deftest}
+%   Test
+% \end{definition}
+% 
+% \begin{theorem}
+%   \label{thm:test}
+%   \lean{test}
+%   Test
+% \end{theorem}
+% \begin{proof}
+% test
+% \end{proof}

blueprint/src/macros/common.tex

@@ -1,3 +1,22 @@
 % In this file you should put all LaTeX macros to be used
 % both by the pdf version and the web version.
-% This should be most of your macros.
+% This should be most of your macros.
+\newcommand{\set}[1]{\left\{ #1 \right\}}
+
+\newcommand{\bN}{\mathbb{N}}
+\newcommand{\bZ}{\mathbb{Z}}
+\newcommand{\bQ}{\mathbb{Q}}
+\newcommand{\bR}{\mathbb{R}}
+\newcommand{\bC}{\mathbb{C}}
+
+\newcommand{\EX}{\mathsf{E}}
+\newcommand{\PR}{\mathsf{P}}
+
+\newcommand{\ind}{\mathsf{1}}
+\newcommand{\indOf}[1]{\ind_{#1}}
+
+\newcommand{\G}{\mathrm{G}}
+\newcommand{\Greg}[1]{\G_{#1}}
+
+\newcommand{\walk}{\mathfrak{w}}
+\newcommand{\RW}{X}

blueprint/src/macros/print.tex

@@ -26,4 +26,17 @@
 \NewDocumentCommand{\proves}{m}
  {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
   \ignorespaces}
-\ExplSyntaxOff
+\ExplSyntaxOff
+
+\newtheorem{theorem}{Theorem}[chapter]
+%\newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{lemma}[theorem]{Lemma}
+%\newtheorem{sublemma}[theorem]{Sub-lemma}
+\newtheorem{corollary}[theorem]{Corollary}
+
+\theoremstyle{definition}
+\newtheorem{definition}[theorem]{Definition}
+
+\theoremstyle{remark}
+\newtheorem{remark}[theorem]{Remark}
+\newtheorem{example}[theorem]{Example}

blueprint/src/macros/web.tex

@@ -2,4 +2,17 @@
 % the web version. Of course they should have a corresponding
 % version in macros/print.tex.
 % Typically the printed version could have more fancy decorations.
-% This will probably be a very short file.
+% This will probably be a very short file.
+
+\newtheorem{theorem}{Theorem}[chapter]
+%\newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{lemma}[theorem]{Lemma}
+%\newtheorem{sublemma}[theorem]{Sub-lemma}
+\newtheorem{corollary}[theorem]{Corollary}
+
+\theoremstyle{definition}
+\newtheorem{definition}[theorem]{Definition}
+
+\theoremstyle{remark}
+\newtheorem{remark}[theorem]{Remark}
+\newtheorem{example}[theorem]{Example}