-
Notifications
You must be signed in to change notification settings - Fork 11
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #245 from trishullab/george
Fix some formalizations, provide few Lean rewrites.
- Loading branch information
Showing
13 changed files
with
65 additions
and
89 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,5 +1,5 @@ | ||
| Require Import Reals Coquelicot.Coquelicot. | ||
| Definition putnam_2022_a1_solution : R -> R -> Prop := (a = 0 /\ b = 0) \/ (Rabs a >= 1) \/ (Rabs a < 1 /\ (b < ln (1 - (1 - sqrt (1 - a ^ 2)) / a) ^ 2 - Rabs a * (1 - (1 - sqrt (1 - a ^ 2)) / a) \/ b > ln (1 - (1 + sqrt (1 - a ^ 2) / a) ^ 2 - Rabs a * (1 + sqrt (1 - a ^ 2) / a)))). | ||
| Definition putnam_2022_a1_solution : R -> R -> Prop := fun a b => (a = 0 /\ b = 0) \/ (Rabs a >= 1) \/ (0 < Rabs a < 1 /\ (b < ln (1 + ((1 - sqrt (1 - a ^2))/ a) ^ 2) - a * (1 - sqrt (1 - a ^ 2) / a) \/ b > ln (1 + ((1 + sqrt (1 - a ^ 2)) / a) ^ 2) - a * (1 + sqrt (1 - a ^ 2) / a))). | ||
| Theorem putnam_2022_a1 | ||
| : forall a b : R, (exists! (x: R), a * x + b = ln (1 + x ^ 2) / ln 10) <-> putnam_2022_a1_solution a b. | ||
| Proof. Admitted. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,22 +1,13 @@ | ||
| import Mathlib | ||
|
|
||
| open Real Equiv | ||
|
|
||
| /-- | ||
| Suppose $f_1(x),f_2(x),\dots,f_n(x)$ are functions of $n$ real variables $x=(x_1,\dots,x_n)$ with continuous second-order partial derivatives everywhere on $\mathbb{R}^n$. Suppose further that there are constants $c_{ij}$ such that $\frac{\partial f_i}{\partial x_j}-\frac{\partial f_j}{\partial x_i}=c_{ij}$ for all $i$ and $j$, $1 \leq i \leq n$, $1 \leq j \leq n$. Prove that there is a function $g(x)$ on $\mathbb{R}^n$ such that $f_i+\partial g/\partial x_i$ is linear for all $i$, $1 \leq i \leq n$. (A linear function is one of the form $a_0+a_1x_1+a_2x_2+\dots+a_nx_n$.) | ||
| -/ | ||
| theorem putnam_1986_a5 | ||
| (n : ℕ) | ||
| (f : Fin n → ((Fin n → ℝ) → ℝ)) | ||
| (xrepl : (Fin n → ℝ) → Fin n → ℝ → (Fin n → ℝ)) | ||
| (contdiffx : ((Fin n → ℝ) → ℝ) → Fin n → (Fin n → ℝ) → Prop) | ||
| (partderiv : ((Fin n → ℝ) → ℝ) → Fin n → ((Fin n → ℝ) → ℝ)) | ||
| (hpartderiv : partderiv = (fun (func : (Fin n → ℝ) → ℝ) (i : Fin n) => (fun x : Fin n → ℝ => deriv (fun xi : ℝ => func (xrepl x i xi)) (x i)))) | ||
| (npos : n ≥ 1) | ||
| (hxrepl : xrepl = (fun (x : Fin n → ℝ) (i : Fin n) (xi : ℝ) => (fun j : Fin n => if j = i then xi else x j))) | ||
| (hcontdiffx : contdiffx = (fun (func : (Fin n → ℝ) → ℝ) (i : Fin n) (x : Fin n → ℝ) => ContDiff ℝ 1 (fun xi : ℝ => func (xrepl x i xi)))) | ||
| (hfcontdiff1 : ∀ i : Fin n, ∀ j : Fin n, ∀ x : Fin n → ℝ, contdiffx (f i) j x) | ||
| (hfcontdiff2 : ∀ i : Fin n, ∀ j1 j2 : Fin n, ∀ x : Fin n → ℝ, contdiffx (partderiv (f i) j1) j2 x) | ||
| (hfc : ∃ c : Fin n → Fin n → ℝ, ∀ i j : Fin n, partderiv (f i) j - partderiv (f j) i = (fun x : Fin n → ℝ => c i j)) | ||
| : ∃ g : (Fin n → ℝ) → ℝ, ∀ i : Fin n, IsLinearMap ℝ (f i + partderiv g i) := | ||
| sorry | ||
| (n : ℕ) (hn : 1 ≤ n) | ||
| (f : Fin n → ((Fin n → ℝ) → ℝ)) | ||
| (hf : ∀ i, ContDiff ℝ 2 (f i)) | ||
| (C : Fin n → Fin n → ℝ) | ||
| (hf' : ∀ i j : Fin n, ∀ x : Fin n → ℝ, fderiv ℝ (f i) x (Pi.single j 1) - fderiv ℝ (f j) x (Pi.single i 1) = C i j) | ||
| : ∃ g : (Fin n → ℝ) → ℝ, ∀ i : Fin n, IsLinearMap ℝ (λ x ↦ f i x + fderiv ℝ g x (Pi.single i 1)) := | ||
| sorry |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,23 +1,22 @@ | ||
| import Mathlib | ||
|
|
||
| open Nat Filter Topology Set | ||
| open Nat Filter Topology Set ProbabilityTheory | ||
|
|
||
| -- Note: uses (ℝ → ℝ) instead of (Set.Icc 0 1 → ℝ) | ||
| /-- | ||
| Let $(x_1,x_2,\dots,x_n)$ be a point chosen at random from the $n$-dimensional region defined by $0<x_1<x_2<\dots<x_n<1$. Let $f$ be a continuous function on $[0,1]$ with $f(1)=0$. Set $x_0=0$ and $x_{n+1}=1$. Show that the expected value of the Riemann sum $\sum_{i=0}^n (x_{i+1}-x_i)f(x_{i+1})$ is $\int_0^1 f(t)P(t)\,dt$, where $P$ is a polynomial of degree $n$, independent of $f$, with $0 \leq P(t) \leq 1$ for $0 \leq t \leq 1$. | ||
| -/ | ||
| theorem putnam_1989_b6 | ||
| (n : ℕ) | ||
| (Sx : Set (Fin n → ℝ)) | ||
| (fprop : (ℝ → ℝ) → Prop) | ||
| (xext : (Fin n → ℝ) → (ℕ → ℝ)) | ||
| (fxsum : (ℝ → ℝ) → (Fin n → ℝ) → ℝ) | ||
| (fEV : (ℝ → ℝ) → ℝ) | ||
| (hSx : Sx = {x : Fin n → ℝ | 0 < x ∧ StrictMono x ∧ x < 1}) | ||
| (hfprop : fprop = (fun f : ℝ → ℝ => ContinuousOn f (Set.Icc 0 1) ∧ f 1 = 0)) | ||
| (hfxsum : fxsum = (fun (f : ℝ → ℝ) (x : Fin n → ℝ) => ∑ i in Finset.Icc 0 n, ((xext x) (i + 1) - (xext x) i) * f ((xext x) (i + 1)))) | ||
| (hfEV : fEV = (fun f : ℝ → ℝ => (∫ x in Sx, fxsum f x) / (∫ x in Sx, 1))) | ||
| (npos : n ≥ 1) | ||
| (hxext : ∀ x : Fin n → ℝ, (xext x) 0 = 0 ∧ (xext x) (n + 1) = 1 ∧ (∀ i : Fin n, (xext x) (i + 1) = x i)) | ||
| : ∃ P : Polynomial ℝ, P.degree = n ∧ (∀ t ∈ Set.Icc 0 1, 0 ≤ P.eval t ∧ P.eval t ≤ 1) ∧ (∀ f : ℝ → ℝ, fprop f → fEV f = (∫ t in Set.Ioo 0 1, f t * P.eval t)) := | ||
| sorry | ||
| (n : ℕ) [NeZero n] | ||
| (I : (Fin n → ℝ) → Fin (n + 2) → ℝ) | ||
| (I_def : ∀ x i, I x i = if i = 0 then 0 else if i = - 1 then 1 else x (i : ℕ).pred) | ||
| (X : Set (Fin n → ℝ)) | ||
| (X_def : ∀ x, x ∈ X ↔ 0 < x 0 ∧ x (-1) < 1 ∧ ∀ i, i + 1 < n → x i < x (i + 1)) | ||
| (S : (ℝ → ℝ) → (Fin (n + 2) → ℝ) → ℝ) | ||
| (S_def : ∀ f x, S f x = ∑ i in Finset.Iic n, (x (i + 1) - x i) * f (i + 1)) : | ||
| ∃ P : Polynomial ℝ, | ||
| P.degree = n ∧ | ||
| (∀ t ∈ Icc 0 1, P.eval t ∈ Icc 0 1) ∧ | ||
| (∀ f : ℝ → ℝ, f 1 = 0 → ContinuousOn f (Icc 0 1) → | ||
| ∫ x, S f (I x) ∂ℙ[|X] = ∫ t in (0)..1, f t * P.eval t) := | ||
| sorry |