diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..645bbce --- /dev/null +++ b/.gitattributes @@ -0,0 +1,2 @@ +# Preserve captured verification logs verbatim, including trailing blank lines. +research/**/*.log -whitespace diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 0980c52..ac9fcbb 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -20,6 +20,6 @@ jobs: # The repository's trust policy, enforced: no `sorry` outside the two # deliberate holes in Challenge.lean, no project-defined axiom, no # native_decide, no unsafe, no floating point, and the top-level results - # depending on the three standard axioms only. See docs/design.md §8. + # depending on the three standard axioms only. See docs/design.md. - name: Trust audit run: bash scripts/audit.sh diff --git a/.gitignore b/.gitignore index bfb30ec..605e5af 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,9 @@ -/.lake +# Build outputs and local dependency environments (including research stages). +.lake/ +.venv/ +__pycache__/ +.pytest_cache/ +.mypy_cache/ +.ruff_cache/ +*.pyc +*.pyo diff --git a/README.md b/README.md index 8734228..d7d4cdd 100644 --- a/README.md +++ b/README.md @@ -1,280 +1,100 @@ # Sendov's conjecture in Lean -A formalization of **Sendov's conjecture** and the **Phelps–Rodriguez conjecture**, in full -generality. - -```lean -/-- Sendov's conjecture. -/ -theorem Sendov.sendov {n : ℕ} (hn : 2 ≤ n) {p : ℂ[X]} (hdeg : p.natDegree = n) - (hroots : ∀ w ∈ p.roots, ‖w‖ ≤ 1) {a : ℂ} (hpa : p.eval a = 0) : - ∃ ζ : ℂ, (derivative p).eval ζ = 0 ∧ ‖ζ - a‖ ≤ 1 - -/-- The Phelps–Rodriguez conjecture. -/ -theorem Sendov.phelps_rodriguez {n : ℕ} (hn : 2 ≤ n) {p : ℂ[X]} (hdeg : p.natDegree = n) - (hroots : ∀ w ∈ p.roots, ‖w‖ ≤ 1) {a : ℂ} (hpa : p.eval a = 0) : - (∃ ζ : ℂ, (derivative p).eval ζ = 0 ∧ ‖ζ - a‖ < 1) - ∨ (‖a‖ = 1 ∧ ∃ c : ℂ, c ≠ 0 ∧ p = C c * (X ^ n - C (a ^ n))) -``` - -If every zero of a complex polynomial of degree `n ≥ 2` lies in the closed unit disk, then -every zero `a` has a critical point within distance `1` — and within distance *strictly* less -than `1`, unless `a` is on the unit circle and `p` is a scalar multiple of `zⁿ - aⁿ`. - -The informal proof being formalized is -[*A digestion of the proof of Sendov's conjecture*](https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/). - -Both are in [`Sendov/Conjecture.lean`](Sendov/Conjecture.lean#L83), and both depend on -`propext`, `Classical.choice` and `Quot.sound` only. - -[`Challenge.lean`](Challenge.lean) is the statement of record: 87 lines, importing only -Mathlib, declaring no definitions of its own. A reader who wants to check *what* has been -proved should read that file and need not read anything else. - -## Roadmap - -The proof is by contradiction throughout. Suppose `p` has degree `n ≥ 2`, all zeroes in the -closed unit disk, `p(a) = 0`, and *no* critical point within distance `1` of `a`. - -### 0. Normalize, and split into two multisets - -A rotation `p(ωz)` moves `a` to the real point `‖a‖`, so `a` may be assumed real and in -`[0,1]` — [`Sendov.rotate`](Sendov/Conjecture.lean#L43). The counterexample is then -repackaged as two multisets of `n-1` points of the closed unit disk: - -| | | -|---|---| -| the other zeroes `zⱼ` | [`exists_root_multiset`](Sendov/Counterexample/Factor.lean#L46) | -| the critical points, as `qⱼ = 1/(a - wⱼ)` | [`exists_crit_multiset`](Sendov/Counterexample/Factor.lean#L74) | - -The hypothesis "no critical point within distance 1" is exactly `‖qⱼ‖ ≤ 1`. - -### 1. Four identities linking zeroes to critical points - -All in [`Sendov/Counterexample/Identities.lean`](Sendov/Counterexample/Identities.lean), all -division-free, so that no `p'(a) ≠ 0` side condition is ever needed: - -| identity | meaning | | -|---|---|---| -| [`centroid_identity`](Sendov/Counterexample/Identities.lean#L60) | centroid of zeroes = centroid of critical points | | -| [`prod_sub_mul_prod`](Sendov/Counterexample/Identities.lean#L322) | `p'(a)` two ways: `(∏qⱼ)(∏(a-zⱼ)) = n` | | -| [`polar_identity`](Sendov/Counterexample/Identities.lean#L355) | `∏(1-azⱼ)/(a-zⱼ)` as an integral | | -| [`first_origin_identity`](Sendov/Counterexample/Identities.lean#L241) | `∫₀¹F` in terms of `∏zⱼ` | `F(t) = ∏(1 - a t qⱼ)` | -| [`second_origin_identity`](Sendov/Counterexample/Identities.lean#L165) | `F(1)` in terms of `∏zⱼ` and `∑1/zⱼ` | | - -### 2. The branch point `(⋆)` - -The polar identity together with `p'(a)` two ways gives - -> [`one_le_integral_prod_norm`](Sendov/Analytic/Polar.lean#L115) : `1 ≤ ∫₀¹ ∏ⱼ ‖a + t(1-a²)qⱼ‖ dt` - -This is where the argument forks. The Möbius estimate `|1-az|/|a-z| ≥ 1` is the one step that -needs `a` real. - -### 3a. Low degrees, `2 ≤ n ≤ 4` - -Bounding each factor of `(⋆)` by the *scalar* `X(t) = a + (1-a²)t` already contradicts itself: -`1 ≤ Jₘ(a) = ∫₀¹X(t)ᵐ dt` with `m = n-1`, while `Jₘ(a) < 1` for `0 < a < 1` and `m ≤ 4`. The -computation is done once, at `m = 4`, where `1 - J₄(a) = ((1-a)³(1+a)/5)(a⁴-3a³+3a+4)`. - -> [`low_degree_contradiction`](Sendov/Analytic/LowDegree.lean#L210), from -> [`one_le_lowJ`](Sendov/Analytic/LowDegree.lean#L93) and -> [`lowJ_lt_one`](Sendov/Analytic/LowDegree.lean#L185) - -No origin channel, no `Real.rpow`, no certificates. - -The lemma is stated for `2 ≤ n ≤ 5`, but this is the only branch that needs no certificate, -and the recorded proof enters it only for `n ≤ 4`: [`sendov_interior`](Sendov/Interior.lean#L53) -splits at `n < 5`, so degree `5` goes through the two-channel branch below like every larger -degree. - -### 3b. High degrees, `n ≥ 5`: two channels that cannot both hold - -Write `x + iy = (∑ⱼqⱼ)/(n-1)` and `α = (n-1)(1-a²)/2`. - -**The polar channel.** AM–GM relaxes `(⋆)` to a scalar inequality in `x` alone: - -> [`one_le_integral_Ppolar`](Sendov/Analytic/Polar.lean#L274) — the raw polar inequality `(1Q)` - -**The origin channel.** Differentiating `F(t) = ∏ⱼ(1 - a t qⱼ)` and integrating against the -fundamental theorem of calculus: - -| step | | +This local development proves **Sendov's conjecture** and the full +**Phelps–Rodriguez equality classification**. The statements of record are +`SendovConjecture.sendov` and `SendovConjecture.phelps_rodriguez` in +[`Solution.lean`](Solution.lean), with the original specifications retained in +[`Challenge.lean`](Challenge.lean). The latter contains the original two +statement placeholders and is not imported by the proof. + +For every complex polynomial of degree at least two whose zeros lie in the +closed unit disk, every zero has a critical point at distance at most one. +The distance is strictly less than one unless the distinguished zero lies on +the unit circle and the polynomial has the stated nonzero scalar-multiple +form. There is no extra numerical, genericity, degree-bound, or simple-root +hypothesis in either final theorem. + +## One active proof route + +The polynomial identities, analytic reduction, low-degree argument and boundary +classification start from Terence Tao's formalization.[1] The scalar endgame +uses Senjian An's rational envelope and two-chord estimate, followed by +full-degree-ray alpha estimates proved in Lean, not trusted Python checks.[2] + +| Part | Active source | |---|---| -| `∑ⱼ∏_{k≠j}‖1-atq_k‖ ≤ (n-1)β(t)^{(n-2)/2}` | [`sumEraseProdMap_norm_le`](Sendov/Analytic/Origin.lean#L158) | -| `‖F'(t) + (n-1)a(x+iy)F(t)‖ ≤ …` | [`norm_deriv_add_le`](Sendov/Analytic/Origin.lean#L329) | -| integrate, using `F(0) = 1` | [`one_le_tri`](Sendov/Analytic/Origin.lean#L388) | -| estimate `J∑1/zⱼ`, paying the defect `1-\|J\|²` | [`Jsum_estimate`](Sendov/Analytic/Jsum.lean#L122) | -| `‖W‖ ≥ 2an/(n-1)`, collapsing `\|J\|` to `1` | [`grow`](Sendov/Analytic/OriginExact.lean#L92) | -| | [`origin_exact`](Sendov/Analytic/OriginExact.lean#L179) | - -`grow` reduces to `(n-1)²a² - (3n-1)a + (n-1) > 0`, whose discriminant `(3n-1)² - 4(n-1)³` is -negative exactly from `n ≥ 5`. **This is the only place `n ≥ 5` is used.** - -**The contradiction.** The two inequalities force `α ≤ 17` and then contradict each other: - -> [`polar_origin_incompatible`](Sendov/Reduction/Main.lean#L60) - -by way of the chain `(1Q) ⟹ (lt)` ([`polar_exp`](Sendov/Reduction/Polar.lean#L74)), -`(lt) ⟹ (beta-bound)` ([`beta_le`](Sendov/Reduction/BetaBound.lean#L108)), -[`alpha_le_seventeen`](Sendov/Reduction/Alpha17.lean#L106), and a numerical claim `stat`: - -> [`stat_lt_one`](Sendov/Main.lean#L40), from -> [`finite_range_le_100`](Sendov/FiniteRange/Cover.lean#L58) (degrees 5–100, by per-degree -> Bernstein certificates) and [`large_degree`](Sendov/LargeDegree/Endgame.lean#L251) -> (degrees ≥ 101, by an analytic reduction that removes the degree, then the single -> Bernstein certificate [`F_pos`](Sendov/LargeDegree/Endgame.lean#L53) for what it leaves) - -See [`docs/finite-range.md`](docs/finite-range.md) for that component on its own. - -### 3c. The boundary, `‖a‖ = 1` - -The polar identity degenerates at the boundary — the reflected point `1/a` coincides with `a` -and `1-a² = 0` — so it is replaced by one identity from `p''(1)/p'(1)`: - -> `∑ⱼqⱼ = 2∑ⱼ1/(1-zⱼ)` — [`boundary_reciprocal`](Sendov/Boundary.lean#L151) - -Both sides are then pinned: `Re qⱼ ≤ ‖qⱼ‖ ≤ 1` caps the left at `n-1`, while -`Re 1/(1-z) - 1/2 = (1-‖z‖²)/(2‖1-z‖²) ≥ 0` floors the right at `n-1`. Equality term by term -forces `qⱼ = 1`, so every critical point is `0` and `p = c(zⁿ-1)`. - -> [`all_q_eq_one`](Sendov/Boundary.lean#L168) → [`rubinstein_one`](Sendov/Boundary.lean#L210) - -The boundary case is Rubinstein's theorem, and it is where the Phelps–Rodriguez equality case -comes from. The argument is **not new**: the identity and the half-plane bound above are -equation (5.1) and Remark 5.1 of [Tang and Zhang](https://arxiv.org/abs/2508.10341), where the -same two steps give the `a = 1` case of Sendov's conjecture. What is done here in addition is -to run the sandwich to equality, recovering the classification — which is Rubinstein's 1968 -theorem, and so not new either. See [Provenance](#provenance-and-novelty). - -### 3d. The centre, `a = 0` - -`p'(a)` two ways is already enough: `(∏qⱼ)(∏zⱼ) = n` with both factors of norm at most one -forces `n ≤ 1`. - -> [`sendov_center`](Sendov/Interior.lean#L125) - -### 4. Assembling - -> [`sendov_interior`](Sendov/Interior.lean#L53) (real `0 < a < 1`) → -> [`sendov_interior_real`](Sendov/Interior.lean#L162) (with `a = 0`) → -> [`phelps_rodriguez`](Sendov/Conjecture.lean#L83) (rotation, and the boundary) → -> [`sendov`](Sendov/Conjecture.lean#L158) - -## Two ingredients absent from Mathlib - -* **Maclaurin's inequality**, top case — [`Multiset.esymm_card_pred_le`](Sendov/Analytic/Maclaurin.lean#L166), - by multiset induction reducing to Bernoulli. The same induction gives multiset AM–GM, - [`Multiset.prod_le_mean_pow`](Sendov/Analytic/Maclaurin.lean#L107). -* **The defect lemma** — [`defect`](Sendov/Analytic/Defect.lean#L93): - `∏|wⱼ| · ∑ⱼ|1/wⱼ - conj wⱼ| ≤ 1 - ∏|wⱼ|²` on the closed unit disk. - -A third piece worth naming is [`log_sinh_div_le`](Sendov/Common/Sinh.lean#L245), -`log(sinh h / h) ≤ √(h²+9) - 3`, which is sharp to three orders at `h = 0` and is the crux of -the `(beta-bound)` step. - -## Trust - -* no `sorry` and no project-defined `axiom`, with one deliberate exception: `Challenge.lean` - *states* the two theorems without proving them, which is what makes it the statement of - record for Comparator to check `Solution.lean` against. `scripts/audit.sh` requires exactly - those two holes and no others, and forbids `sorry` everywhere else including `Solution.lean`; -* no `native_decide`, no `unsafe`, no floating point in any statement or proof; -* `maxHeartbeats` / `maxRecDepth` appear only as deliberate resource knobs, each with an - explanatory comment. - -`scripts/audit.sh` checks all of this and prints the axiom dependencies of the top-level -results; `scripts/mutation_test.sh` checks that the numerical certificates are actually -load-bearing. - -## Building - -``` +| Final statements and rotation | [`Solution.lean`](Solution.lean), [`Conjecture`](Sendov/Conjecture.lean) | +| Unit-circle boundary and equality case | [`Boundary`](Sendov/Boundary.lean) | +| Interior degrees `2 ≤ n ≤ 5` | [`LowDegree`](Sendov/Analytic/LowDegree.lean), [`Interior`](Sendov/Interior.lean) | +| Original polar/origin hypotheses → scalar domain and lower bound | [`CubicScalar`](Sendov/Reduction/CubicScalar.lean) | +| Strong hyperbolic bound and cubic polar envelope | [`DistillationHyperbolic`](Sendov/Common/DistillationHyperbolic.lean), [`CubicPolar`](Sendov/Reduction/CubicPolar.lean) | +| Two-chord integral estimate and regularized factors | [`TwoChord`](Sendov/Common/TwoChord.lean), [`DistillationFactors`](Sendov/Common/DistillationFactors.lean) | +| Small alpha, `0 < alpha <= 7/5` | [`DistillationTotalBound`](Sendov/Common/DistillationTotalBound.lean) | +| Middle alpha, `7/5 <= alpha <= 2` | [`DistillationMiddleAlpha`](Sendov/Common/DistillationMiddleAlpha.lean) | +| Large alpha, `2 <= alpha <= 17` | [`DistillationPeakClosure`](Sendov/Common/DistillationPeakClosure.lean) | +| Complete contradiction | [`DistillationBounds`](Sendov/Common/DistillationBounds.lean), [`Reduction/Main`](Sendov/Reduction/Main.lean) | + +The convention is **`m = n - 1`**. `distillScalar_lt_one_real` proves the +original raw scalar bound `<1` for **every real `m >= 5`, +`0 < alpha <= 17`, `2*alpha <= m`**, including noninteger degrees and the +legal `m=2*alpha` endpoint. The natural `n >= 6` wrapper has its original type. +There is no finite-degree certificate, numerical degree base, interval patch +or later tail cutoff. No claim is made that 5 is globally minimal. + +The three alpha regimes are mathematical estimates on entire degree rays. +Large alpha uses three complete polynomial identities of degrees **53, 47, 47**, +with 150 ordered coefficients and 71 low-degree homogeneous factor coefficients. +All scales, factors and identities are checked by Lean's kernel. These are +fixed alpha certificates, not degree rows; their full source and data cost is +included in the implementation, not hidden behind three theorem names. +The raw value at `alpha=0` remains `1/(2*m)`, separately from regularization. + +The old `R`-based finite/large-degree certificate system and its specialized +generators are retired, not shipped as a second compatibility route. General +lemmas still used by the new proof remain. The mean/variance budget formulation +also incorporates an idea examined in Pickhardt's work; no conditional Sendov +claim or assumed threshold from that project is used.[3] + +## Build and verify + +Use the versions pinned by [`lean-toolchain`](lean-toolchain) and +[`lake-manifest.json`](lake-manifest.json): + +```sh lake exe cache get lake build -bash scripts/audit.sh +lake env lean scripts/axioms.lean ``` -Memory, not time, is the binding constraint on a full build; `scripts/staged_build.sh` builds -the certificate files in batches. - -## Documents - -| | | -|---|---| -| [`docs/making-of.md`](docs/making-of.md) | how this formalization happened: a curated transcript of the conversation that produced it | -| [`docs/getting-started.md`](docs/getting-started.md) | how to set up to do something like this, for someone new to Lean, VS Code, GitHub or coding agents | -| [`docs/design.md`](docs/design.md) | design record: status table, the measurements behind each decision, and the traps encountered | -| [`docs/finite-range.md`](docs/finite-range.md) | the finite-range check on its own | -| [`docs/proof-large-degree.md`](docs/proof-large-degree.md) | informal proof for degrees ≥ 101 | -| [`docs/plan-*.md`](docs/) | the staged hand-off plans, with notes on where they were superseded | -| [the blog post](https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/) | the informal proof being formalized | - -## Provenance and novelty - -**No novelty is claimed anywhere in this repository, and no literature or formalization search -was performed.** Where this document notes that something here differs from earlier work, that -is a description of this development, not a priority claim: whether any of it is new is -unknown. - -The mathematics descends from **Lech Mazur's** proof. Sendov's conjecture was first proved, and -first formalized in Lean, by that work at [ProofAtlas](https://www.proofatlas.ai/formalizations/sendov-conjecture/) — priority for both belongs there. -The informal proof formalized here is [Tao's digestion](https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/) of Mazur's argument, described in -the post as an effort "to place the proof in proper context with previous literature and to -simplify and streamline the argument to highlight the main ideas". This repository is therefore -the **second** formalization of Sendov's conjecture, and its mathematical content is a -streamlined descendant of the first rather than an independent route to the same theorem. - -As far as we are aware it is the first formalization of the **Phelps–Rodriguez** form: the -earlier formalization reports a single main theorem, Sendov's `‖ζ - a‖ ≤ 1`, and does not state -the equality classification. That is an observation about the one earlier formalization we know -of, not the result of a search. - -The two developments are separately checkable evidence for the same theorem, and they differ in -what they state and in size: - -| | this repository | the earlier formalization | -|---|---|---| -| statement | Sendov **and** Phelps–Rodriguez | Sendov | -| Lean | 80 files, 15,152 lines | 1,160 files, 92,816 lines *(as reported there)* | -| shared code | none | | - -The boundary argument in [`Sendov/Boundary.lean`](Sendov/Boundary.lean) is likewise not new. -It was reached here from the blog post rather than from the literature, but its two ingredients -are equation (5.1) and Remark 5.1 of Quanyu Tang and Teng Zhang, *Sharp Schoenberg type -inequalities and the de Bruin–Sharma problem*, [arXiv:2508.10341](https://arxiv.org/abs/2508.10341): -their `∑ₖ 1/wₖ = 2 ∑ⱼ 1/zⱼ` is `boundary_reciprocal` after moving the distinguished zero from -`0` to `1`, and their `ℜ(1/zⱼ) ≤ -1/2` is `half_le_re_inv_one_sub`. Remark 5.1 stops at the -non-strict conclusion `min|wₖ| ≤ 1`; the extra step here, extracting equality term by term to -get the classification, recovers Rubinstein's 1968 theorem and is not claimed as new either. - -One difference is worth naming because it is checkable here: this development uses **no -interval arithmetic and no floating point at all**. The computational step — a numerical -inequality reached by every degree from `5` up, in both the finite range and, after the -analytic reduction, the large-degree endgame — is discharged by exact rational Bernstein -certificates re-verified inside Lean, and `scripts/audit.sh` fails the build if `Float` -appears anywhere in a statement or proof. No comparison of the two proofs' internal arguments has been carried out. - -## How this was produced - -Essentially all of the Lean source in this repository was written by **Claude Opus 5** -(Anthropic), working interactively in Claude Code under the direction and review of the -author: choosing the Lean formulations, finding and repairing proofs, and designing the -certificate machinery. The author set the targets, supplied the informal proof and the staged -plans in `docs/`, made the mathematical decisions, and reviewed the output as it was produced. -No external or independent review has been performed. - -The Bernstein certificates are emitted by the Python scripts in `scripts/`: the per-degree -ones in `Sendov/FiniteRange/`, and the degree-58 endgame certificate `F_pos` in -`Sendov/LargeDegree/Endgame.lean`, from `scripts/gen_endgame.py`. Those scripts are outside the trusted base: they write Lean source that Lean -re-verifies from scratch, so a bug in them causes a build failure, not an unsound theorem. - -Two documents record the process rather than the result. -[`docs/making-of.md`](docs/making-of.md) is a curated transcript of the conversation that -produced the development — the stages it went through, and the dead ends and mistakes along -the way. [`docs/getting-started.md`](docs/getting-started.md) describes the setup this -repository started from and the working habits that mattered, for someone new to Lean, VS Code, -GitHub or coding agents. - -## Licence - -Apache-2.0; see [`LICENSE`](LICENSE). +The mathematical proof uses only `propext`, `Classical.choice`, and `Quot.sound`. +No project axiom, `sorry`, `native_decide`, or floating-point computation is used +in the proved library. Kernel replay, original headline-type comparison and +actual proof-dependency checks are separate acceptance steps; compilation alone +is not reported as all of them. + +See [`docs/getting-started.md`](docs/getting-started.md) for verification and +[`scripts/GENERATORS.md`](scripts/GENERATORS.md) for reproducible generation. +The alpha identities are self-contained Lean source and need no generator. +The existing global `sinh` generator remains reproducible. A successful +generator run is **not** a completed proof check. + +## Provenance and scope + +This is a local adaptation, not a claim that upstream maintainers reviewed or +endorsed these changes. The repository keeps the original Apache-2.0 code +license. The retained distilled mathematics is attributed to +Senjian An's fixed source version; the source paper is CC BY 4.0.[2] +The retained generator entry points incorporate applicable portability fixes; +obsolete batch-specific tools are not retained merely to preserve a PR surface.[4] +Only contributions serving the active proof and its reproducibility are kept. +Unverified theorem corpora, numerical demonstrations, unrelated visualization +programs and obsolete generator interfaces are not part of the proof deliverable. + +See [`docs/design.md`](docs/design.md) for the reduction contract and trust boundary. + +## Sources + +[1] https://github.com/teorth/sendov +[2] https://github.com/SJanPerth/Sendov-Proof-Distillation/tree/e8ae601491ec171ab4f7f8456113dd6a047aa85d +[3] https://github.com/pickhardt/sendov-explicit-threshold +[4] https://github.com/teorth/sendov/pull/1 diff --git a/Sendov.lean b/Sendov.lean index 2f6e5d8..23d37c0 100644 --- a/Sendov.lean +++ b/Sendov.lean @@ -1,75 +1,2 @@ -import Sendov.Common.Basic -import Sendov.Common.Rpow -import Sendov.Common.Quadratic -import Sendov.Common.Chord -import Sendov.FiniteRange.Batch -import Sendov.FiniteRange.Moments -import Sendov.FiniteRange.OddBound -import Sendov.FiniteRange.Pack -import Sendov.FiniteRange.Recurrence -import Sendov.FiniteRange.PackBridge -import Sendov.FiniteRange.Reduce -import Sendov.FiniteRange.Degree5 -import Sendov.FiniteRange.Degree6 -import Sendov.FiniteRange.Degree7 -import Sendov.FiniteRange.Degree8 -import Sendov.FiniteRange.Degree20 -import Sendov.FiniteRange.Degree20Packed -import Sendov.FiniteRange.Degree53Packed -import Sendov.FiniteRange.Degree97Packed -import Sendov.FiniteRange.Degree6_6 -import Sendov.FiniteRange.Degree8_9 -import Sendov.FiniteRange.Degree10_11 -import Sendov.FiniteRange.Degree12_13 -import Sendov.FiniteRange.Degree14_15 -import Sendov.FiniteRange.Degree16_18 -import Sendov.FiniteRange.Degree18_20 -import Sendov.FiniteRange.Degree20_22 -import Sendov.FiniteRange.Degree22_24 -import Sendov.FiniteRange.Degree24_26 -import Sendov.FiniteRange.Degree26_27 -import Sendov.FiniteRange.Degree28_29 -import Sendov.FiniteRange.Degree30_31 -import Sendov.FiniteRange.Degree32_33 -import Sendov.FiniteRange.Degree34_35 -import Sendov.FiniteRange.Degree36_37 -import Sendov.FiniteRange.Degree38_39 -import Sendov.FiniteRange.Degree40_41 -import Sendov.FiniteRange.Degree42_43 -import Sendov.FiniteRange.Degree44_45 -import Sendov.FiniteRange.Degree46_47 -import Sendov.FiniteRange.Degree48_49 -import Sendov.FiniteRange.Degree50_51 -import Sendov.FiniteRange.Degree52_53 -import Sendov.FiniteRange.Degree54_55 -import Sendov.FiniteRange.Degree56_58 -import Sendov.FiniteRange.Degree58_60 -import Sendov.FiniteRange.Degree60_63 -import Sendov.FiniteRange.Degree64_69 -import Sendov.FiniteRange.Degree70_79 -import Sendov.FiniteRange.Degree80_100 -import Sendov.LargeDegree.Tail -import Sendov.FiniteRange.Cover -import Sendov.LargeDegree.Monotone -import Sendov.LargeDegree.Endgame -import Sendov.Main -import Sendov.Common.Sinh -import Sendov.Reduction.Setup -import Sendov.Reduction.Polar -import Sendov.Reduction.BetaBound -import Sendov.Reduction.Stat -import Sendov.Reduction.Simplified -import Sendov.Reduction.Alpha17 -import Sendov.Reduction.Main -import Sendov.Analytic.Maclaurin -import Sendov.Analytic.Defect -import Sendov.Counterexample.Factor -import Sendov.Counterexample.Identities -import Sendov.Analytic.Polar -import Sendov.Analytic.Origin -import Sendov.Analytic.Jsum -import Sendov.Analytic.OriginExact -import Sendov.Analytic.LowDegree -import Sendov.Interior -import Sendov.Boundary import Sendov.Conjecture +import Sendov.Collinear.Moment diff --git a/Sendov/Analytic/Defect.lean b/Sendov/Analytic/Defect.lean index 28be48b..c4a0c9b 100644 --- a/Sendov/Analytic/Defect.lean +++ b/Sendov/Analytic/Defect.lean @@ -47,24 +47,14 @@ open Multiset /-! ### Products of norms -/ lemma prod_norm_nonneg (s : Multiset ℂ) : 0 ≤ (s.map (fun z => ‖z‖)).prod := by - refine Multiset.prod_nonneg ?_ - intro y hy - obtain ⟨z, _, rfl⟩ := Multiset.mem_map.1 hy - exact norm_nonneg z + exact Multiset.prod_map_nonneg (fun z _ => norm_nonneg z) lemma prod_norm_le_one : ∀ (s : Multiset ℂ), (∀ z ∈ s, ‖z‖ ≤ 1) → (s.map (fun z => ‖z‖)).prod ≤ 1 := by - intro s - induction s using Multiset.induction_on with - | empty => intro _; simp - | cons w t ih => - intro hs - have hw : ‖w‖ ≤ 1 := hs w (mem_cons_self w t) - have ht : ∀ z ∈ t, ‖z‖ ≤ 1 := fun z hz => hs z (mem_cons_of_mem hz) - have hIH := ih ht - have hP0 : 0 ≤ (t.map (fun z => ‖z‖)).prod := prod_norm_nonneg t - simp only [Multiset.map_cons, Multiset.prod_cons] - nlinarith [norm_nonneg w] + intro s hs + simpa [normHom] using + (Multiset.prod_map_le_pow_card (f := (normHom : ℂ →*₀ ℝ)) + (fun z _ => norm_nonneg z) hs) /-! ### The pointwise fact -/ @@ -74,18 +64,12 @@ lemma norm_mul_norm_inv_sub_conj_le {w : ℂ} (hw : ‖w‖ ≤ 1) : ‖w‖ * ‖w⁻¹ - (starRingEnd ℂ) w‖ ≤ 1 - ‖w‖ ^ 2 := by rcases eq_or_ne w 0 with rfl | hne · simp - · have hkey : w * (w⁻¹ - (starRingEnd ℂ) w) = 1 - ((‖w‖ : ℝ) : ℂ) ^ 2 := by - rw [mul_sub, mul_inv_cancel₀ hne, Complex.mul_conj] - norm_cast - rw [Complex.normSq_eq_norm_sq] - have h1 : ‖w‖ * ‖w⁻¹ - (starRingEnd ℂ) w‖ = ‖(1 : ℂ) - ((‖w‖ : ℝ) : ℂ) ^ 2‖ := by - rw [← norm_mul, hkey] - rw [h1] - have h2 : ((1 : ℂ) - ((‖w‖ : ℝ) : ℂ) ^ 2) = ((1 - ‖w‖ ^ 2 : ℝ) : ℂ) := by + · have hkey : w * (w⁻¹ - (starRingEnd ℂ) w) = ((1 - ‖w‖ ^ 2 : ℝ) : ℂ) := by + rw [mul_sub, mul_inv_cancel₀ hne, Complex.mul_conj, Complex.normSq_eq_norm_sq] push_cast - ring - rw [h2, Complex.norm_real, Real.norm_eq_abs, - abs_of_nonneg (by nlinarith [norm_nonneg w])] + rfl + rw [← norm_mul, hkey, Complex.norm_real, Real.norm_eq_abs, + abs_of_nonneg (sub_nonneg.2 (pow_le_one₀ (norm_nonneg w) hw))] /-! ### The lemma -/ diff --git a/Sendov/Analytic/FirstOriginAlgebra.lean b/Sendov/Analytic/FirstOriginAlgebra.lean new file mode 100644 index 0000000..d916c32 --- /dev/null +++ b/Sendov/Analytic/FirstOriginAlgebra.lean @@ -0,0 +1,122 @@ +import Sendov.Analytic.Origin + +/-! Finite polynomial integrals and positive decompositions for degrees five and six. +No sampling, general Bernstein framework, or endpoint strictness assumptions. -/ + +namespace Sendov.FirstOriginSmall + +noncomputable def B (a t : ℝ) : ℝ := 1 - a * (1 + a) * t + a ^ 2 * t ^ 2 +noncomputable def Q (a : ℝ) : ℝ := + 120 + 170 * a + 102 * a ^ 2 - 29 * a ^ 3 - 117 * a ^ 4 - 93 * a ^ 5 - 61 * a ^ 6 + 13 * a ^ 7 + 25 * a ^ 8 + 9 * a ^ 9 + a ^ 10 + +lemma integral_quadratic_cube (c d e : ℝ) : + (∫ t in (0 : ℝ)..1, (c + d * t + e * t ^ 2) ^ 3) = + c ^ 3 + 3 * c ^ 2 * d / 2 + (3 * c ^ 2 * e + 3 * c * d ^ 2) / 3 + (6 * c * d * e + d ^ 3) / 4 + (3 * c * e ^ 2 + 3 * d ^ 2 * e) / 5 + 3 * d * e ^ 2 / 6 + e ^ 3 / 7 := by + have hex : (fun t : ℝ => (c + d * t + e * t ^ 2) ^ 3) = + (fun t => c ^ 3 + (3 * c ^ 2 * d) * t ^ 1 + (3 * c ^ 2 * e + 3 * c * d ^ 2) * t ^ 2 + (6 * c * d * e + d ^ 3) * t ^ 3 + (3 * c * e ^ 2 + 3 * d ^ 2 * e) * t ^ 4 + (3 * d * e ^ 2) * t ^ 5 + e ^ 3 * t ^ 6) := by + funext t; ring + rw [hex] + simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _) + only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul, + intervalIntegral.integral_const, integral_pow, integral_id] + norm_num + <;> ring + +lemma integral_t_quadratic_sq (c d e : ℝ) : + (∫ t in (0 : ℝ)..1, t * (c + d * t + e * t ^ 2) ^ 2) = + c ^ 2 / 2 + 2 * c * d / 3 + (2 * c * e + d ^ 2) / 4 + 2 * d * e / 5 + e ^ 2 / 6 := by + have hex : (fun t : ℝ => t * (c + d * t + e * t ^ 2) ^ 2) = + (fun t => c ^ 2 * t ^ 1 + (2 * c * d) * t ^ 2 + (2 * c * e + d ^ 2) * t ^ 3 + (2 * d * e) * t ^ 4 + e ^ 2 * t ^ 5) := by + funext t; ring + rw [hex] + simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _) + only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul, integral_pow, integral_id] + norm_num + <;> ring + +lemma integral_t_linear_fifth (a : ℝ) : + (∫ t in (0 : ℝ)..1, t * (1 - a * t) ^ 5) = + 1 / 2 - 5 * a / 3 + 5 * a ^ 2 / 2 - 2 * a ^ 3 + 5 * a ^ 4 / 6 - a ^ 5 / 7 := by + have hex : (fun t : ℝ => t * (1 - a * t) ^ 5) = + (fun t => t + (-5 * a) * t ^ 2 + (10 * a ^ 2) * t ^ 3 + (-10 * a ^ 3) * t ^ 4 + (5 * a ^ 4) * t ^ 5 + (-a ^ 5) * t ^ 6) := by + funext t; ring + rw [hex] + simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _) + only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul, integral_pow, integral_id] + norm_num + <;> ring + +lemma integral_sq_linear_cube (a : ℝ) : + (∫ t in (0 : ℝ)..1, t ^ 2 * (1 - a * t) ^ 3) = 1 / 3 - 3 * a / 4 + 3 * a ^ 2 / 5 - a ^ 3 / 6 := by + have hex : (fun t : ℝ => t ^ 2 * (1 - a * t) ^ 3) = + (fun t => t ^ 2 + (-3 * a) * t ^ 3 + (3 * a ^ 2) * t ^ 4 + (-a ^ 3) * t ^ 5) := by + funext t; ring + rw [hex] + simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _) + only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul, integral_pow] + norm_num + <;> ring + +lemma polar_cube_integral (a : ℝ) : + 1 - (∫ t in (0 : ℝ)..1, Ppolar a ((1 + a) / 2) t ^ (3 : ℕ)) = (1 - a) ^ 2 * Q a / 140 := by + have hp : (fun t => Ppolar a ((1 + a) / 2) t) = + (fun t => a ^ 2 + (a * (1 - a ^ 2) * (1 + a)) * t + (1 - a ^ 2) ^ 2 * t ^ 2) := by + funext t; unfold Ppolar; ring + simp_rw [hp] + rw [integral_quadratic_cube] + unfold Q + ring + +lemma Q_lower {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) : 92 ≤ Q a := by + have h3 : a ^ 3 ≤ a ^ 2 := pow_le_pow_of_le_one ha0 ha1 (by omega : 2 ≤ 3) + have h4 : a ^ 4 ≤ a ^ 2 := pow_le_pow_of_le_one ha0 ha1 (by omega : 2 ≤ 4) + have h5 : a ^ 5 ≤ a ^ 2 := pow_le_pow_of_le_one ha0 ha1 (by omega : 2 ≤ 5) + have h6 : a ^ 6 ≤ a ^ 2 := pow_le_pow_of_le_one ha0 ha1 (by omega : 2 ≤ 6) + have h2 : a ^ 2 ≤ a := by nlinarith + unfold Q + nlinarith [pow_nonneg ha0 7, pow_nonneg ha0 8, pow_nonneg ha0 9, pow_nonneg ha0 10] + +lemma polar_cube_lt_one {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) : + (∫ t in (0 : ℝ)..1, Ppolar a ((1 + a) / 2) t ^ (3 : ℕ)) < 1 := by + have hQ := Q_lower ha0.le ha1.le + have h := polar_cube_integral a + have hg : 0 < (1 - a) ^ 2 * Q a := mul_pos (sq_pos_of_pos (by linarith)) (by linarith) + linarith + +lemma fifth_sixth_majorant {y : ℝ} (hy : 0 ≤ y) : 6 * y ^ 5 ≤ 1 + 5 * y ^ 6 := by + have hid : 1 + 5 * y ^ 6 - 6 * y ^ 5 = (y - 1) ^ 2 * (5 * y ^ 4 + 4 * y ^ 3 + 3 * y ^ 2 + 2 * y + 1) := by ring + have hp : 0 ≤ (y - 1) ^ 2 * (5 * y ^ 4 + 4 * y ^ 3 + 3 * y ^ 2 + 2 * y + 1) := by positivity + linarith + +lemma five_halves_majorant {u w : ℝ} (hu : 0 ≤ u) (huw : u ≤ w) (hw : w ≤ 1) : + w ^ 5 ≤ u ^ 5 + (5 / 2 : ℝ) * u ^ 3 * (w ^ 2 - u ^ 2) + (15 / 8 : ℝ) * (w ^ 2 - u ^ 2) ^ 2 := by + have hid : u ^ 5 + (5 / 2 : ℝ) * u ^ 3 * (w ^ 2 - u ^ 2) + (15 / 8 : ℝ) * (w ^ 2 - u ^ 2) ^ 2 - w ^ 5 = + (15 / 8 : ℝ) * (1 - w) * (w ^ 2 - u ^ 2) ^ 2 + (w - u) ^ 3 * (5 * u ^ 2 + (35 / 8 : ℝ) * u * (w - u) + (7 / 8 : ℝ) * (w - u) ^ 2) := by ring + have hd : 0 ≤ w - u := sub_nonneg.mpr huw + have hp : 0 ≤ (15 / 8 : ℝ) * (1 - w) * (w ^ 2 - u ^ 2) ^ 2 + (w - u) ^ 3 * (5 * u ^ 2 + (35 / 8 : ℝ) * u * (w - u) + (7 / 8 : ℝ) * (w - u) ^ 2) := by + have : 0 ≤ 1 - w := sub_nonneg.mpr hw + positivity + linarith + +lemma upper_five_gap {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) : + (1 - a) ^ 2 + 5 * a ^ 2 * (∫ t in (0 : ℝ)..1, t * (B a t) ^ 2) < 1 - 5 * a / 6 := by + have he : (fun t => B a t) = (fun t => 1 + (-a * (1 + a)) * t + a ^ 2 * t ^ 2) := by + funext t; unfold B; ring + simp_rw [he] + rw [integral_t_quadratic_sq] + have hh : 0 < 1 - a := by linarith + have hp : 0 < a * (1 - a) * (14 * (1 - a) ^ 4 + 28 * a * (1 - a) ^ 3 + 12 * a ^ 2 * (1 - a) ^ 2 + 3 * a ^ 3 * (1 - a) + 6 * a ^ 4) / 12 := by positivity + have hid : 1 - 5 * a / 6 - ((1 - a) ^ 2 + 5 * a ^ 2 * (1 ^ 2 / 2 + 2 * 1 * (-a * (1 + a)) / 3 + (2 * 1 * a ^ 2 + (-a * (1 + a)) ^ 2) / 4 + 2 * (-a * (1 + a)) * a ^ 2 / 5 + (a ^ 2) ^ 2 / 6)) = + a * (1 - a) * (14 * (1 - a) ^ 4 + 28 * a * (1 - a) ^ 3 + 12 * a ^ 2 * (1 - a) ^ 2 + 3 * a ^ 3 * (1 - a) + 6 * a ^ 4) / 12 := by ring + linarith + +lemma upper_six_gap {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) : + (1 - a) ^ 3 + 6 * a ^ 2 * ((∫ t in (0 : ℝ)..1, t * (1 - a * t) ^ 5) + (5 / 2 : ℝ) * a * (1 - a) * (∫ t in (0 : ℝ)..1, t ^ 2 * (1 - a * t) ^ 3) + (15 / 32 : ℝ) * a ^ 2 * (1 - a) ^ 2) < 1 - 6 * a / 7 := by + rw [integral_t_linear_fifth, integral_sq_linear_cube] + have hh : 0 < 1 - a := by linarith + have hp : 0 < a * (1 - a) * (240 * (1 - a) ^ 5 + 768 * a * (1 - a) ^ 4 + 912 * a ^ 2 * (1 - a) ^ 3 + 593 * a ^ 3 * (1 - a) ^ 2 + 93 * a ^ 4 * (1 - a) + 68 * a ^ 5) / 112 := by positivity + have hid : 1 - 6 * a / 7 - ((1 - a) ^ 3 + 6 * a ^ 2 * ((1 / 2 - 5 * a / 3 + 5 * a ^ 2 / 2 - 2 * a ^ 3 + 5 * a ^ 4 / 6 - a ^ 5 / 7) + (5 / 2 : ℝ) * a * (1 - a) * (1 / 3 - 3 * a / 4 + 3 * a ^ 2 / 5 - a ^ 3 / 6) + (15 / 32 : ℝ) * a ^ 2 * (1 - a) ^ 2)) = + a * (1 - a) * (240 * (1 - a) ^ 5 + 768 * a * (1 - a) ^ 4 + 912 * a ^ 2 * (1 - a) ^ 3 + 593 * a ^ 3 * (1 - a) ^ 2 + 93 * a ^ 4 * (1 - a) + 68 * a ^ 5) / 112 := by ring + linarith + +end Sendov.FirstOriginSmall diff --git a/Sendov/Analytic/FirstOriginBounds.lean b/Sendov/Analytic/FirstOriginBounds.lean new file mode 100644 index 0000000..39563a6 --- /dev/null +++ b/Sendov/Analytic/FirstOriginBounds.lean @@ -0,0 +1,166 @@ +import Sendov.Analytic.FirstOriginAlgebra + +/-! The raw polar mean bound and the complete T budgets on 0 < a < 1. +The five/six split is intentional; no extrapolation to larger degrees. -/ + +namespace Sendov.FirstOriginSmall + +lemma sqrt_pow_eq_rpow {z : ℝ} (hz : 0 ≤ z) (k : ℕ) : + (Real.sqrt z) ^ k = z ^ ((k : ℝ) / 2) := by + rw [Real.sqrt_eq_rpow, ← Real.rpow_natCast, ← Real.rpow_mul hz] + congr 1 + ring + +lemma Ppolar_nonneg_small {a x t : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) + (hx : -1 ≤ x) (ht : 0 ≤ t) : 0 ≤ Ppolar a x t := by + have hd : 0 ≤ 1 - a ^ 2 := by nlinarith + have hid : Ppolar a x t = (a - (1 - a ^ 2) * t) ^ 2 + 2 * a * (1 - a ^ 2) * t * (x + 1) := by + unfold Ppolar; ring + rw [hid] + have : 0 ≤ x + 1 := by linarith + positivity + +lemma Ppolar_le_half {a x t : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) + (hx : x ≤ (1 + a) / 2) (ht : 0 ≤ t) : Ppolar a x t ≤ Ppolar a ((1 + a) / 2) t := by + have hd : 0 ≤ 1 - a ^ 2 := by nlinarith + have hh : 0 ≤ (1 + a) / 2 - x := sub_nonneg.mpr hx + have hp := mul_nonneg (mul_nonneg (mul_nonneg (by positivity : 0 ≤ 2 * a) hd) ht) hh + unfold Ppolar + nlinarith only [hp] + +lemma polar_mean_gt_half_add_one {n : ℕ} (hn : n = 6 ∨ n = 7) {a x : ℝ} + (ha0 : 0 < a) (ha1 : a < 1) (hx0 : -1 ≤ x) + (hpolar : 1 ≤ ∫ t in (0 : ℝ)..1, Ppolar a x t ^ (((n : ℝ) - 1) / 2)) : + (1 + a) / 2 < x := by + by_contra hx + have hx : x ≤ (1 + a) / 2 := le_of_not_gt hx + have hcube := polar_cube_lt_one ha0 ha1 + have hcp : Continuous (fun t => Ppolar a ((1 + a) / 2) t ^ (3 : ℕ)) := by + exact (continuous_Ppolar _ _).pow 3 + rcases hn with rfl | rfl + · norm_num at hpolar + have hcont : Continuous (fun t => Ppolar a x t ^ (5 / 2 : ℝ)) := + (continuous_rpow_const (by norm_num : (0 : ℝ) ≤ 5 / 2)).comp (continuous_Ppolar a x) + have hi := intervalIntegral.integral_mono_on (μ := MeasureTheory.volume) (by norm_num : (0 : ℝ) ≤ 1) + (hcont.intervalIntegrable 0 1) + ((continuous_const.add (continuous_const.mul hcp)).intervalIntegrable 0 1) + (show ∀ t ∈ Set.Icc (0 : ℝ) 1, + Ppolar a x t ^ (5 / 2 : ℝ) ≤ (1 / 6 : ℝ) + (5 / 6 : ℝ) * Ppolar a ((1 + a) / 2) t ^ (3 : ℕ) from by + intro t ht + have hp0 := Ppolar_nonneg_small ha0.le ha1.le hx0 ht.1 + have hp1 := Ppolar_le_half ha0.le ha1.le hx ht.1 + have hz : 0 ≤ Ppolar a ((1 + a) / 2) t := hp0.trans hp1 + have hm := Real.rpow_le_rpow hp0 hp1 (by norm_num : (0 : ℝ) ≤ 5 / 2) + have hf := fifth_sixth_majorant (Real.sqrt_nonneg (Ppolar a ((1 + a) / 2) t)) + rw [sqrt_pow_eq_rpow hz 5, sqrt_pow_eq_rpow hz 6] at hf + norm_num [Real.rpow_natCast] at hf + linarith) + dsimp only [Pi.add_apply, Pi.mul_apply, Pi.pow_apply] at hi + simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _) + only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul, + intervalIntegral.integral_const] at hi + norm_num at hi + linarith + · norm_num [Real.rpow_natCast] at hpolar + have hi := intervalIntegral.integral_mono_on (μ := MeasureTheory.volume) (by norm_num : (0 : ℝ) ≤ 1) + (((continuous_Ppolar a x).pow 3).intervalIntegrable 0 1) + (hcp.intervalIntegrable 0 1) (show ∀ t ∈ Set.Icc (0 : ℝ) 1, + Ppolar a x t ^ (3 : ℕ) ≤ Ppolar a ((1 + a) / 2) t ^ (3 : ℕ) from by + intro t ht + exact pow_le_pow_left₀ (Ppolar_nonneg_small ha0.le ha1.le hx0 ht.1) + (Ppolar_le_half ha0.le ha1.le hx ht.1) 3) + dsimp only [Pi.pow_apply] at hi + linarith + +lemma beta_B_bounds {a x t : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) + (hx : (1 + a) / 2 ≤ x) (hx1 : x ≤ 1) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : + 0 ≤ QQ (a * x) (a ^ 2) t ∧ QQ (a * x) (a ^ 2) t ≤ B a t ∧ + (1 - a * t) ^ 2 ≤ B a t ∧ B a t ≤ 1 ∧ 0 ≤ 1 - a * t := by + have hat : a * t ≤ 1 := (mul_le_mul_of_nonneg_left ht1 ha0).trans (by simpa using ha1) + have hq : QQ (a * x) (a ^ 2) t = (1 - a * t) ^ 2 + 2 * a * t * (1 - x) := by unfold QQ; ring + have hb : B a t = (1 - a * t) ^ 2 + a * (1 - a) * t := by unfold B; ring + have hdiff : B a t - QQ (a * x) (a ^ 2) t = 2 * a * t * (x - (1 + a) / 2) := by + unfold B QQ; ring + have hupper : 1 - B a t = a * t * (1 + a - a * t) := by unfold B; ring + have hp : 0 ≤ a * (1 - a) * t := by positivity + have hp2 : 0 ≤ 2 * a * t * (1 - x) := by positivity + have hp3 : 0 ≤ 2 * a * t * (x - (1 + a) / 2) := by positivity + have hp4 : 0 ≤ a * t * (1 + a - a * t) := by + have : 0 ≤ 1 + a - a * t := by linarith + positivity + constructor + · rw [hq]; positivity + constructor + · linarith + constructor + · linarith + constructor <;> linarith + +lemma B_five_halves {a t : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) + (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : + B a t ^ (5 / 2 : ℝ) ≤ (1 - a * t) ^ 5 + (5 / 2 : ℝ) * a * (1 - a) * t * (1 - a * t) ^ 3 + (15 / 8 : ℝ) * a ^ 2 * (1 - a) ^ 2 * t ^ 2 := by + obtain ⟨_, _, hu2, hb1, hu⟩ := beta_B_bounds ha0 ha1 (le_refl ((1 + a) / 2)) + (by linarith : (1 + a) / 2 ≤ 1) ht0 ht1 + have hb0 : 0 ≤ B a t := (sq_nonneg _).trans hu2 + have hsq := Real.sq_sqrt hb0 + have huw : 1 - a * t ≤ Real.sqrt (B a t) := by + nlinarith [Real.sqrt_nonneg (B a t)] + have hw1 : Real.sqrt (B a t) ≤ 1 := by + nlinarith [Real.sqrt_nonneg (B a t)] + have h := five_halves_majorant hu huw hw1 + rw [sqrt_pow_eq_rpow hb0 5, hsq] at h + have he : B a t - (1 - a * t) ^ 2 = a * (1 - a) * t := by unfold B; ring + rw [he] at h + convert h using 1 <;> ring + +lemma direct_budget_five {a x : ℝ} (ha0 : 0 < a) (ha1 : a < 1) + (hx : (1 + a) / 2 ≤ x) (hx1 : x ≤ 1) : + QQ (a * x) (a ^ 2) 1 ^ (5 / 2 : ℝ) + 5 * a ^ 2 * (∫ t in (0 : ℝ)..1, t * QQ (a * x) (a ^ 2) t ^ (2 : ℕ)) < 1 - 5 * a / 6 := by + have hend := beta_B_bounds ha0.le ha1.le hx hx1 (by norm_num : (0 : ℝ) ≤ 1) le_rfl + have heB : B a 1 = 1 - a := by unfold B; ring + have he := Real.rpow_le_rpow hend.1 hend.2.1 (by norm_num : (0 : ℝ) ≤ 5 / 2) + rw [heB] at he + have he2 := Real.rpow_le_rpow_of_exponent_ge (by linarith : 0 < 1 - a) + (by linarith : 1 - a ≤ 1) (by norm_num : (2 : ℝ) ≤ 5 / 2) + norm_num [Real.rpow_natCast] at he2 + have hi : (∫ t in (0 : ℝ)..1, t * QQ (a * x) (a ^ 2) t ^ (2 : ℕ)) ≤ + ∫ t in (0 : ℝ)..1, t * (B a t) ^ 2 := by + apply intervalIntegral.integral_mono_on (by norm_num) + (Continuous.intervalIntegrable (by unfold QQ; fun_prop) _ _) + (Continuous.intervalIntegrable (by unfold B; fun_prop) _ _) + intro t ht + have hb := beta_B_bounds ha0.le ha1.le hx hx1 ht.1 ht.2 + exact mul_le_mul_of_nonneg_left (pow_le_pow_left₀ hb.1 hb.2.1 2) ht.1 + have hmul := mul_le_mul_of_nonneg_left hi (by positivity : 0 ≤ 5 * a ^ 2) + have hg := upper_five_gap ha0 ha1 + linarith + +lemma direct_budget_six {a x : ℝ} (ha0 : 0 < a) (ha1 : a < 1) + (hx : (1 + a) / 2 ≤ x) (hx1 : x ≤ 1) : + QQ (a * x) (a ^ 2) 1 ^ (3 : ℕ) + 6 * a ^ 2 * (∫ t in (0 : ℝ)..1, t * QQ (a * x) (a ^ 2) t ^ (5 / 2 : ℝ)) < 1 - 6 * a / 7 := by + have hend := beta_B_bounds ha0.le ha1.le hx hx1 (by norm_num : (0 : ℝ) ≤ 1) le_rfl + have heB : B a 1 = 1 - a := by unfold B; ring + have he := pow_le_pow_left₀ hend.1 hend.2.1 3 + rw [heB] at he + have hi : (∫ t in (0 : ℝ)..1, t * QQ (a * x) (a ^ 2) t ^ (5 / 2 : ℝ)) ≤ + ∫ t in (0 : ℝ)..1, (t * (1 - a * t) ^ 5 + ((5 / 2 : ℝ) * a * (1 - a)) * (t ^ 2 * (1 - a * t) ^ 3) + ((15 / 8 : ℝ) * a ^ 2 * (1 - a) ^ 2) * t ^ 3) := by + apply intervalIntegral.integral_mono_on (by norm_num) + (by simpa only [pow_one] using + (continuous_pow_mul_QQ (a * x) (a ^ 2) 1 (by norm_num : (0 : ℝ) ≤ 5 / 2)).intervalIntegrable 0 1) + (Continuous.intervalIntegrable (by fun_prop) _ _) + intro t ht + have hb := beta_B_bounds ha0.le ha1.le hx hx1 ht.1 ht.2 + have hp := (Real.rpow_le_rpow hb.1 hb.2.1 (by norm_num : (0 : ℝ) ≤ 5 / 2)).trans + (B_five_halves ha0.le ha1.le ht.1 ht.2) + have hm := mul_le_mul_of_nonneg_left hp ht.1 + calc + _ ≤ t * ((1 - a * t) ^ 5 + (5 / 2 : ℝ) * a * (1 - a) * t * (1 - a * t) ^ 3 + (15 / 8 : ℝ) * a ^ 2 * (1 - a) ^ 2 * t ^ 2) := hm + _ = _ := by ring + simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _) + only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul, integral_pow] at hi + norm_num at hi + have hmul := mul_le_mul_of_nonneg_left hi (by positivity : 0 ≤ 6 * a ^ 2) + have hg := upper_six_gap ha0 ha1 + nlinarith only [he, hmul, hg] + +end Sendov.FirstOriginSmall diff --git a/Sendov/Analytic/FirstOriginBudget.lean b/Sendov/Analytic/FirstOriginBudget.lean new file mode 100644 index 0000000..aed9631 --- /dev/null +++ b/Sendov/Analytic/FirstOriginBudget.lean @@ -0,0 +1,101 @@ +import Sendov.Analytic.FirstOriginSmall +import Sendov.Analytic.PaperNear +import Sendov.Analytic.PaperUniform + +/-! Generic first-origin consumers of the scalar D estimates. +No second-origin or polynomial centroid identity is used in these proofs. -/ +namespace Sendov.FirstOriginBudget + +lemma beta_eq_QQ (a x t : ℝ) : PaperTaylor.beta a x t = QQ (a * x) (a ^ 2) t := by + unfold PaperTaylor.beta QQ + ring + +/-- First-origin forces the opposite of D, in the closed pointwise disk domain. -/ +theorem lower_budget {n : ℕ} (hn : 2 ≤ n) {a x y : ℝ} {q : Multiset ℂ} + (ha : 0 < a) (ha1 : a < 1) (hx1 : x ≤ 1) + (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) + (hx : (q.map (fun v => v.re)).sum = ((n : ℝ) - 1) * x) + (hsum : q.sum = ((n : ℂ) - 1) * ((x : ℂ) + (y : ℂ) * Complex.I)) + (hfirst : ‖∫ t in (0 : ℝ)..1, Fprod a q t‖ ≤ 1 / (n : ℝ)) : + 1 ≤ PaperTaylor.budget ((n : ℝ) - 1) a x + a * ((n : ℝ) - 1) / (n : ℝ) := by + have hnR : (2 : ℝ) ≤ n := by exact_mod_cast hn + have hm0 : 0 ≤ (n : ℝ) - 1 := by linarith + have hc : (q.card : ℝ) = (n : ℝ) - 1 := by + rw [hqcard, Nat.cast_sub (by omega : 1 ≤ n)] + norm_num + have hq0 : q ≠ 0 := by + intro h + simp [h] at hqcard + omega + have hsumle := FirstOriginSmall.norm_sum_le_card q hq1 + rw [hc] at hsumle + have ht := one_le_tri hn hqcard hq0 hq1 ha.le hx hsum + have hβ : 0 ≤ QQ (a * x) (a ^ 2) 1 := by + rw [← beta_eq_QQ] + exact (PaperTaylor.beta_pos ha ha1 hx1 (by norm_num)).le + have hf := FirstOriginSmall.norm_Fprod_le hn hqcard hq1 hx hβ + have hcoef : ((n : ℂ) - 1) * (a : ℂ) * ((x : ℂ) + (y : ℂ) * Complex.I) = + (a : ℂ) * q.sum := by rw [hsum]; ring + rw [hcoef] at ht + have hi : ‖(a : ℂ) * q.sum * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ ≤ + a * ((n : ℝ) - 1) / (n : ℝ) := by + rw [norm_mul, norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos ha] + have hmul := mul_le_mul (mul_le_mul_of_nonneg_left hsumle ha.le) hfirst + (norm_nonneg _) (by positivity : 0 ≤ a * ((n : ℝ) - 1)) + simpa only [mul_one_div] using hmul + have htri := norm_add_le (Fprod a q 1) + ((a : ℂ) * q.sum * (∫ t in (0 : ℝ)..1, Fprod a q t)) + have hexp : (n : ℝ) - 1 - 1 = (n : ℝ) - 2 := by ring + simp only [PaperTaylor.budget, beta_eq_QQ, hexp] + nlinarith only [ht, hf, hi, htri] + +/-- The near-endpoint raw-polar theorem is consumed without an analytic assumption. -/ +theorem near_contradiction {n : ℕ} (hn : 8 ≤ n) {a x y : ℝ} {q : Multiset ℂ} + (ha : 0 < a) (ha1 : a < 1) (hx0 : -1 ≤ x) (hx1 : x ≤ 1) + (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) + (hx : (q.map (fun v => v.re)).sum = ((n : ℝ) - 1) * x) + (hsum : q.sum = ((n : ℂ) - 1) * ((x : ℂ) + (y : ℂ) * Complex.I)) + (hraw : 1 ≤ ∫ t in (0 : ℝ)..1, Ppolar a x t ^ (((n : ℝ) - 1) / 2)) + (hnear : ((n : ℝ) - 1) * (1 - a) ≤ 2 / 5) + (hfirst : ‖∫ t in (0 : ℝ)..1, Fprod a q t‖ ≤ 1 / (n : ℝ)) : False := by + have hm : 7 ≤ n - 1 := by omega + have hcast : ((n - 1 : ℕ) : ℝ) = (n : ℝ) - 1 := by + rw [Nat.cast_sub (by omega : 1 ≤ n)] + norm_num + have hr : PaperPolar.RawPolar (n - 1) a x := by + rw [PaperPolar.rawPolar_iff, hcast] + exact hraw + have hd := PaperNearClosure.near_endpoint_D hm ha ha1 hx0 hx1 hr + (by simpa only [hcast] using hnear) + have hl := lower_budget (by omega) ha ha1 hx1 hqcard hq1 hx hsum hfirst + rw [hcast] at hd + have he : (n : ℝ) - 1 + 1 = n := by ring + rw [he] at hd + have hh : 0 < (1 - a) / 1000 := by positivity + rw [mul_comm a ((n : ℝ) - 1)] at hl + linarith + +/-- All degrees n≥257 close using only polar and the first-origin bound. -/ +theorem uniform_contradiction {n : ℕ} (hn : 257 ≤ n) {a x y : ℝ} {q : Multiset ℂ} + (ha : 0 < a) (ha1 : a < 1) (hx0 : -1 ≤ x) (hx1 : x ≤ 1) + (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) + (hx : (q.map (fun v => v.re)).sum = ((n : ℝ) - 1) * x) + (hsum : q.sum = ((n : ℂ) - 1) * ((x : ℂ) + (y : ℂ) * Complex.I)) + (hraw : 1 ≤ ∫ t in (0 : ℝ)..1, Ppolar a x t ^ (((n : ℝ) - 1) / 2)) + (hfirst : ‖∫ t in (0 : ℝ)..1, Fprod a q t‖ ≤ 1 / (n : ℝ)) : False := by + have hm : 256 ≤ n - 1 := by omega + have hcast : ((n - 1 : ℕ) : ℝ) = (n : ℝ) - 1 := by + rw [Nat.cast_sub (by omega : 1 ≤ n)] + norm_num + have hr : PaperPolar.RawPolar (n - 1) a x := by + rw [PaperPolar.rawPolar_iff, hcast] + exact hraw + have hd := PaperUniform.uniform_D hm ha ha1 hx0 hx1 hr + have hl := lower_budget (by omega) ha ha1 hx1 hqcard hq1 hx hsum hfirst + rw [hcast] at hd + have he : (n : ℝ) - 1 + 1 = n := by ring + rw [he] at hd + rw [mul_comm a ((n : ℝ) - 1)] at hl + linarith + +end Sendov.FirstOriginBudget diff --git a/Sendov/Analytic/FirstOriginMargins.lean b/Sendov/Analytic/FirstOriginMargins.lean new file mode 100644 index 0000000..c0c6955 --- /dev/null +++ b/Sendov/Analytic/FirstOriginMargins.lean @@ -0,0 +1,284 @@ +import Sendov.Analytic.FirstOriginSmall + +/-! +# Quantitative first-origin margins for m = 5, 6 + +The hypotheses concern only the pointwise closed disk and the polar integral. +In particular, no first-origin factorization or upper bound on the integral is +assumed. The conclusion is a direct lower bound on its norm, not a contradiction. +The polynomial constants and the actual (not surrogate) T budgets are exposed. +-/ +namespace Sendov.FirstOriginMargins + +open FirstOriginSmall + +noncomputable def A5 (a : ℝ) : ℝ := + 7 / 6 - (7 / 3) * a + a ^ 2 + (7 / 12) * a ^ 3 + (1 / 12) * a ^ 4 + +noncomputable def A6 (a : ℝ) : ℝ := + 15 / 7 - (27 / 7) * a + (15 / 7) * a ^ 2 + (65 / 112) * a ^ 3 - + (229 / 112) * a ^ 4 + (23 / 14) * a ^ 5 + +/-- Explicit nonnegative Bernstein remainder after subtracting 1/16. -/ +lemma A5_remainder (a : ℝ) : + A5 a - 1 / 16 = (53 / 48) * (1 - a) ^ 4 + (25 / 12) * a * (1 - a) ^ 3 + + (5 / 8) * a ^ 2 * (1 - a) ^ 2 + (7 / 16) * a ^ 4 := by + unfold A5 + ring + +/-- Explicit nonnegative Bernstein remainder after subtracting 93/560. -/ +lemma A6_remainder (a : ℝ) : + A6 a - 93 / 560 = (1107 / 560) * (1 - a) ^ 5 + + (675 / 112) * a * (1 - a) ^ 4 + (363 / 56) * a ^ 2 * (1 - a) ^ 3 + + (407 / 112) * a ^ 3 * (1 - a) ^ 2 + (247 / 560) * a ^ 5 := by + unfold A6 + ring + +lemma A5_lower {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) : 1 / 16 ≤ A5 a := by + have hh : 0 ≤ 1 - a := sub_nonneg.mpr ha1 + have hp : 0 ≤ A5 a - 1 / 16 := by rw [A5_remainder]; positivity + linarith + +lemma A6_lower {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) : 93 / 560 ≤ A6 a := by + have hh : 0 ≤ 1 - a := sub_nonneg.mpr ha1 + have hp : 0 ≤ A6 a - 93 / 560 := by rw [A6_remainder]; positivity + linarith + +lemma upper_five_gap_identity (a : ℝ) : + 1 - 5 * a / 6 - ((1 - a) ^ 2 + + 5 * a ^ 2 * (∫ t in (0 : ℝ)..1, t * B a t ^ 2)) = a * (1 - a) * A5 a := by + have he : (fun t => B a t) = + (fun t => 1 + (-a * (1 + a)) * t + a ^ 2 * t ^ 2) := by + funext t; unfold B; ring + simp_rw [he] + rw [integral_t_quadratic_sq] + unfold A5 + ring + +lemma upper_six_gap_identity (a : ℝ) : + 1 - 6 * a / 7 - ((1 - a) ^ 3 + 6 * a ^ 2 * + ((∫ t in (0 : ℝ)..1, t * (1 - a * t) ^ 5) + + (5 / 2 : ℝ) * a * (1 - a) * + (∫ t in (0 : ℝ)..1, t ^ 2 * (1 - a * t) ^ 3) + + (15 / 32 : ℝ) * a ^ 2 * (1 - a) ^ 2)) = a * (1 - a) * A6 a := by + rw [integral_t_linear_fifth, integral_sq_linear_cube] + unfold A6 + ring + +/-- The actual direct budget, with real exponents and the original QQ integrand. -/ +noncomputable def T (m a x : ℝ) : ℝ := + QQ (a * x) (a ^ 2) 1 ^ (m / 2) + + m * a ^ 2 * (∫ t in (0 : ℝ)..1, t * QQ (a * x) (a ^ 2) t ^ ((m - 1) / 2)) + +lemma T_five_gap {a x : ℝ} (ha0 : 0 < a) (ha1 : a < 1) + (hx : (1 + a) / 2 ≤ x) (hx1 : x ≤ 1) : + T 5 a x ≤ 1 - 5 * a / 6 - a * (1 - a) / 16 := by + have hend := beta_B_bounds ha0.le ha1.le hx hx1 (by norm_num : (0 : ℝ) ≤ 1) le_rfl + have heB : B a 1 = 1 - a := by unfold B; ring + have he := Real.rpow_le_rpow hend.1 hend.2.1 (by norm_num : (0 : ℝ) ≤ 5 / 2) + rw [heB] at he + have he2 := Real.rpow_le_rpow_of_exponent_ge (by linarith : 0 < 1 - a) + (by linarith : 1 - a ≤ 1) (by norm_num : (2 : ℝ) ≤ 5 / 2) + norm_num [Real.rpow_natCast] at he2 + have hi : (∫ t in (0 : ℝ)..1, t * QQ (a * x) (a ^ 2) t ^ (2 : ℕ)) ≤ + ∫ t in (0 : ℝ)..1, t * (B a t) ^ 2 := by + apply intervalIntegral.integral_mono_on (by norm_num) + (Continuous.intervalIntegrable (by unfold QQ; fun_prop) _ _) + (Continuous.intervalIntegrable (by unfold B; fun_prop) _ _) + intro t ht + have hb := beta_B_bounds ha0.le ha1.le hx hx1 ht.1 ht.2 + exact mul_le_mul_of_nonneg_left (pow_le_pow_left₀ hb.1 hb.2.1 2) ht.1 + have hmul := mul_le_mul_of_nonneg_left hi (by positivity : 0 ≤ 5 * a ^ 2) + have hg := upper_five_gap_identity a + have hl := mul_le_mul_of_nonneg_left (A5_lower ha0.le ha1.le) + (by positivity : 0 ≤ a * (1 - a)) + norm_num [T, Real.rpow_natCast] + linarith + +lemma T_six_gap {a x : ℝ} (ha0 : 0 < a) (ha1 : a < 1) + (hx : (1 + a) / 2 ≤ x) (hx1 : x ≤ 1) : + T 6 a x ≤ 1 - 6 * a / 7 - (93 / 560) * a * (1 - a) := by + have hend := beta_B_bounds ha0.le ha1.le hx hx1 (by norm_num : (0 : ℝ) ≤ 1) le_rfl + have heB : B a 1 = 1 - a := by unfold B; ring + have he := pow_le_pow_left₀ hend.1 hend.2.1 3 + rw [heB] at he + have hi : (∫ t in (0 : ℝ)..1, t * QQ (a * x) (a ^ 2) t ^ (5 / 2 : ℝ)) ≤ + ∫ t in (0 : ℝ)..1, (t * (1 - a * t) ^ 5 + + ((5 / 2 : ℝ) * a * (1 - a)) * (t ^ 2 * (1 - a * t) ^ 3) + + ((15 / 8 : ℝ) * a ^ 2 * (1 - a) ^ 2) * t ^ 3) := by + apply intervalIntegral.integral_mono_on (by norm_num) + (by simpa only [pow_one] using + (continuous_pow_mul_QQ (a * x) (a ^ 2) 1 + (by norm_num : (0 : ℝ) ≤ 5 / 2)).intervalIntegrable 0 1) + (Continuous.intervalIntegrable (by fun_prop) _ _) + intro t ht + have hb := beta_B_bounds ha0.le ha1.le hx hx1 ht.1 ht.2 + have hp := (Real.rpow_le_rpow hb.1 hb.2.1 (by norm_num : (0 : ℝ) ≤ 5 / 2)).trans + (B_five_halves ha0.le ha1.le ht.1 ht.2) + have hm := mul_le_mul_of_nonneg_left hp ht.1 + calc + _ ≤ t * ((1 - a * t) ^ 5 + (5 / 2 : ℝ) * a * (1 - a) * t * + (1 - a * t) ^ 3 + (15 / 8 : ℝ) * a ^ 2 * (1 - a) ^ 2 * t ^ 2) := hm + _ = _ := by ring + simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _) + only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul, integral_pow] at hi + norm_num at hi + have hmul := mul_le_mul_of_nonneg_left hi (by positivity : 0 ≤ 6 * a ^ 2) + have hg := upper_six_gap_identity a + have hl := mul_le_mul_of_nonneg_left (A6_lower ha0.le ha1.le) + (by positivity : 0 ≤ a * (1 - a)) + norm_num [T, Real.rpow_natCast] + nlinarith only [he, hmul, hg, hl] + +/-- General lower budget retaining the actual norm of J, without assuming it ≤ 1. +The explicit beta nonnegativity hypothesis permits reuse beyond the small degrees. -/ +theorem lower_budget_norm {n : ℕ} (hn : 2 ≤ n) {a x y : ℝ} {q : Multiset ℂ} + (ha : 0 ≤ a) + (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) + (hx : (q.map (fun v => v.re)).sum = ((n : ℝ) - 1) * x) + (hsum : q.sum = ((n : ℂ) - 1) * ((x : ℂ) + (y : ℂ) * Complex.I)) + (hβ : 0 ≤ QQ (a * x) (a ^ 2) 1) : + 1 ≤ T ((n : ℝ) - 1) a x + a * ((n : ℝ) - 1) / (n : ℝ) * + ‖(n : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ := by + have hnR : (2 : ℝ) ≤ n := by exact_mod_cast hn + have hn0 : (n : ℝ) ≠ 0 := by linarith + have hc : (q.card : ℝ) = (n : ℝ) - 1 := by + rw [hqcard, Nat.cast_sub (by omega : 1 ≤ n)]; norm_num + have hq0 : q ≠ 0 := by + intro h + simp [h] at hqcard + omega + have hsumle := norm_sum_le_card q hq1 + rw [hc] at hsumle + have ht := one_le_tri hn hqcard hq0 hq1 ha hx hsum + have hf := norm_Fprod_le hn hqcard hq1 hx hβ + have hcoef : ((n : ℂ) - 1) * (a : ℂ) * ((x : ℂ) + (y : ℂ) * Complex.I) = + (a : ℂ) * q.sum := by rw [hsum]; ring + rw [hcoef] at ht + have hi : ‖(a : ℂ) * q.sum * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ ≤ + a * ((n : ℝ) - 1) / (n : ℝ) * + ‖(n : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ := by + simp only [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg ha, + Complex.norm_natCast] + have hm := mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hsumle ha) + (norm_nonneg (∫ t in (0 : ℝ)..1, Fprod a q t)) + have he : a * ((n : ℝ) - 1) / (n : ℝ) * + ((n : ℝ) * ‖∫ t in (0 : ℝ)..1, Fprod a q t‖) = + a * ((n : ℝ) - 1) * ‖∫ t in (0 : ℝ)..1, Fprod a q t‖ := by + field_simp + rw [he] + exact hm + have htri := norm_add_le (Fprod a q 1) + ((a : ℂ) * q.sum * (∫ t in (0 : ℝ)..1, Fprod a q t)) + have hexp : (n : ℝ) - 1 - 1 = (n : ℝ) - 2 := by ring + simp only [T, hexp] + nlinarith only [ht, hf, hi, htri] + +/-- Solved form of the general norm budget. No polar or first-origin upper bound +is needed; those hypotheses are not hidden in the beta nonnegativity proof. -/ +theorem norm_J_lower {n : ℕ} (hn : 2 ≤ n) {a x y : ℝ} {q : Multiset ℂ} + (ha : 0 < a) (hx1 : x ≤ 1) + (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) + (hx : (q.map (fun v => v.re)).sum = ((n : ℝ) - 1) * x) + (hsum : q.sum = ((n : ℂ) - 1) * ((x : ℂ) + (y : ℂ) * Complex.I)) : + ((1 - T ((n : ℝ) - 1) a x) * (n : ℝ)) / (a * ((n : ℝ) - 1)) ≤ + ‖(n : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ := by + have hnR : (2 : ℝ) ≤ n := by exact_mod_cast hn + have hn0 : (n : ℝ) ≠ 0 := by linarith + have hm0 : 0 < (n : ℝ) - 1 := by linarith + have hβ : 0 ≤ QQ (a * x) (a ^ 2) 1 := by + have he : QQ (a * x) (a ^ 2) 1 = (1 - a) ^ 2 + 2 * a * (1 - x) := by + unfold QQ; ring + rw [he] + have : 0 ≤ 1 - x := sub_nonneg.mpr hx1 + positivity + have hl := lower_budget_norm hn ha.le hqcard hq1 hx hsum hβ + have hs : 1 - T ((n : ℝ) - 1) a x ≤ a * ((n : ℝ) - 1) / (n : ℝ) * + ‖(n : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ := by linarith + have hmul := mul_le_mul_of_nonneg_right hs (by linarith : (0 : ℝ) ≤ n) + have he : a * ((n : ℝ) - 1) / (n : ℝ) * + ‖(n : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ * (n : ℝ) = + ‖(n : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ * (a * ((n : ℝ) - 1)) := by + field_simp + rw [he] at hmul + exact (div_le_iff₀ (mul_pos ha hm0)).mpr hmul + +/-- The finite mean coordinates, proved solely from the pointwise closed disk. -/ +lemma mean_coordinates {n : ℕ} (hn : 2 ≤ n) {q : Multiset ℂ} + (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) : + ∃ x y : ℝ, -1 ≤ x ∧ x ≤ 1 ∧ + (q.map (fun v => v.re)).sum = ((n : ℝ) - 1) * x ∧ + q.sum = ((n : ℂ) - 1) * ((x : ℂ) + (y : ℂ) * Complex.I) := by + have hnR : (2 : ℝ) ≤ n := by exact_mod_cast hn + have hm0 : 0 < (n : ℝ) - 1 := by linarith + have hmC : (n : ℂ) - 1 ≠ 0 := by exact_mod_cast (ne_of_gt hm0) + have hc : (q.card : ℝ) = (n : ℝ) - 1 := by + rw [hqcard, Nat.cast_sub (by omega : 1 ≤ n)]; norm_num + let μ : ℂ := q.sum / ((n : ℂ) - 1) + have hsum : q.sum = ((n : ℂ) - 1) * ((μ.re : ℂ) + (μ.im : ℂ) * Complex.I) := by + rw [Complex.re_add_im] + dsimp [μ] + field_simp + have hnc : ‖(n : ℂ) - 1‖ = (n : ℝ) - 1 := by + have he : (n : ℂ) - 1 = (((n : ℝ) - 1 : ℝ) : ℂ) := by push_cast; rfl + rw [he, Complex.norm_real, Real.norm_eq_abs, abs_of_pos hm0] + have hqsum := norm_sum_le_card q hq1 + rw [hc] at hqsum + have hμ : ‖μ‖ ≤ 1 := by + dsimp [μ] + rw [norm_div, hnc, div_le_iff₀ hm0] + simpa using hqsum + have hx0 : -1 ≤ μ.re := by + have h := Complex.abs_re_le_norm μ + exact (abs_le.mp (h.trans hμ)).1 + have hx1 : μ.re ≤ 1 := (Complex.re_le_norm μ).trans hμ + have hx : (q.map (fun v => v.re)).sum = ((n : ℝ) - 1) * μ.re := by + have hre : (q.map (fun v => v.re)).sum = q.sum.re := + (map_multiset_sum Complex.reAddGroupHom q).symm + rw [hre, hsum] + simp + exact ⟨μ.re, μ.im, hx0, hx1, hx, hsum⟩ + +/-- n = 6: a quantitative lower norm bound from pointwise disk plus polar alone. -/ +theorem norm_J_six {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) {q : Multiset ℂ} + (hqcard : q.card = 6 - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) + (hstar : 1 ≤ ∫ t in (0 : ℝ)..1, + (q.map (fun v => ‖(a : ℂ) + (t : ℂ) * (1 - (a : ℂ) ^ 2) * v‖)).prod) : + 1 + (3 / 40 : ℝ) * (1 - a) ≤ + ‖(6 : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ := by + obtain ⟨x, y, hx0, hx1, hx, hsum⟩ := mean_coordinates (by norm_num : 2 ≤ 6) hqcard hq1 + have hpolar := one_le_integral_Ppolar (by norm_num : 2 ≤ 6) hqcard hq1 hx hstar + have hxhalf := polar_mean_gt_half_add_one (Or.inl rfl : 6 = 6 ∨ 6 = 7) ha0 ha1 hx0 hpolar + have hβ := (beta_B_bounds ha0.le ha1.le hxhalf.le hx1 + (by norm_num : (0 : ℝ) ≤ 1) le_rfl).1 + have hl := lower_budget_norm (by norm_num : 2 ≤ 6) ha0.le hqcard hq1 hx hsum hβ + have hg := T_five_gap ha0 ha1 hxhalf.le hx1 + norm_num at hl + have hm : a * (1 + (3 / 40 : ℝ) * (1 - a)) ≤ + a * ‖(6 : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ := by + norm_num + nlinarith only [hl, hg] + exact (mul_le_mul_iff_right₀ ha0).mp hm + +/-- n = 7: a quantitative lower norm bound from pointwise disk plus polar alone. -/ +theorem norm_J_seven {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) {q : Multiset ℂ} + (hqcard : q.card = 7 - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) + (hstar : 1 ≤ ∫ t in (0 : ℝ)..1, + (q.map (fun v => ‖(a : ℂ) + (t : ℂ) * (1 - (a : ℂ) ^ 2) * v‖)).prod) : + 1 + (31 / 160 : ℝ) * (1 - a) ≤ + ‖(7 : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ := by + obtain ⟨x, y, hx0, hx1, hx, hsum⟩ := mean_coordinates (by norm_num : 2 ≤ 7) hqcard hq1 + have hpolar := one_le_integral_Ppolar (by norm_num : 2 ≤ 7) hqcard hq1 hx hstar + have hxhalf := polar_mean_gt_half_add_one (Or.inr rfl : 7 = 6 ∨ 7 = 7) ha0 ha1 hx0 hpolar + have hβ := (beta_B_bounds ha0.le ha1.le hxhalf.le hx1 + (by norm_num : (0 : ℝ) ≤ 1) le_rfl).1 + have hl := lower_budget_norm (by norm_num : 2 ≤ 7) ha0.le hqcard hq1 hx hsum hβ + have hg := T_six_gap ha0 ha1 hxhalf.le hx1 + norm_num at hl + have hm : a * (1 + (31 / 160 : ℝ) * (1 - a)) ≤ + a * ‖(7 : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ := by + norm_num + nlinarith only [hl, hg] + exact (mul_le_mul_iff_right₀ ha0).mp hm + +end Sendov.FirstOriginMargins diff --git a/Sendov/Analytic/FirstOriginSmall.lean b/Sendov/Analytic/FirstOriginSmall.lean new file mode 100644 index 0000000..f7170c9 --- /dev/null +++ b/Sendov/Analytic/FirstOriginSmall.lean @@ -0,0 +1,158 @@ +import Sendov.Analytic.FirstOriginBounds + +/-! Actual Fprod and first-origin consumers for n = 6 or n = 7. +All root norm hypotheses are closed (at most one). -/ + +namespace Sendov.FirstOriginSmall + +lemma norm_sum_le_card (q : Multiset ℂ) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) : + ‖q.sum‖ ≤ (q.card : ℝ) := by + refine (norm_multiset_sum_le q).trans ?_ + simpa using Multiset.sum_map_le_sum_map (fun v : ℂ => ‖v‖) (fun _ => (1 : ℝ)) hq1 + +lemma norm_Fprod_le {n : ℕ} (hn : 2 ≤ n) {a x t : ℝ} {q : Multiset ℂ} + (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) + (hx : (q.map (fun v => v.re)).sum = ((n : ℝ) - 1) * x) + (hb : 0 ≤ QQ (a * x) (a ^ 2) t) : + ‖Fprod a q t‖ ≤ QQ (a * x) (a ^ 2) t ^ (((n : ℝ) - 1) / 2) := by + have hc : (q.card : ℝ) = (n : ℝ) - 1 := by + rw [hqcard, Nat.cast_sub (by omega : 1 ≤ n)]; norm_num + have hnR : (2 : ℝ) ≤ n := by exact_mod_cast hn + have hcpos : (0 : ℝ) < q.card := by rw [hc]; linarith + let f : ℂ → ℝ := fun v => ‖1 - (a : ℂ) * (t : ℂ) * v‖ + have hsum := sum_norm_sq_one_sub_le hqcard hq1 (by omega) hx (t := t) (a := a) + have ham := Multiset.prod_le_mean_pow (q.map (fun v => (f v) ^ 2)) (by + intro y hy + obtain ⟨v, _, rfl⟩ := Multiset.mem_map.mp hy + exact sq_nonneg _) + rw [Multiset.card_map, prod_map_sq] at ham + have hmean : (q.map (fun v => (f v) ^ 2)).sum / (q.card : ℝ) ≤ QQ (a * x) (a ^ 2) t := by + rw [div_le_iff₀ hcpos, hc] + simpa only [f, mul_comm] using hsum + have hmean0 : 0 ≤ (q.map (fun v => (f v) ^ 2)).sum / (q.card : ℝ) := by + apply div_nonneg _ hcpos.le + apply Multiset.sum_nonneg + intro y hy + obtain ⟨v, _, rfl⟩ := Multiset.mem_map.mp hy + exact sq_nonneg _ + have hprod := ham.trans (pow_le_pow_left₀ hmean0 hmean q.card) + have heq : (QQ (a * x) (a ^ 2) t ^ (((n : ℝ) - 1) / 2)) ^ 2 = QQ (a * x) (a ^ 2) t ^ q.card := by + rw [← Real.rpow_natCast _ 2, ← Real.rpow_mul hb, ← Real.rpow_natCast _ q.card, hc] + congr 1 + norm_num + have hf : ‖Fprod a q t‖ = (q.map f).prod := norm_prod_map q _ + rw [hf] + apply (sq_le_sq₀ (prod_map_norm_nonneg q _) (Real.rpow_nonneg hb _)).mp + rw [heq] + exact hprod + +lemma norm_integral_Fprod_le_of_first_origin {n : ℕ} (hn : 0 < n) + {a : ℝ} {q z : Multiset ℂ} + (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) (hz1 : ∀ v ∈ z, ‖v‖ ≤ 1) + (hfirst : (n : ℂ) * (∫ t in (0 : ℝ)..1, Fprod a q t) = + (-1) ^ (n - 1) * q.prod * z.prod) : + ‖∫ t in (0 : ℝ)..1, Fprod a q t‖ ≤ 1 / (n : ℝ) := by + have hnR : (0 : ℝ) < n := by exact_mod_cast hn + have hpq : ‖q.prod‖ ≤ 1 := by + rw [norm_multiset_prod] + exact prod_norm_le_one q hq1 + have hpz : ‖z.prod‖ ≤ 1 := by + rw [norm_multiset_prod] + exact prod_norm_le_one z hz1 + have hnorm := congrArg norm hfirst + simp only [norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul, Complex.norm_natCast] at hnorm + rw [le_div_iff₀ hnR] + have hp := mul_le_mul hpq hpz (norm_nonneg _) (by norm_num : (0 : ℝ) ≤ 1) + nlinarith only [hnorm, hp] + +lemma first_origin_polar_six_seven_core + {n : ℕ} (hn : n = 6 ∨ n = 7) {a : ℝ} + (ha0 : 0 < a) (ha1 : a < 1) {q : Multiset ℂ} + (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) + (hstar : 1 ≤ ∫ t in (0 : ℝ)..1, + (q.map (fun v => ‖(a : ℂ) + (t : ℂ) * (1 - (a : ℂ) ^ 2) * v‖)).prod) + (hfirst_bound : ‖∫ t in (0 : ℝ)..1, Sendov.Fprod a q t‖ ≤ 1 / (n : ℝ)) : + False := by + have hn2 : 2 ≤ n := by omega + have hnR : (2 : ℝ) ≤ n := by exact_mod_cast hn2 + have hm0 : 0 < (n : ℝ) - 1 := by linarith + have hmC : (n : ℂ) - 1 ≠ 0 := by + exact_mod_cast (ne_of_gt hm0) + have hc : (q.card : ℝ) = (n : ℝ) - 1 := by + rw [hqcard, Nat.cast_sub (by omega : 1 ≤ n)]; norm_num + let μ : ℂ := q.sum / ((n : ℂ) - 1) + have hsum : q.sum = ((n : ℂ) - 1) * ((μ.re : ℂ) + (μ.im : ℂ) * Complex.I) := by + rw [Complex.re_add_im] + dsimp [μ] + field_simp + have hnc : ‖(n : ℂ) - 1‖ = (n : ℝ) - 1 := by + have he : (n : ℂ) - 1 = (((n : ℝ) - 1 : ℝ) : ℂ) := by push_cast; rfl + rw [he, Complex.norm_real, Real.norm_eq_abs, abs_of_pos hm0] + have hqsum := norm_sum_le_card q hq1 + rw [hc] at hqsum + have hμ : ‖μ‖ ≤ 1 := by + dsimp [μ] + rw [norm_div, hnc, div_le_iff₀ hm0] + simpa using hqsum + have hx0 : -1 ≤ μ.re := by + have h := Complex.abs_re_le_norm μ + exact (abs_le.mp (h.trans hμ)).1 + have hx1 : μ.re ≤ 1 := (Complex.re_le_norm μ).trans hμ + have hx : (q.map (fun v => v.re)).sum = ((n : ℝ) - 1) * μ.re := by + have hre : (q.map (fun v => v.re)).sum = q.sum.re := + (map_multiset_sum Complex.reAddGroupHom q).symm + rw [hre, hsum] + simp + have hpolar := one_le_integral_Ppolar hn2 hqcard hq1 hx hstar + have hxhalf := polar_mean_gt_half_add_one hn ha0 ha1 hx0 hpolar + have hq0 : q ≠ 0 := by + intro h + simp [h] at hqcard + omega + have ht := one_le_tri hn2 hqcard hq0 hq1 ha0.le hx hsum + have hβ := (beta_B_bounds ha0.le ha1.le hxhalf.le hx1 + (by norm_num : (0 : ℝ) ≤ 1) le_rfl).1 + have hf := norm_Fprod_le hn2 hqcard hq1 hx hβ + have hcoef : ((n : ℂ) - 1) * (a : ℂ) * ((μ.re : ℂ) + (μ.im : ℂ) * Complex.I) = (a : ℂ) * q.sum := by + rw [hsum]; ring + rw [hcoef] at ht + have hi : ‖(a : ℂ) * q.sum * (∫ t in (0 : ℝ)..1, Fprod a q t)‖ ≤ + a * ((n : ℝ) - 1) / (n : ℝ) := by + rw [norm_mul, norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos ha0] + have hmul := mul_le_mul (mul_le_mul_of_nonneg_left hqsum ha0.le) hfirst_bound + (norm_nonneg _) (by positivity : 0 ≤ a * ((n : ℝ) - 1)) + simpa only [mul_one_div] using hmul + have htri := norm_add_le (Fprod a q 1) ((a : ℂ) * q.sum * (∫ t in (0 : ℝ)..1, Fprod a q t)) + rcases hn with rfl | rfl + · have hb := direct_budget_five ha0 ha1 hxhalf.le hx1 + norm_num [Real.rpow_natCast] at ht hf hi htri + linarith + · have hb := direct_budget_six ha0 ha1 hxhalf.le hx1 + norm_num [Real.rpow_natCast] at ht hf hi htri + linarith + +theorem first_origin_polar_six_seven + {n : ℕ} (hn : n = 6 ∨ n = 7) {a : ℝ} + (ha0 : 0 < a) (ha1 : a < 1) {q : Multiset ℂ} + (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) + (hstar : 1 ≤ ∫ t in (0 : ℝ)..1, + (q.map (fun v => ‖(a : ℂ) + (t : ℂ) * (1 - (a : ℂ) ^ 2) * v‖)).prod) + (hfirst_bound : ‖∫ t in (0 : ℝ)..1, Sendov.Fprod a q t‖ ≤ 1 / (n : ℝ)) : + False := by + exact first_origin_polar_six_seven_core hn ha0 ha1 hqcard hq1 hstar hfirst_bound + +theorem norm_integral_Fprod_le_of_factorization + {n : ℕ} (hn : 0 < n) {a : ℝ} (ha0 : a ≠ 0) + {c : ℂ} (hc0 : c ≠ 0) {p : Polynomial ℂ} {q z : Multiset ℂ} + (hzcard : z.card = n - 1) (hq0 : ∀ v ∈ q, v ≠ 0) + (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) (hz1 : ∀ v ∈ z, ‖v‖ ≤ 1) + (hpa : p.eval (a : ℂ) = 0) + (hpz : p = Polynomial.C c * ((Polynomial.X - Polynomial.C (a : ℂ)) * (z.map (fun w => Polynomial.X - Polynomial.C w)).prod)) + (hpq : Polynomial.derivative p = Polynomial.C ((n : ℂ) * c) * ((q.map (fun v => (a : ℂ) - v⁻¹)).map + (fun w => Polynomial.X - Polynomial.C w)).prod) : + ‖∫ t in (0 : ℝ)..1, Fprod a q t‖ ≤ 1 / (n : ℝ) := by + apply norm_integral_Fprod_le_of_first_origin hn hq1 hz1 + exact first_origin_identity hc0 (Complex.ofReal_ne_zero.mpr ha0) hzcard hq0 hpa hpz hpq + + +end Sendov.FirstOriginSmall diff --git a/Sendov/Analytic/Jsum.lean b/Sendov/Analytic/Jsum.lean index 8d4c413..14dd792 100644 --- a/Sendov/Analytic/Jsum.lean +++ b/Sendov/Analytic/Jsum.lean @@ -39,58 +39,35 @@ namespace Sendov lemma sum_map_sub (s : Multiset ℂ) (f g : ℂ → ℂ) : (s.map (fun v => f v - g v)).sum = (s.map f).sum - (s.map g).sum := by - induction s using Multiset.induction_on with - | empty => simp - | cons v t ih => - simp only [Multiset.map_cons, Multiset.sum_cons, ih] - ring + exact Multiset.sum_map_sub lemma sum_map_const_sub (s : Multiset ℂ) (c : ℂ) (g : ℂ → ℂ) : (s.map (fun v => c - g v)).sum = (s.card : ℂ) * c - (s.map g).sum := by - induction s using Multiset.induction_on with - | empty => simp - | cons v t ih => - simp only [Multiset.map_cons, Multiset.sum_cons, Multiset.card_cons, ih] - push_cast - ring + rw [sum_map_sub] + simp lemma sum_map_re (s : Multiset ℂ) : (s.map (fun v => v.re)).sum = s.sum.re := by - induction s using Multiset.induction_on with - | empty => simp - | cons v t ih => simp only [Multiset.map_cons, Multiset.sum_cons, Complex.add_re, ih] + exact (map_multiset_sum Complex.reAddGroupHom s).symm lemma norm_sum_map_le (s : Multiset ℂ) (f : ℂ → ℂ) : ‖(s.map f).sum‖ ≤ (s.map (fun w => ‖f w‖)).sum := by - induction s using Multiset.induction_on with - | empty => simp - | cons v t ih => - simp only [Multiset.map_cons, Multiset.sum_cons] - linarith [norm_add_le (f v) ((t.map f).sum), ih] + simpa only [Multiset.map_map, Function.comp_def] using norm_multiset_sum_le (s.map f) lemma norm_prod_le_one : ∀ (s : Multiset ℂ), (∀ w ∈ s, ‖w‖ ≤ 1) → ‖s.prod‖ ≤ 1 := by - intro s - induction s using Multiset.induction_on with - | empty => intro _; simp - | cons v t ih => - intro hs - have hv := hs v (Multiset.mem_cons_self v t) - have ht : ∀ u ∈ t, ‖u‖ ≤ 1 := fun u hu => hs u (Multiset.mem_cons_of_mem hu) - rw [Multiset.prod_cons, norm_mul] - nlinarith [ih ht, norm_nonneg v, norm_nonneg t.prod] + intro s hs + rw [norm_multiset_prod] + exact prod_norm_le_one s hs /-- `(∏ s) ∑ⱼ 1/sⱼ = ∑ⱼ ∏_{k≠j} sₖ`, the clearing of denominators that is valid exactly when no `sⱼ` vanishes. -/ lemma prod_mul_sum_inv : ∀ (s : Multiset ℂ), (∀ w ∈ s, w ≠ 0) → s.prod * (s.map (fun w => w⁻¹)).sum = sumEraseProd s := by - intro s - induction s using Multiset.induction_on with - | empty => simp [sumEraseProd] - | cons v t ih => - intro hs - have hv := hs v (Multiset.mem_cons_self v t) - have ht : ∀ u ∈ t, u ≠ 0 := fun u hu => hs u (Multiset.mem_cons_of_mem hu) - rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, sumEraseProd_cons, ← ih ht] - field_simp + classical + intro s hs + rw [sumEraseProd, ← Multiset.sum_map_mul_left] + refine congrArg Multiset.sum (Multiset.map_congr rfl ?_) + intro w hw + rw [← Multiset.prod_erase hw, mul_right_comm, mul_inv_cancel₀ (hs w hw), one_mul] /-- The degenerate case. If `∏ sⱼ = 0` then some `sⱼ` vanishes, so at most one term of `∑ⱼ ∏_{k≠j} sₖ` is nonzero — and that term is a product of points of the closed unit disk. -/ @@ -106,12 +83,10 @@ lemma sumEraseProd_norm_le_one : ∀ (s : Multiset ℂ), (∀ w ∈ s, ‖w‖ rw [sumEraseProd_cons] rcases eq_or_ne t.prod 0 with ht0 | ht0 · rw [ht0, zero_add, norm_mul] - nlinarith [ih ht ht0, norm_nonneg v, norm_nonneg (sumEraseProd t), hv] + exact mul_le_one₀ hv (norm_nonneg _) (ih ht ht0) · have hv0 : v = 0 := by rw [Multiset.prod_cons] at hp - rcases mul_eq_zero.1 hp with h | h - · exact h - · exact absurd h ht0 + exact (mul_eq_zero.1 hp).resolve_right ht0 rw [hv0, zero_mul, add_zero] exact norm_prod_le_one t ht @@ -137,7 +112,7 @@ theorem Jsum_estimate {n : ℕ} (hn : 2 ≤ n) {a x y : ℝ} {z q : Multiset ℂ · -- degenerate: `J = 0`, and `sumEraseProd z` has at most one surviving term rw [hz0, mul_zero, mul_zero, sub_zero, norm_zero, mul_zero, norm_mul] have h2 : ‖sumEraseProd z‖ ≤ 1 := sumEraseProd_norm_le_one z hz1 hz0 - nlinarith [norm_nonneg q.prod, norm_nonneg (sumEraseProd z)] + simpa using (mul_le_one₀ hqpnorm (norm_nonneg _) h2).trans hratio · -- the main case: every `zⱼ` is nonzero, so denominators may be cleared have hzne : ∀ w ∈ z, w ≠ 0 := by intro w hw hw0 diff --git a/Sendov/Analytic/LowDegree.lean b/Sendov/Analytic/LowDegree.lean index 3cfd2f2..6d566d5 100644 --- a/Sendov/Analytic/LowDegree.lean +++ b/Sendov/Analytic/LowDegree.lean @@ -65,29 +65,18 @@ lemma norm_le_lowX {a t : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (ht0 : 0 ≤ t) { refine (norm_add_le _ _).trans ?_ rw [norm_mul, Complex.norm_real, Complex.norm_real, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg ha0, abs_of_nonneg (mul_nonneg ht0 hb)] - simp only [lowX] - nlinarith [hv, norm_nonneg v, mul_nonneg ht0 hb] + simpa only [lowX, mul_comm t] using + add_le_add_right (mul_le_of_le_one_right (mul_nonneg ht0 hb) hv) a lemma prod_norm_le_lowX_pow {a t : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (ht0 : 0 ≤ t) : ∀ (q : Multiset ℂ), (∀ v ∈ q, ‖v‖ ≤ 1) → (q.map (fun v => ‖(a : ℂ) + (t : ℂ) * (1 - (a : ℂ) ^ 2) * v‖)).prod ≤ lowX a t ^ q.card := by - intro q - induction q using Multiset.induction_on with - | empty => intro _; simp - | cons v s ih => - intro hq - have hv := hq v (Multiset.mem_cons_self v s) - have hs : ∀ u ∈ s, ‖u‖ ≤ 1 := fun u hu => hq u (Multiset.mem_cons_of_mem hu) - have hX0 : 0 ≤ lowX a t := lowX_nonneg ha0 ha1 ht0 - have h3 : 0 ≤ (s.map (fun v => ‖(a : ℂ) + (t : ℂ) * (1 - (a : ℂ) ^ 2) * v‖)).prod := - prod_map_norm_nonneg s _ - simp only [Multiset.map_cons, Multiset.prod_cons, Multiset.card_cons, pow_succ] - calc ‖(a : ℂ) + (t : ℂ) * (1 - (a : ℂ) ^ 2) * v‖ - * (s.map (fun v => ‖(a : ℂ) + (t : ℂ) * (1 - (a : ℂ) ^ 2) * v‖)).prod - ≤ lowX a t * lowX a t ^ s.card := - mul_le_mul (norm_le_lowX ha0 ha1 ht0 hv) (ih hs) h3 hX0 - _ = lowX a t ^ s.card * lowX a t := by ring + intro q hq + simpa using Multiset.prod_map_le_prod_map₀ + (fun v : ℂ => ‖(a : ℂ) + (t : ℂ) * (1 - (a : ℂ) ^ 2) * v‖) + (fun _ => lowX a t) (fun _ _ => norm_nonneg _) + (fun v hv => norm_le_lowX ha0 ha1 ht0 (hq v hv)) /-- The branch point `(⋆)`, with every factor replaced by the scalar `X(t)`. -/ theorem one_le_lowJ {n : ℕ} {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) diff --git a/Sendov/Analytic/Maclaurin.lean b/Sendov/Analytic/Maclaurin.lean index eb9177b..f684caa 100644 --- a/Sendov/Analytic/Maclaurin.lean +++ b/Sendov/Analytic/Maclaurin.lean @@ -152,15 +152,10 @@ lemma esymm_card_cons (a : ℝ) (t : Multiset ℝ) (ht : t ≠ 0) : omega⟩ rw [hm] simp only [Multiset.esymm, Multiset.powersetCard_cons, Multiset.map_add, Multiset.sum_add, - Multiset.map_map, Nat.add_sub_cancel] - congr 1 - · rw [← hm, Multiset.powersetCard_self] - simp - · rw [← Multiset.sum_map_mul_left] - congr 1 - apply Multiset.map_congr rfl - intro u _ - simp + Multiset.map_map, Nat.add_sub_cancel, Function.comp_def, Multiset.prod_cons, + Multiset.sum_map_mul_left] + rw [← hm, Multiset.powersetCard_self] + simp /-- **Maclaurin's inequality, top case.** `e_{N-1}(s) ≤ N (mean s)^{N-1}`. -/ theorem Multiset.esymm_card_pred_le : ∀ (s : Multiset ℝ), (∀ x ∈ s, 0 ≤ x) → s ≠ 0 → @@ -213,9 +208,7 @@ theorem Multiset.esymm_card_pred_le : ∀ (s : Multiset ℝ), (∀ x ∈ s, 0 · have hstep := maclaurin_step (a := a) t.card hc hupos ha calc t.prod + a * t.esymm (t.card - 1) ≤ u ^ t.card + a * ((t.card : ℝ) * u ^ (t.card - 1)) := by - have h2 : a * t.esymm (t.card - 1) ≤ a * ((t.card : ℝ) * u ^ (t.card - 1)) := - mul_le_mul_of_nonneg_left hIH ha - linarith [hamgm] + exact add_le_add hamgm (mul_le_mul_of_nonneg_left hIH ha) _ = u ^ t.card + (t.card : ℝ) * a * u ^ (t.card - 1) := by ring _ ≤ ((t.card : ℝ) + 1) * ((a + t.card * u) / (t.card + 1)) ^ t.card := hstep _ = ((t.card : ℝ) + 1) * ((a + t.sum) / ((t.card : ℝ) + 1)) ^ t.card := by rw [hsum] diff --git a/Sendov/Analytic/Origin.lean b/Sendov/Analytic/Origin.lean index 5e22114..f06d372 100644 --- a/Sendov/Analytic/Origin.lean +++ b/Sendov/Analytic/Origin.lean @@ -89,22 +89,13 @@ theorem sumEraseProdMap_eq_esymm {α : Type*} : ∀ (s : Multiset α) (f : α /-- `‖1 + s v‖² = 1 + 2 s Re v + s² ‖v‖²` for real `s`. -/ lemma norm_sq_one_add_real_mul (s : ℝ) (v : ℂ) : ‖1 + (s : ℂ) * v‖ ^ 2 = 1 + 2 * s * v.re + s ^ 2 * ‖v‖ ^ 2 := by - rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq] - simp only [Complex.normSq_apply, Complex.add_re, Complex.add_im, Complex.mul_re, - Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, Complex.one_re, Complex.one_im] - ring + simpa using norm_sq_add_real_mul 1 s v lemma sum_norm_sq_one_sub_split (s : ℝ) (q : Multiset ℂ) : (q.map (fun v => ‖1 + (s : ℂ) * v‖ ^ 2)).sum = (q.card : ℝ) + 2 * s * ((q.map (fun v => v.re)).sum) + s ^ 2 * ((q.map (fun v => ‖v‖ ^ 2)).sum) := by - induction q using Multiset.induction_on with - | empty => simp - | cons v t ih => - simp only [Multiset.map_cons, Multiset.sum_cons, Multiset.card_cons] - rw [ih, norm_sq_one_add_real_mul] - push_cast - ring + simpa using sum_norm_sq_split 1 s q /-- `∑ⱼ ‖1 - a t qⱼ‖² ≤ (n-1) β(t)`, where `β(t) = 1 - 2 a x t + a² t²`. -/ theorem sum_norm_sq_one_sub_le {n : ℕ} {a x t : ℝ} {q : Multiset ℂ} @@ -131,26 +122,13 @@ theorem sum_norm_sq_one_sub_le {n : ℕ} {a x t : ℝ} {q : Multiset ℂ} lemma sq_sum_le_card_mul_sum_sq (s : Multiset ℝ) (hs : ∀ b ∈ s, 0 ≤ b) : (s.sum) ^ 2 ≤ (s.card : ℝ) * (s.map (fun b => b ^ 2)).sum := by - induction s using Multiset.induction_on with - | empty => simp - | cons b t ih => - have hb := hs b (Multiset.mem_cons_self b t) - have ht : ∀ u ∈ t, 0 ≤ u := fun u hu => hs u (Multiset.mem_cons_of_mem hu) - rcases eq_or_ne t 0 with rfl | ht0 - · simp - · have hIH := ih ht - have hcard : (0 : ℝ) < (t.card : ℕ) := by - have := Multiset.card_pos.2 ht0 - exact_mod_cast this - have hsum : 0 ≤ t.sum := Multiset.sum_nonneg ht - have hQ : (0 : ℝ) ≤ (t.map (fun b => b ^ 2)).sum := - Multiset.sum_nonneg (by - intro y hy - obtain ⟨u, _, rfl⟩ := Multiset.mem_map.1 hy - exact sq_nonneg u) - simp only [Multiset.sum_cons, Multiset.card_cons, Multiset.map_cons] - push_cast - nlinarith [hIH, sq_nonneg (t.sum - (t.card : ℝ) * b), hcard, hsum, hb, hQ] + -- Apply Cauchy–Schwarz with f = 1 and g = l.get on list positions, preserving repeats. + -- The original nonnegativity hypothesis hs is retained for interface compatibility. + induction s using Quotient.inductionOn with + | h l => + have h := Finset.sum_mul_sq_le_sq_mul_sq Finset.univ + (fun _ : Fin l.length => (1 : ℝ)) l.get + simpa [← List.sum_ofFn, List.ofFn_getElem_eq_map l (fun b : ℝ => b ^ 2)] using h /-- **The error bound.** `∑ⱼ ∏_{k≠j} ‖1 - a t q_k‖ ≤ (n-1) β(t)^{(n-2)/2}`: Maclaurin's inequality, then Cauchy–Schwarz, then the quadratic mean. Nonnegativity of `β(t)` is not @@ -259,18 +237,16 @@ lemma sumEraseProdC_cons (v : ℂ) (t : Multiset ℂ) (g f : ℂ → ℂ) : /-- A weighted erasure sum with unit-size weights is dominated by the unweighted one. -/ lemma norm_sumEraseProdC_le (g f : ℂ → ℂ) : ∀ (s : Multiset ℂ), (∀ v ∈ s, ‖g v‖ ≤ 1) → ‖sumEraseProdC s g f‖ ≤ sumEraseProdMap s (fun v => ‖f v‖) := by - intro s - induction s using Multiset.induction_on with - | empty => intro _; simp [sumEraseProdMap] - | cons v t ih => - intro hg - have hv := hg v (Multiset.mem_cons_self v t) - have ht : ∀ u ∈ t, ‖g u‖ ≤ 1 := fun u hu => hg u (Multiset.mem_cons_of_mem hu) - rw [sumEraseProdC_cons, sumEraseProdMap_cons] - refine (norm_add_le _ _).trans ?_ - rw [norm_mul, norm_mul, norm_prod_map] - have h2 : (0 : ℝ) ≤ (t.map (fun v => ‖f v‖)).prod := prod_map_norm_nonneg t f - nlinarith [ih ht, norm_nonneg (f v), norm_nonneg (sumEraseProdC t g f), h2, hv] + classical + intro s hg + unfold sumEraseProdC sumEraseProdMap + refine (norm_multiset_sum_le _).trans ?_ + rw [Multiset.map_map] + refine Multiset.sum_map_le_sum_map _ _ ?_ + intro v hv + dsimp only [Function.comp_def] + rw [norm_mul, norm_prod_map] + exact mul_le_of_le_one_left (prod_map_norm_nonneg _ _) (hg v hv) /-- `F(t) = ∏ⱼ (1 - a t qⱼ)`. -/ noncomputable def Fprod (a : ℝ) (q : Multiset ℂ) (t : ℝ) : ℂ := @@ -303,27 +279,20 @@ lemma hasDerivAt_Fprod (a t : ℝ) : ∀ (q : Multiset ℂ), induction q using Multiset.induction_on with | empty => have he : Fprod a 0 = fun _ : ℝ => (1 : ℂ) := by funext s; simp [Fprod] - have hz : -(a : ℂ) * sumEraseProdC 0 id (fun v => 1 - (a : ℂ) * (t : ℂ) * v) = 0 := by simp - rw [he, hz] + rw [he, sumEraseProdC_zero, mul_zero] exact hasDerivAt_const t 1 | cons v r ih => have h0 : HasDerivAt (fun s : ℝ => (s : ℂ)) 1 t := Complex.ofRealCLM.hasDerivAt have h1 : HasDerivAt (fun s : ℝ => 1 - (a : ℂ) * (s : ℂ) * v) (-((a : ℂ) * v)) t := by simpa using ((h0.const_mul (a : ℂ)).mul_const v).const_sub 1 - have h2 := h1.mul ih have hfun : Fprod a (v ::ₘ r) = fun s : ℝ => (1 - (a : ℂ) * (s : ℂ) * v) * Fprod a r s := by funext s simp only [Fprod, Multiset.map_cons, Multiset.prod_cons] - have hderiv : -(a : ℂ) * ((v : ℂ) * (r.map (fun w => 1 - (a : ℂ) * (t : ℂ) * w)).prod - + (1 - (a : ℂ) * (t : ℂ) * v) * sumEraseProdC r id (fun w => 1 - (a : ℂ) * (t : ℂ) * w)) - = -((a : ℂ) * v) * Fprod a r t - + (1 - (a : ℂ) * (t : ℂ) * v) - * (-(a : ℂ) * sumEraseProdC r id (fun w => 1 - (a : ℂ) * (t : ℂ) * w)) := by - simp only [Fprod] - ring - rw [hfun, sumEraseProdC_cons, id_eq, hderiv] - exact h2 + rw [hfun, sumEraseProdC_cons, id_eq] + apply (h1.mul ih).congr_deriv + simp only [Fprod] + ring /-- **The pointwise estimate.** `‖F'(t) + (n-1) a (x+iy) F(t)‖ ≤ a² t (n-1) β(t)^{(n-2)/2}`. -/ theorem norm_deriv_add_le {n : ℕ} (hn : 2 ≤ n) {a x y t : ℝ} {q : Multiset ℂ} diff --git a/Sendov/Analytic/OriginExact.lean b/Sendov/Analytic/OriginExact.lean index 63fb6f4..c152646 100644 --- a/Sendov/Analytic/OriginExact.lean +++ b/Sendov/Analytic/OriginExact.lean @@ -42,25 +42,17 @@ open Complex (I) lemma sum_norm_le_card : ∀ (q : Multiset ℂ), (∀ v ∈ q, ‖v‖ ≤ 1) → (q.map (fun v => ‖v‖)).sum ≤ (q.card : ℝ) := by - intro q - induction q using Multiset.induction_on with - | empty => intro _; simp - | cons v t ih => - intro hq - have hv := hq v (Multiset.mem_cons_self v t) - have ht : ∀ u ∈ t, ‖u‖ ≤ 1 := fun u hu => hq u (Multiset.mem_cons_of_mem hu) - simp only [Multiset.map_cons, Multiset.sum_cons, Multiset.card_cons] - push_cast - linarith [ih ht] + intro q hq + simpa using Multiset.sum_map_le_sum_map (fun v : ℂ => ‖v‖) (fun _ => (1 : ℝ)) hq /-- `|s + it| ≤ s + t²/(2s)` for `s > 0`, in cleared form. Squaring both sides leaves -`t⁴ ≥ 0`. -/ +`t⁴ ≥ 0`; directly, the cleared inequality is `(‖w‖ - w.re)² ≥ 0`. -/ lemma norm_mul_two_re_le {w : ℂ} (_hs : 0 < w.re) : ‖w‖ * (2 * w.re) ≤ 2 * w.re ^ 2 + w.im ^ 2 := by have h1 : ‖w‖ ^ 2 = w.re ^ 2 + w.im ^ 2 := by rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply] ring - nlinarith [norm_nonneg w, h1, sq_nonneg (w.im ^ 2), sq_nonneg (w.re * w.im)] + nlinarith only [h1, sq_nonneg (‖w‖ - w.re)] /-! ### The quantity `W`, the growth bound `(grow)`, and the two real-arithmetic steps -/ @@ -77,14 +69,13 @@ lemma Worigin_eq (n : ℕ) (a x y : ℝ) : lemma Worigin_re (n : ℕ) (a x y : ℝ) : (Worigin n a x y).re = a ^ 2 * ((n : ℝ) - 1) + 1 - a * x := by - rw [Worigin_eq, Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.ofReal_re, - Complex.ofReal_im, Complex.I_re, Complex.I_im] - ring + rw [Worigin_eq] + simp only [Complex.add_re, Complex.ofReal_re, Complex.mul_I_re, Complex.ofReal_im, + neg_zero, add_zero] lemma Worigin_im (n : ℕ) (a x y : ℝ) : (Worigin n a x y).im = -(a * y) := by - rw [Worigin_eq, Complex.add_im, Complex.ofReal_im, Complex.mul_im, Complex.ofReal_re, - Complex.ofReal_im, Complex.I_re, Complex.I_im] - ring + rw [Worigin_eq] + simp only [Complex.add_im, Complex.ofReal_im, Complex.mul_I_im, Complex.ofReal_re, zero_add] /-- **(grow).** `‖W‖ ≥ 2an/(n-1)`. Bounding `‖W‖` below by its real part reduces this to `(n-1)²a² - (3n-1)a + (n-1) > 0`; completing the square turns that into @@ -135,7 +126,7 @@ lemma norm_Worigin_le {n : ℕ} {a x y : ℝ} (ha0 : 0 < a) (ha1 : a < 1) ≤ (1 - x ^ 2) / (2 * ((n : ℝ) - 1)) := by rw [div_le_div_iff₀ hs hden] nlinarith [hy2, hslow, ha2, sq_nonneg y, hn1] - linarith [hmain, htail] + exact hmain.trans (add_le_add_right htail _) /-- `x` and `y` are determined by `q.sum`, and inherit two bounds from `‖qⱼ‖ ≤ 1`: the real part is what the polar and origin estimates need, and `x² + y² ≤ 1` is what eliminates `y`. -/ @@ -160,17 +151,13 @@ lemma xy_bounds {n : ℕ} (hn : 2 ≤ n) {x y : ℝ} {q : Multiset ℂ} simp · have hxynorm : ‖(x : ℂ) + (y : ℂ) * I‖ ^ 2 = x ^ 2 + y ^ 2 := by rw [← Complex.normSq_eq_norm_sq, Complex.normSq_add_mul_I] - have h2 : ‖q.sum‖ ≤ (q.map (fun v => ‖v‖)).sum := by - have h := norm_sum_map_le q (fun v => v) - simpa using h + have h2 : ‖q.sum‖ ≤ (q.map (fun v => ‖v‖)).sum := norm_multiset_sum_le q have h3 := sum_norm_le_card q hq1 rw [hqcardR] at h3 have h1 : ‖q.sum‖ ≤ (n : ℝ) - 1 := h2.trans h3 rw [hxy, norm_mul, hnc] at h1 - have h4 : ‖(x : ℂ) + (y : ℂ) * I‖ ≤ 1 := by - by_contra hcon - rw [not_le] at hcon - nlinarith [h1, hn1] + have h4 : ‖(x : ℂ) + (y : ℂ) * I‖ ≤ 1 := + (mul_le_mul_iff_right₀ hn1).mp (by simpa only [mul_one] using h1) nlinarith [hxynorm, h4, norm_nonneg ((x : ℂ) + (y : ℂ) * I)] /-! ### The origin inequality -/ @@ -219,9 +206,7 @@ theorem origin_exact {n : ℕ} (hn : 5 ≤ n) {a x y α : ℝ} {z q : Multiset rw [Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg (le_of_lt ha0)] have hPJ0 : (0 : ℝ) ≤ ‖q.prod‖ * ‖z.prod‖ := by positivity have hPJ1 : ‖q.prod‖ * ‖z.prod‖ ≤ 1 := by - have h1 : ‖q.prod‖ ≤ 1 := norm_prod_le_one q hq1 - have h2 : ‖z.prod‖ ≤ 1 := norm_prod_le_one z hz1 - nlinarith [norm_nonneg q.prod, norm_nonneg z.prod] + exact mul_le_one₀ (norm_prod_le_one q hq1) (norm_nonneg _) (norm_prod_le_one z hz1) have hstep1 : (n : ℝ) * ‖Fprod a q 1 + ((n : ℂ) - 1) * (a : ℂ) * ((x : ℂ) + (y : ℂ) * I) * ∫ t in (0 : ℝ)..1, Fprod a q t‖ ≤ ‖q.prod‖ * ‖z.prod‖ * ‖Worigin n a x y‖ diff --git a/Sendov/Analytic/PaperBulkAlgebra.lean b/Sendov/Analytic/PaperBulkAlgebra.lean new file mode 100644 index 0000000..02f4210 --- /dev/null +++ b/Sendov/Analytic/PaperBulkAlgebra.lean @@ -0,0 +1,90 @@ +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring +import Mathlib.Data.Real.Basic + +/-! +# Parameter-preserving bulk budget + +The algebraic middle-region argument of first-origin-uniform/round5, §4. +These lemmas close the scalar budget from the stated integral estimate; +they do not assert that estimate or claim the complete uniform D theorem. +-/ + +namespace Sendov.PaperBulk + +/-- The middle-region cubic has an explicit positive decomposition. -/ +theorem middle_cubic_pos {a : ℝ} (ha : 1 / 3 ≤ a) (hb : a ≤ 4 / 5) : + 0 < 256 * a ^ 2 * (1 - a) - 24 * a ^ 2 - 16 := by + have h₁ : 0 ≤ (a - 1 / 3) * (536 / 225) := by positivity + have h₂ : 0 ≤ (a - 1 / 3) * (4 / 5 - a) * (256 * a + 872 / 15) := by + positivity + have hid : 256 * a ^ 2 * (1 - a) - 24 * a ^ 2 - 16 = + 8 / 27 + (a - 1 / 3) * (536 / 225) + + (a - 1 / 3) * (4 / 5 - a) * (256 * a + 872 / 15) := by ring + rw [hid] + linarith + +/-- All real m ≥ 256 satisfy the retained-a budget on the middle interval. -/ +theorem middle_budget {m a : ℝ} (hm : 256 ≤ m) + (ha : 1 / 3 ≤ a) (hb : a ≤ 4 / 5) : + 16 / (m * a ^ 2) + 24 / m < 1 - a := by + have hm0 : 0 < m := by linarith + have ha0 : 0 < a := by linarith + have hh : 0 ≤ 1 - a := by linarith + have hc := middle_cubic_pos ha hb + have hmul : 0 ≤ (m - 256) * a ^ 2 * (1 - a) := by positivity + have hp : 16 + 24 * a ^ 2 < (1 - a) * (m * a ^ 2) := by nlinarith + have hd : 0 < m * a ^ 2 := by positivity + calc + 16 / (m * a ^ 2) + 24 / m = (16 + 24 * a ^ 2) / (m * a ^ 2) := by + field_simp + _ < 1 - a := (div_lt_iff₀ hd).2 hp + +/-- A consumer of the analytic estimate, with strictness unchanged. -/ +theorem direct_budget_middle {m a T : ℝ} (hm : 256 ≤ m) + (ha : 1 / 3 ≤ a) (hb : a ≤ 4 / 5) + (hT : T < 16 / (m * a ^ 2) + 24 / m) : + T < 1 - m * a / (m + 1) := by + have hm0 : 0 < m + 1 := by linarith + have ha0 : 0 < a := by linarith + have hp : 0 < a / (m + 1) := div_pos ha0 hm0 + have he : 1 - m * a / (m + 1) = 1 - a + a / (m + 1) := by + field_simp + ring + rw [he] + have ht := hT.trans (middle_budget hm ha hb) + linarith + +/-- The same retained-a estimate closes the large-a, large-ray region. -/ +theorem large_ray_budget {m a : ℝ} (hm : 0 < m) (ha : 4 / 5 ≤ a) + (hscale : 49 ≤ m * (1 - a)) : + 16 / (m * a ^ 2) + 24 / m ≤ 1 - a := by + have ha0 : 0 < a := by linarith + have ha2 : (4 / 5 : ℝ) ^ 2 ≤ a ^ 2 := by nlinarith + have hd : 0 < m * a ^ 2 := by positivity + have hfirst : 16 / (m * a ^ 2) ≤ 25 / m := by + apply (div_le_iff₀ hd).2 + have he : 25 / m * (m * a ^ 2) = 25 * a ^ 2 := by field_simp + rw [he] + nlinarith + have hlast : 49 / m ≤ 1 - a := (div_le_iff₀ hm).2 (by nlinarith [hscale]) + calc + 16 / (m * a ^ 2) + 24 / m ≤ 25 / m + 24 / m := by linarith + _ = 49 / m := by ring + _ ≤ 1 - a := hlast + +/-- Small-a closure of the global two-thirds bound. -/ +theorem direct_budget_small {m a T : ℝ} (hm : 0 ≤ m) + (ha : 0 < a) (hb : a ≤ 1 / 3) (hT : T < 2 / 3) : + T < 1 - m * a / (m + 1) := by + have hd : 0 < m + 1 := by linarith + have he : 1 - m * a / (m + 1) = 1 - a + a / (m + 1) := by + field_simp + ring + have hp := div_pos ha hd + rw [he] + linarith + +end Sendov.PaperBulk diff --git a/Sendov/Analytic/PaperCentered.lean b/Sendov/Analytic/PaperCentered.lean new file mode 100644 index 0000000..75c413b --- /dev/null +++ b/Sendov/Analytic/PaperCentered.lean @@ -0,0 +1,362 @@ +import Sendov.Counterexample.Identities +import Mathlib.RingTheory.Polynomial.Vieta + +/-! # Finite centered expansion +All endpoints are finite complex polynomials; no reality or positivity of the mean is used. +-/ +noncomputable section +open scoped BigOperators +open Polynomial +namespace Sendov.PaperCentered + +/-- The finite endpoint sum in the paper. -/ +def B (m k : ℕ) (z : ℂ) : ℂ := + ∑ j ∈ Finset.range (k + 1), (m + 1).choose j * z ^ j * (1 - z) ^ (m + 1 - j) + +/-- The complementary endpoint, retained at every degree. -/ +def H (m k : ℕ) (z : ℂ) : ℂ := 1 - B m k z + +@[simp] theorem B_zero (m : ℕ) (z : ℂ) : B m 0 z = (1 - z) ^ (m + 1) := by + simp [B] + +theorem H_succ (m k : ℕ) (z : ℂ) : + H m (k + 1) z = H m k z - + (m + 1).choose (k + 1) * z ^ (k + 1) * (1 - z) ^ (m - k) := by + simp only [H, B, Finset.sum_range_succ] + rw [show m + 1 - (k + 1) = m - k by omega] + ring + +/-- Homogeneous Vieta identity, including repeated values and zero scaling. -/ +theorem prod_affine (r : Multiset ℂ) (x y : ℂ) : + (r.map (fun v => x + y * v)).prod = + ∑ k ∈ Finset.range (r.card + 1), y ^ k * r.esymm k * x ^ (r.card - k) := by + have h := congrArg (Polynomial.eval x) + (Multiset.prod_X_add_C_eq_sum_esymm (r.map (fun v => y * v))) + have hs (k : ℕ) : (r.map (fun v => y * v)).esymm k = y ^ k * r.esymm k := by + exact (Multiset.pow_smul_esymm y k r).symm + simpa only [eval_multiset_prod, Multiset.map_map, Function.comp_def, eval_add, + eval_X, eval_C, eval_finsetSum, eval_mul, eval_pow, Multiset.card_map, hs] using h + +/-- The actual centered product expansion, before integration. -/ +theorem centered_product (q : Multiset ℂ) (a μ : ℂ) (t : ℝ) : + (q.map (fun v => 1 - a * t * v)).prod = + ∑ k ∈ Finset.range (q.card + 1), (-a) ^ k * + (q.map (fun v => v - μ)).esymm k * (t : ℂ) ^ k * + (1 - a * μ * t) ^ (q.card - k) := by + have h := prod_affine (q.map (fun v => v - μ)) (1 - a * μ * t) (-a * t) + simp only [Multiset.map_map, Function.comp_def, Multiset.card_map, mul_pow] at h + convert h using 1 + · congr 2; ext v; ring + · apply Finset.sum_congr rfl + intro k hk + ring + +@[simp] theorem esymm_zero (r : Multiset ℂ) : r.esymm 0 = 1 := by + simp [Multiset.esymm] + +@[simp] theorem esymm_one (r : Multiset ℂ) : r.esymm 1 = r.sum := by + simp [Multiset.esymm, Multiset.powersetCard_one] + +/-- Elementary symmetric recursion, without distinctness assumptions. -/ +theorem esymm_cons (v : ℂ) (r : Multiset ℂ) (k : ℕ) : + (v ::ₘ r).esymm (k + 1) = r.esymm (k + 1) + v * r.esymm k := by + simp only [Multiset.esymm, Multiset.powersetCard_cons, Multiset.map_add, + Multiset.sum_add, Multiset.map_map, Function.comp_def, Multiset.prod_cons] + rw [Multiset.sum_map_mul_left] + +/-- Degree two Newton identity proved directly from the multiset recursion. -/ +theorem two_mul_esymm_two (r : Multiset ℂ) : + 2 * r.esymm 2 = r.sum ^ 2 - (r.map (fun v => v ^ 2)).sum := by + induction r using Multiset.induction_on with + | empty => simp [Multiset.esymm, show 2 = 1 + 1 from rfl, Multiset.powersetCard_zero_right] + | cons v r ih => + rw [show 2 = 1 + 1 from rfl, esymm_cons, esymm_one] + simp only [Multiset.sum_cons, Multiset.map_cons] + linear_combination ih + +/-- Centering really kills the linear coefficient. -/ +theorem centered_sum (q : Multiset ℂ) (μ : ℂ) (hμ : q.sum = q.card * μ) : + (q.map (fun v => v - μ)).sum = 0 := by + have hc : (q.map (fun _ => μ)).sum = (q.card : ℂ) * μ := by + induction q using Multiset.induction_on with + | empty => simp + | cons v q ih => simp [Nat.cast_add, add_mul]; ring + simp only [Multiset.sum_map_sub, Multiset.map_id', hc, hμ, sub_self] + +/-- Differentiating the finite endpoint sum telescopes exactly. -/ +theorem hasDerivAt_H (m k : ℕ) (hk : k ≤ m) (z : ℂ) : + HasDerivAt (H m k) ((m + 1) * (m.choose k : ℂ) * z ^ k * (1 - z) ^ (m - k)) z := by + induction k with + | zero => + have he : H m 0 = fun w => 1 - (1 - w) ^ (m + 1) := by + funext w; simp [H] + rw [he] + simpa using + (((hasDerivAt_id z).const_sub 1).pow (m + 1)).const_sub 1 + | succ k ih => + have hk' : k ≤ m := by omega + have hmk : m - k = (m - (k + 1)) + 1 := by omega + have hc₁ : ((m + 1 : ℕ) : ℂ) * m.choose k = + ((m + 1).choose (k + 1) : ℂ) * (k + 1) := by + exact_mod_cast Nat.add_one_mul_choose_eq m k + have hc₂ : (m.choose (k + 1) : ℂ) * (m + 1) = + ((m + 1).choose (k + 1) : ℂ) * (m - k) := by + have h := Nat.choose_mul_succ_eq m (k + 1) + rw [show m + 1 - (k + 1) = m - k by omega] at h + exact_mod_cast h + have hd := (ih hk').sub + ((((hasDerivAt_id z).pow (k + 1)).const_mul + ((m + 1).choose (k + 1) : ℂ)).mul + (((hasDerivAt_id z).const_sub 1).pow (m - k))) + have he : H m (k + 1) = fun w => H m k w - + (m + 1).choose (k + 1) * w ^ (k + 1) * (1 - w) ^ (m - k) := + funext (H_succ m k) + rw [he] + convert hd using 1 <;> try rfl + simp only [Pi.pow_apply, id_eq, Nat.cast_add, Nat.cast_one, + Nat.add_sub_cancel, mul_one, mul_neg, hmk, pow_succ] + have hc₃ : ((m - (k + 1) : ℕ) : ℂ) + 1 = (m : ℂ) - k := by + simpa only [Nat.cast_add, Nat.cast_one, Nat.cast_sub hk'] using + congrArg (Nat.cast : ℕ → ℂ) hmk.symm + rw [hc₃] + push_cast at hc₁ + linear_combination -(z ^ k * (1 - z) ^ (m - (k + 1)) * (1 - z)) * hc₁ + + (z ^ k * z * (1 - z) ^ (m - (k + 1))) * hc₂ + +@[simp] theorem H_at_zero (m k : ℕ) : H m k 0 = 0 := by + rw [H, B, Finset.sum_eq_single 0] + · simp + · intro j hj hj0 + simp [zero_pow hj0] + · simp + +/-- Integer incomplete-beta identity, division-free and valid for every complex z, +including z=0 and the top index k=m. -/ +theorem finite_beta (m k : ℕ) (hk : k ≤ m) (z : ℂ) : + ((m + 1) * (m.choose k : ℂ) * z ^ (k + 1)) * + (∫ t in (0 : ℝ)..1, (t : ℂ) ^ k * (1 - z * t) ^ (m - k)) = H m k z := by + have hd (t : ℝ) : HasDerivAt (fun t : ℝ => H m k (z * t)) + (((m + 1) * (m.choose k : ℂ) * z ^ (k + 1)) * + ((t : ℂ) ^ k * (1 - z * t) ^ (m - k))) t := by + have ht : HasDerivAt (fun t : ℝ => z * (t : ℂ)) z t := by + simpa using (Complex.ofRealCLM.hasDerivAt (x := t)).const_mul z + convert (hasDerivAt_H m k hk (z * t)).scomp t ht using 1 <;> try rfl + simp only [smul_eq_mul, mul_pow, pow_succ] + ring + have hi : IntervalIntegrable (fun t : ℝ => + ((m + 1) * (m.choose k : ℂ) * z ^ (k + 1)) * + ((t : ℂ) ^ k * (1 - z * t) ^ (m - k))) MeasureTheory.volume 0 1 := by + apply Continuous.intervalIntegrable + fun_prop + have h := intervalIntegral.integral_eq_sub_of_hasDerivAt (fun t _ => hd t) hi + simpa [intervalIntegral.integral_const_mul] using h + +/-- Normalized elementary coefficient (the sign is part of the coefficient). -/ +def coeff (r : Multiset ℂ) (μ : ℂ) (k : ℕ) : ℂ := + (-1) ^ k * r.esymm k / ((r.card.choose k : ℂ) * μ ^ k) + +/-- Exact finite centered beta expansion. Centering need not equal the mean for this +identity; the mean condition is used only to remove degree one below. -/ +theorem centered_integral (q : Multiset ℂ) (a μ : ℂ) (hμ : μ ≠ 0) : + (q.card + 1) * (a * μ) * + (∫ t in (0 : ℝ)..1, (q.map (fun v => 1 - a * t * v)).prod) = + ∑ k ∈ Finset.range (q.card + 1), + coeff (q.map (fun v => v - μ)) μ k * H q.card k (a * μ) := by + let r := q.map (fun v => v - μ) + have he : (fun t : ℝ => (q.map (fun v => 1 - a * t * v)).prod) = + fun t : ℝ => ∑ k ∈ Finset.range (q.card + 1), + ((-a) ^ k * r.esymm k) * ((t : ℂ) ^ k * (1 - a * μ * t) ^ (q.card - k)) := by + funext t + rw [centered_product q a μ t] + apply Finset.sum_congr rfl + intro k hk + dsimp [r] + ring + rw [he, intervalIntegral.integral_finsetSum] + · rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro k hk + have hk' : k ≤ q.card := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk) + have hc : (q.card.choose k : ℂ) ≠ 0 := by exact_mod_cast Nat.choose_ne_zero hk' + rw [intervalIntegral.integral_const_mul, ← finite_beta q.card k hk' (a * μ)] + dsimp [coeff, r] + rw [Multiset.card_map] + rw [show -a = (-1 : ℂ) * a by ring] + simp only [mul_pow, pow_succ] + field_simp + · intro k hk + apply Continuous.intervalIntegrable + fun_prop + +/-- The top endpoint is not dropped: H at k=m is exactly z^(m+1). -/ +theorem H_top (m : ℕ) (z : ℂ) : H m m z = z ^ (m + 1) := by + have hs := add_pow z (1 - z) (m + 1) + rw [Finset.sum_range_succ] at hs + simp only [Nat.choose_self, Nat.sub_self, pow_zero, Nat.cast_one, mul_one] at hs + have hb : B m m z = ∑ i ∈ Finset.range (m + 1), + z ^ i * (1 - z) ^ (m + 1 - i) * ((m + 1).choose i : ℂ) := by + apply Finset.sum_congr rfl + intro i hi + ring + rw [H, hb] + have he : z + (1 - z) = 1 := by ring + rw [he, one_pow] at hs + linear_combination hs + +/-- The centered second moment, without complex conjugation. -/ +def kappa (r : Multiset ℂ) : ℂ := (r.map (fun v => v ^ 2)).sum / r.card + +/-- The exact second-order correction. -/ +def correction (r : Multiset ℂ) (μ : ℂ) : ℂ := + kappa r / (((r.card : ℂ) - 1) * μ ^ 2) + +@[simp] theorem coeff_zero (r : Multiset ℂ) (μ : ℂ) : coeff r μ 0 = 1 := by + simp [coeff] + +theorem coeff_one (r : Multiset ℂ) (μ : ℂ) (hr : r.sum = 0) : coeff r μ 1 = 0 := by + simp [coeff, hr] + +/-- The second-order coefficient is computed, not postulated. -/ +theorem coeff_two (r : Multiset ℂ) (μ : ℂ) (hm : 2 ≤ r.card) + (hr : r.sum = 0) (hμ : μ ≠ 0) : coeff r μ 2 = -correction r μ := by + have hc : (r.card.choose 2 : ℂ) ≠ 0 := by exact_mod_cast Nat.choose_ne_zero hm + have hm₀ : (r.card : ℂ) ≠ 0 := by exact_mod_cast (by omega : r.card ≠ 0) + have hm₁ : (r.card : ℂ) - 1 ≠ 0 := by + have h : (r.card : ℂ) ≠ 1 := by exact_mod_cast (by omega : r.card ≠ 1) + exact sub_ne_zero.mpr h + have hc₂ : 2 * (r.card.choose 2 : ℂ) = (r.card : ℂ) * ((r.card : ℂ) - 1) := by + have h₂ := Nat.add_one_mul_choose_eq (r.card - 1) 1 + rw [show r.card - 1 + 1 = r.card by omega] at h₂ + norm_num only [Nat.choose_one_right, Nat.reduceAdd] at h₂ + have h₃ : (r.card : ℂ) * ((r.card : ℂ) - 1) = (r.card.choose 2 : ℂ) * 2 := by + simpa only [Nat.cast_mul, Nat.cast_sub (by omega : 1 ≤ r.card), Nat.cast_one, + Nat.cast_ofNat] using congrArg (Nat.cast : ℕ → ℂ) h₂ + linear_combination h₃.symm + have he := two_mul_esymm_two r + rw [hr, zero_pow (by decide : 2 ≠ 0), zero_sub] at he + dsimp [coeff, correction, kappa] + norm_num + field_simp + linear_combination (r.card.choose 2 : ℂ) * he - r.esymm 2 * hc₂ + +/-- Every degree from 3 through m is retained. -/ +def tail (r : Multiset ℂ) (μ z : ℂ) : ℂ := + ∑ k ∈ Finset.Ico 3 (r.card + 1), coeff r μ k * H r.card k z + +/-- Finite epsilon, with both low-degree endpoint corrections and all higher H terms. -/ +def epsilon (r : Multiset ℂ) (μ z : ℂ) : ℂ := + -(1 - z) ^ (r.card + 1) + correction r μ * B r.card 2 z + tail r μ z + +/-- The paper's exact second-order identity, for any complex nonzero mean. -/ +theorem second_order (q : Multiset ℂ) (a μ : ℂ) (hm : 2 ≤ q.card) + (hmean : q.sum = q.card * μ) (hμ : μ ≠ 0) : + (q.card + 1) * (a * μ) * + (∫ t in (0 : ℝ)..1, (q.map (fun v => 1 - a * t * v)).prod) = + 1 - correction (q.map (fun v => v - μ)) μ + + epsilon (q.map (fun v => v - μ)) μ (a * μ) := by + let r := q.map (fun v => v - μ) + have hrc : r.card = q.card := Multiset.card_map _ _ + have hrs : r.sum = 0 := centered_sum q μ hmean + rw [centered_integral q a μ hμ] + have hs := Finset.sum_range_add_sum_Ico + (fun k => coeff r μ k * H q.card k (a * μ)) (by omega : 3 ≤ q.card + 1) + rw [← hs] + rw [show 3 = 2 + 1 from rfl, Finset.sum_range_succ, + show 2 = 1 + 1 from rfl, Finset.sum_range_succ, Finset.sum_range_succ] + simp only [Finset.sum_range_zero, coeff_zero, one_mul, coeff_one r μ hrs, zero_mul, + zero_add, add_zero] + rw [coeff_two r μ (by omega) hrs hμ] + dsimp [epsilon, tail] + rw [hrc] + simp only [H, B_zero] + ring + +/-- The mean squared norm of the centered family. -/ +def variance (r : Multiset ℂ) : ℝ := (r.map (fun v => ‖v‖ ^ 2)).sum / r.card + +/-- The paper's Γ, in real arithmetic. -/ +def Gamma (r : Multiset ℂ) (μ : ℂ) : ℝ := + variance r / (((r.card : ℝ) - 1) * ‖μ‖ ^ 2) + +theorem norm_kappa_le_variance (r : Multiset ℂ) : ‖kappa r‖ ≤ variance r := by + have hs : ‖(r.map (fun v => v ^ 2)).sum‖ ≤ (r.map (fun v => ‖v‖ ^ 2)).sum := by + induction r using Multiset.induction_on with + | empty => simp + | cons v r ih => + simp only [Multiset.map_cons, Multiset.sum_cons] + exact (norm_add_le _ _).trans (by simpa [norm_pow] using add_le_add_left ih (‖v ^ 2‖)) + simpa [kappa, variance, norm_div] using + div_le_div_of_nonneg_right hs (Nat.cast_nonneg r.card) + +theorem norm_correction_le_Gamma (r : Multiset ℂ) (μ : ℂ) (hm : 2 ≤ r.card) : + ‖correction r μ‖ ≤ Gamma r μ := by + have hmR : (2 : ℝ) ≤ r.card := by exact_mod_cast hm + have he : (r.card : ℂ) - 1 = (((r.card : ℝ) - 1 : ℝ) : ℂ) := by push_cast; rfl + have hn : ‖(r.card : ℂ) - 1‖ = (r.card : ℝ) - 1 := by + rw [he, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg (by linarith)] + simp only [correction, Gamma, norm_div, norm_mul, norm_pow, hn] + exact div_le_div_of_nonneg_right (norm_kappa_le_variance r) + (mul_nonneg (by linarith) (sq_nonneg _)) + +/-- The actual coefficient modulus, ready for an independent Fourier upper bound. -/ +theorem norm_coeff (r : Multiset ℂ) (μ : ℂ) (k : ℕ) : + ‖coeff r μ k‖ = ‖r.esymm k‖ / ((r.card.choose k : ℝ) * ‖μ‖ ^ k) := by + simp [coeff, norm_pow] + +/-- The finite triangle budget, using the actual elementary symmetric coefficients. +No endpoint H is replaced by 1. -/ +def Efin (r : Multiset ℂ) (μ z : ℂ) : ℝ := + ‖1 - z‖ ^ (r.card + 1) + Gamma r μ * ‖B r.card 2 z‖ + + ∑ k ∈ Finset.Ico 3 (r.card + 1), + (‖r.esymm k‖ / ((r.card.choose k : ℝ) * ‖μ‖ ^ k)) * ‖H r.card k z‖ + +theorem norm_epsilon_le (r : Multiset ℂ) (μ z : ℂ) (hm : 2 ≤ r.card) : + ‖epsilon r μ z‖ ≤ Efin r μ z := by + have ht : ‖tail r μ z‖ ≤ ∑ k ∈ Finset.Ico 3 (r.card + 1), + (‖r.esymm k‖ / ((r.card.choose k : ℝ) * ‖μ‖ ^ k)) * ‖H r.card k z‖ := by + simpa only [tail, norm_mul, norm_coeff] using + norm_sum_le (Finset.Ico 3 (r.card + 1)) (fun k => coeff r μ k * H r.card k z) + have hc := mul_le_mul_of_nonneg_right (norm_correction_le_Gamma r μ hm) + (norm_nonneg (B r.card 2 z)) + calc + ‖epsilon r μ z‖ ≤ ‖-(1 - z) ^ (r.card + 1) + correction r μ * B r.card 2 z‖ + + ‖tail r μ z‖ := norm_add_le _ _ + _ ≤ (‖-(1 - z) ^ (r.card + 1)‖ + ‖correction r μ * B r.card 2 z‖) + + ‖tail r μ z‖ := add_le_add (norm_add_le _ _) le_rfl + _ ≤ Efin r μ z := by + simp only [norm_neg, norm_pow, norm_mul, Efin] + linarith + +/-- C-budget: the strict finite budget forces the normalized first-origin integral +outside the closed unit disk. The expansion is proved above, not a hypothesis. -/ +theorem C_budget (q : Multiset ℂ) (a : ℝ) (μ : ℂ) (hm : 2 ≤ q.card) + (ha : 0 ≤ a) (hmean : q.sum = q.card * μ) (hμ : μ ≠ 0) + (hbudget : Efin (q.map (fun v => v - μ)) μ (a * μ) + + Gamma (q.map (fun v => v - μ)) μ < 1 - a * ‖μ‖) : + 1 < ‖(q.card + 1 : ℂ) * + (∫ t in (0 : ℝ)..1, (q.map (fun v => 1 - (a : ℂ) * t * v)).prod)‖ := by + let r := q.map (fun v => v - μ) + let J : ℂ := (q.card + 1 : ℂ) * + (∫ t in (0 : ℝ)..1, (q.map (fun v => 1 - (a : ℂ) * t * v)).prod) + have hm' : 2 ≤ r.card := by simpa [r] using hm + have he := second_order q (a : ℂ) μ hm hmean hμ + have hident : (1 : ℂ) = (a * μ) * J + correction r μ - epsilon r μ (a * μ) := by + dsimp [J, r] + linear_combination -he + have hn : (1 : ℝ) ≤ ‖(a * μ) * J‖ + ‖correction r μ‖ + ‖epsilon r μ (a * μ)‖ := by + calc (1 : ℝ) = ‖(1 : ℂ)‖ := by simp + _ = ‖(a * μ) * J + correction r μ - epsilon r μ (a * μ)‖ := congrArg norm hident + _ ≤ ‖(a * μ) * J + correction r μ‖ + ‖epsilon r μ (a * μ)‖ := norm_sub_le _ _ + _ ≤ _ := add_le_add (norm_add_le _ _) le_rfl + have ha' : ‖(a : ℂ)‖ = a := by simp [Real.norm_eq_abs, abs_of_nonneg ha] + simp only [norm_mul, ha'] at hn + have hc := norm_correction_le_Gamma r μ hm' + have heps := norm_epsilon_le r μ (a * μ) hm' + change 1 < ‖J‖ + by_contra h + have hJ : ‖J‖ ≤ 1 := le_of_not_gt h + have hmul := mul_le_mul_of_nonneg_left hJ (mul_nonneg ha (norm_nonneg μ)) + change Efin r μ (a * μ) + Gamma r μ < 1 - a * ‖μ‖ at hbudget + nlinarith + +end Sendov.PaperCentered diff --git a/Sendov/Analytic/PaperCenteredBound.lean b/Sendov/Analytic/PaperCenteredBound.lean new file mode 100644 index 0000000..5615181 --- /dev/null +++ b/Sendov/Analytic/PaperCenteredBound.lean @@ -0,0 +1,143 @@ +import Sendov.Analytic.PaperCentered +import Sendov.Analytic.PaperCoefficient + +/-! +# The paper's square-root centered finite budget + +Assembles the optimized coefficient estimate and the exact centered expansion. +The variance is always that of the actual centered multiset. Every complex +endpoint H is retained, including the top degree. This is a sufficient-budget +implication, not a claim that the budget is positive on any geometric domain. +-/ + +noncomputable section +open scoped BigOperators +namespace Sendov.PaperCenteredBound +open PaperCentered + +/-- The two component modules use definitionally identical actual variances. -/ +theorem variance_eq (r : Multiset ℂ) : + PaperCoefficient.variance r = PaperCentered.variance r := rfl + +/-- REPORT §3.2, with an explicit top-degree branch. Only positive degrees +through m are used; outside that range the value is zero (except m=k=0). -/ +def C (m k : ℕ) (v : ℝ) : ℝ := + if k = m then Real.sqrt (v ^ m) + else if 0 < k ∧ k < m then + Real.sqrt ((m : ℝ) ^ m / ((k : ℝ) ^ k * ((m - k : ℕ) : ℝ) ^ (m - k)) * v ^ k) + else 0 + +@[simp] theorem C_top (m : ℕ) (v : ℝ) : C m m v = Real.sqrt (v ^ m) := by + simp [C] + +theorem C_interior (m k : ℕ) (v : ℝ) (hk : 0 < k) (hkm : k < m) : + C m k v = Real.sqrt + ((m : ℝ) ^ m / ((k : ℝ) ^ k * ((m - k : ℕ) : ℝ) ^ (m - k)) * v ^ k) := by + simp [C, hkm.ne, hk, hkm] + +theorem C_nonneg (m k : ℕ) (v : ℝ) : 0 ≤ C m k v := by + unfold C + split_ifs <;> positivity + +/-- Zero variance is covered without choosing a singular optimizing radius. -/ +@[simp] theorem C_zero_variance (m k : ℕ) (hk : 0 < k) : C m k 0 = 0 := by + by_cases hkm : k = m + · subst m + simp [C, zero_pow hk.ne'] + · simp [C, hkm, zero_pow hk.ne'] + +/-- The exact paper square-root bound, including k=m and zero variance. -/ +theorem norm_esymm_le_C (r : Multiset ℂ) (hr : r.sum = 0) + (k : ℕ) (hk : 0 < k) (hkm : k ≤ r.card) : + ‖r.esymm k‖ ≤ C r.card k (variance r) := by + by_cases htop : k = r.card + · subst k + rw [C_top] + have h := PaperCoefficient.norm_esymm_card_sq_le r + rw [variance_eq] at h + exact (Real.le_sqrt (norm_nonneg _) ((sq_nonneg _).trans h)).2 h + · rw [C_interior _ _ _ hk (lt_of_le_of_ne hkm htop)] + have h := PaperCoefficient.norm_esymm_sq_le_optimized r hr k hk + (lt_of_le_of_ne hkm htop) + rw [variance_eq] at h + exact (Real.le_sqrt (norm_nonneg _) ((sq_nonneg _).trans h)).2 h + +/-- Normalized actual coefficient interface. No real-mean assumption is made; +the inequality even holds at zero mean under Lean's total division convention. -/ +theorem norm_coeff_le_C (r : Multiset ℂ) (hr : r.sum = 0) + (μ : ℂ) (k : ℕ) (hk : 0 < k) (hkm : k ≤ r.card) : + ‖coeff r μ k‖ ≤ C r.card k (variance r) / ((r.card.choose k : ℝ) * ‖μ‖ ^ k) := by + rw [norm_coeff] + exact div_le_div_of_nonneg_right (norm_esymm_le_C r hr k hk hkm) (by positivity) + +/-- The coefficient interface on the actual deviations from a complex mean. -/ +theorem norm_centered_coeff_le_C (q : Multiset ℂ) (μ : ℂ) + (hmean : q.sum = q.card * μ) (k : ℕ) (hk : 0 < k) (hkm : k ≤ q.card) : + ‖coeff (q.map (fun v => v - μ)) μ k‖ ≤ + C q.card k (variance (q.map (fun v => v - μ))) / + ((q.card.choose k : ℝ) * ‖μ‖ ^ k) := by + simpa only [Multiset.card_map] using + norm_coeff_le_C (q.map (fun v => v - μ)) (centered_sum q μ hmean) μ k hk + (by simpa only [Multiset.card_map] using hkm) + +/-- REPORT §3.3 E_fin: the exact square-root majorant, not the actual-coefficient +triangle bound. All finite endpoints remain inside complex norms. -/ +def majorant_Efin (r : Multiset ℂ) (μ z : ℂ) : ℝ := + ‖1 - z‖ ^ (r.card + 1) + Gamma r μ * ‖B r.card 2 z‖ + + ∑ k ∈ Finset.Ico 3 (r.card + 1), + (C r.card k (variance r) / ((r.card.choose k : ℝ) * ‖μ‖ ^ k)) * ‖H r.card k z‖ + +/-- Comparison with the accepted actual-coefficient finite budget. -/ +theorem Efin_le_majorant_Efin (r : Multiset ℂ) (hr : r.sum = 0) (μ z : ℂ) : + Efin r μ z ≤ majorant_Efin r μ z := by + unfold Efin majorant_Efin + apply add_le_add le_rfl + apply Finset.sum_le_sum + intro k hk + obtain ⟨hk₀, hk₁⟩ := Finset.mem_Ico.mp hk + apply mul_le_mul_of_nonneg_right _ (norm_nonneg _) + exact div_le_div_of_nonneg_right (norm_esymm_le_C r hr k (by omega) (by omega)) + (by positivity) + +/-- The actual finite epsilon obeys the paper's square-root majorant. -/ +theorem norm_epsilon_le_majorant_Efin (r : Multiset ℂ) (hr : r.sum = 0) + (μ z : ℂ) (hm : 2 ≤ r.card) : + ‖epsilon r μ z‖ ≤ majorant_Efin r μ z := + (norm_epsilon_le r μ z hm).trans (Efin_le_majorant_Efin r hr μ z) + +/-- C-budget with the actual centered variance, valid for any nonzero complex +mean. The strict scalar budget is an explicit hypothesis, never a conclusion. -/ +theorem C_budget (q : Multiset ℂ) (a : ℝ) (μ : ℂ) (hm : 2 ≤ q.card) + (ha : 0 ≤ a) (hmean : q.sum = q.card * μ) (hμ : μ ≠ 0) + (hbudget : majorant_Efin (q.map (fun v => v - μ)) μ (a * μ) + + Gamma (q.map (fun v => v - μ)) μ < 1 - a * ‖μ‖) : + 1 < ‖(q.card + 1 : ℂ) * + (∫ t in (0 : ℝ)..1, (q.map (fun v => 1 - (a : ℂ) * t * v)).prod)‖ := by + apply PaperCentered.C_budget q a μ hm ha hmean hμ + exact lt_of_le_of_lt + (add_le_add (Efin_le_majorant_Efin _ (centered_sum q μ hmean) μ (a * μ)) le_rfl) + hbudget + +/-- At the top endpoint the apparent inverse power of the mean cancels exactly. +The scale a can itself be complex; no positivity interpretation of H is used. -/ +theorem majorant_top_suppression (r : Multiset ℂ) (a μ : ℂ) (hμ : μ ≠ 0) : + (C r.card r.card (variance r) / ((r.card.choose r.card : ℝ) * ‖μ‖ ^ r.card)) * + ‖H r.card r.card (a * μ)‖ = + Real.sqrt (variance r ^ r.card) * ‖a‖ ^ (r.card + 1) * ‖μ‖ := by + have hn : ‖μ‖ ≠ 0 := norm_ne_zero_iff.mpr hμ + rw [C_top, H_top, norm_pow, norm_mul, mul_pow, Nat.choose_self] + simp only [Nat.cast_one, one_mul] + rw [pow_succ ‖μ‖] + field_simp + +/-- The same cancellation for the signed actual top coefficient. -/ +theorem coeff_top_suppression (r : Multiset ℂ) (a μ : ℂ) (hμ : μ ≠ 0) : + coeff r μ r.card * H r.card r.card (a * μ) = + (-1) ^ r.card * r.prod * a ^ (r.card + 1) * μ := by + rw [coeff, H_top, Nat.choose_self] + simp only [Nat.cast_one, one_mul] + have he : r.esymm r.card = r.prod := by simp [Multiset.esymm] + rw [he, mul_pow, pow_succ μ] + field_simp + +end Sendov.PaperCenteredBound diff --git a/Sendov/Analytic/PaperCenteredCertificate.lean b/Sendov/Analytic/PaperCenteredCertificate.lean new file mode 100644 index 0000000..5faeb82 --- /dev/null +++ b/Sendov/Analytic/PaperCenteredCertificate.lean @@ -0,0 +1,141 @@ +import Sendov.Analytic.PaperCenteredBound +import Mathlib.Algebra.Polynomial.Expand +import Mathlib.Analysis.SpecialFunctions.Integrals.Basic + +/-! +# Exact finite certificate bridge + +Rational witnesses may be generated externally, but this module consumes only +kernel-checked inequalities bound to the actual centered multiset. It does not +assume an error estimate or replace either error definition by a scalar proxy. +-/ +noncomputable section +open scoped BigOperators +namespace Sendov.PaperCenteredCertificate +open PaperCentered PaperCenteredBound + +/-- Real binomial endpoint, useful for exact rational replay. -/ +def realB (m k : ℕ) (z : ℝ) : ℝ := + ∑ j ∈ Finset.range (k + 1), (m + 1).choose j * z ^ j * (1 - z) ^ (m + 1 - j) + +lemma B_ofReal (m k : ℕ) (z : ℝ) : B m k (z : ℂ) = (realB m k z : ℂ) := by + simp [B, realB] + +lemma realB_nonneg (m k : ℕ) (z : ℝ) (hz : 0 ≤ z) (hz1 : z ≤ 1) : + 0 ≤ realB m k z := by + apply Finset.sum_nonneg + intro j hj + exact mul_nonneg (mul_nonneg (Nat.cast_nonneg _) (pow_nonneg hz _)) + (pow_nonneg (sub_nonneg.mpr hz1) _) + +lemma realB_le_one (m k : ℕ) (z : ℝ) (hk : k ≤ m) + (hz : 0 ≤ z) (hz1 : z ≤ 1) : realB m k z ≤ 1 := by + have hsum : (∑ j ∈ Finset.range (m + 1 + 1), + ((m + 1).choose j : ℝ) * z ^ j * (1 - z) ^ (m + 1 - j)) = 1 := by + have h := add_pow z (1 - z) (m + 1) + rw [show z + (1 - z) = 1 by ring, one_pow] at h + calc + _ = ∑ j ∈ Finset.range (m + 1 + 1), + z ^ j * (1 - z) ^ (m + 1 - j) * ((m + 1).choose j : ℝ) := by + apply Finset.sum_congr rfl + intro j hj + ring + _ = 1 := h.symm + unfold realB + apply le_trans (b := ∑ j ∈ Finset.range (m + 1 + 1), + ((m + 1).choose j : ℝ) * z ^ j * (1 - z) ^ (m + 1 - j)) _ hsum.le + apply Finset.sum_le_sum_of_subset_of_nonneg + · exact Finset.range_mono (by omega) + · intro j hj hj' + exact mul_nonneg (mul_nonneg (Nat.cast_nonneg _) (pow_nonneg hz _)) + (pow_nonneg (sub_nonneg.mpr hz1) _) + +/-- All endpoints, including the top endpoint, have norm at most one when the +scale really is in the real unit interval. No such claim is made for complex scales. -/ +theorem norm_H_ofReal_le_one (m k : ℕ) (z : ℝ) (hk : k ≤ m) + (hz : 0 ≤ z) (hz1 : z ≤ 1) : ‖H m k (z : ℂ)‖ ≤ 1 := by + rw [H, B_ofReal, ← Complex.ofReal_one, ← Complex.ofReal_sub, + Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg + (sub_nonneg.mpr (realB_le_one m k z hk hz hz1))] + linarith [realB_nonneg m k z hz hz1] + +/-- A square witness checks a normalized square-root coefficient without trusting +an external square-root implementation. The top-degree branch is explicit. -/ +theorem normalized_C_le (m k : ℕ) (v u b : ℝ) + (hk : 0 < k) (hkm : k ≤ m) (hu : 0 < u) (hb : 0 ≤ b) + (hsq : (if k = m then v ^ m else + (m : ℝ) ^ m / ((k : ℝ) ^ k * ((m - k : ℕ) : ℝ) ^ (m - k)) * v ^ k) ≤ + (b * ((m.choose k : ℝ) * u ^ k)) ^ 2) : + C m k v / ((m.choose k : ℝ) * u ^ k) ≤ b := by + have hd : 0 < (m.choose k : ℝ) * u ^ k := + mul_pos (by exact_mod_cast Nat.choose_pos hkm) (pow_pos hu _) + apply (div_le_iff₀ hd).2 + have he : C m k v = Real.sqrt (if k = m then v ^ m else + (m : ℝ) ^ m / ((k : ℝ) ^ k * ((m - k : ℕ) : ℝ) ^ (m - k)) * v ^ k) := by + by_cases h : k = m + · simp [h] + · simp [C, h, hk, lt_of_le_of_ne hkm h] + rw [he] + exact (Real.sqrt_le_left (mul_nonneg hb hd.le)).2 hsq + +/-- Finite per-degree normalized bounds assemble into the actual majorant. -/ +theorem majorant_le (r : Multiset ℂ) (μ z : ℂ) (p : ℝ) (b : ℕ → ℝ) + (hp : ‖1 - z‖ ^ (r.card + 1) + Gamma r μ * ‖B r.card 2 z‖ ≤ p) + (hH : ∀ k ∈ Finset.Ico 3 (r.card + 1), ‖H r.card k z‖ ≤ 1) + (hb : ∀ k ∈ Finset.Ico 3 (r.card + 1), + C r.card k (variance r) / ((r.card.choose k : ℝ) * ‖μ‖ ^ k) ≤ b k) : + majorant_Efin r μ z ≤ p + ∑ k ∈ Finset.Ico 3 (r.card + 1), b k := by + apply add_le_add hp + apply Finset.sum_le_sum + intro k hk + calc + _ ≤ C r.card k (variance r) / ((r.card.choose k : ℝ) * ‖μ‖ ^ k) := + mul_le_of_le_one_right (div_nonneg (C_nonneg _ _ _) (by positivity)) (hH k hk) + _ ≤ b k := hb k hk + +/-- Independent actual-coefficient certificate path, not the generic C majorant. -/ +theorem actual_le (r : Multiset ℂ) (μ z : ℂ) (p : ℝ) (b : ℕ → ℝ) + (hp : ‖1 - z‖ ^ (r.card + 1) + Gamma r μ * ‖B r.card 2 z‖ ≤ p) + (hH : ∀ k ∈ Finset.Ico 3 (r.card + 1), ‖H r.card k z‖ ≤ 1) + (hb : ∀ k ∈ Finset.Ico 3 (r.card + 1), + ‖r.esymm k‖ / ((r.card.choose k : ℝ) * ‖μ‖ ^ k) ≤ b k) : + Efin r μ z ≤ p + ∑ k ∈ Finset.Ico 3 (r.card + 1), b k := by + apply add_le_add hp + apply Finset.sum_le_sum + intro k hk + calc + _ ≤ ‖r.esymm k‖ / ((r.card.choose k : ℝ) * ‖μ‖ ^ k) := + mul_le_of_le_one_right (by positivity) (hH k hk) + _ ≤ b k := hb k hk + +/-- Exact elementary coefficients of two equally repeated opposite deviations. +The formula uses Vieta and polynomial dilation, not enumeration of subsets. -/ +theorem esymm_opposite_replicate (n k : ℕ) (d : ℂ) (hk : k ≤ 2 * n) : + (Multiset.replicate n (-d) + Multiset.replicate n d).esymm k = + if 2 ∣ (2 * n - k) then + (-d ^ 2) ^ (n - (2 * n - k) / 2) * (n.choose ((2 * n - k) / 2) : ℂ) + else 0 := by + let r := Multiset.replicate n (-d) + Multiset.replicate n d + have hc : r.card = 2 * n := by simp [r]; omega + have hp : (r.map (fun w => Polynomial.X + Polynomial.C w)).prod = + Polynomial.expand ℂ 2 ((Polynomial.X + Polynomial.C (-d ^ 2)) ^ n) := by + simp only [r, Multiset.map_add, Multiset.map_replicate, Multiset.prod_add, + Multiset.prod_replicate, map_pow, map_add, Polynomial.expand_X, + Polynomial.expand_C, ← mul_pow] + congr 1 + simp only [map_neg, map_pow] + ring + have hv := Multiset.prod_X_add_C_coeff r (k := 2 * n - k) (by omega) + rw [hc, Nat.sub_sub_self hk, hp, Polynomial.coeff_expand (by decide : 0 < 2)] at hv + simpa only [Polynomial.coeff_X_add_C_pow] using hv.symm + +/-- A reusable exact lower rectangle for a real integrand. -/ +theorem lower_rectangle (f : ℝ → ℝ) (s t b : ℝ) (hst : s ≤ t) + (hf : IntervalIntegrable f MeasureTheory.volume s t) + (hb : ∀ x ∈ Set.Icc s t, b ≤ f x) : + (t - s) * b ≤ ∫ x in s..t, f x := by + have h := intervalIntegral.integral_mono_on hst + (intervalIntegrable_const (c := b)) hf hb + simpa only [intervalIntegral.integral_const, smul_eq_mul] using h + +end Sendov.PaperCenteredCertificate diff --git a/Sendov/Analytic/PaperCenteredEndpoint.lean b/Sendov/Analytic/PaperCenteredEndpoint.lean new file mode 100644 index 0000000..c1e8207 --- /dev/null +++ b/Sendov/Analytic/PaperCenteredEndpoint.lean @@ -0,0 +1,153 @@ +import Sendov.Analytic.PaperCenteredTail +import Sendov.Analytic.PaperPolar +import Mathlib.Data.Nat.Choose.Cast + +/-! # Uniform control of the zeroth centered endpoint +A single binomial term proves the h/2 bound for the zeroth endpoint in every +degree; no finite table or bound on alpha is used. The positive-variance tail +and the second endpoint remain separate obligations. +-/ +noncomputable section +open scoped BigOperators +namespace Sendov.PaperCenteredEndpoint + +lemma binomial_term (n k : ℕ) (hk : k ≤ n) (b : ℝ) + (hb0 : 0 ≤ b) (hb1 : b ≤ 1) : + (n.choose k : ℝ) * (1 - b) ^ k * b ^ (n-k) ≤ 1 := by + have ht := Finset.single_le_sum + (s := Finset.range (n+1)) + (f := fun j => (1-b)^j * b^(n-j) * (n.choose j : ℝ)) + (a := k) (fun j _ => by positivity) (by simp; omega) + have hs := add_pow (1-b) b n + rw [show 1-b+b = 1 by ring, one_pow] at hs + rw [← hs] at ht + nlinarith only [ht] + +/-- Any fixed endpoint order, with the finite binomial factor retained. +This provides arbitrarily high algebraic endpoint decay without a degree table. -/ +theorem endpoint_power_order (m k : ℕ) (hk : k ≤ m + 1) (b L : ℝ) + (hb0 : 0 ≤ b) (hb1 : b ≤ 1) (hL : 0 ≤ L) + (hslope : 3 * b ≤ L * (1 - b)) : + 3^k * ((m+1).choose k : ℝ) * b^(m+1) ≤ L^k := by + have hs := pow_le_pow_left₀ (by positivity : 0 ≤ 3*b) hslope k + have hc := binomial_term (m+1) k hk b hb0 hb1 + have he : b^k*b^(m+1-k) = b^(m+1) := by + rw [← pow_add, Nat.add_sub_of_le hk] + have ht := mul_le_mul_of_nonneg_right hs + (mul_nonneg (Nat.cast_nonneg ((m+1).choose k)) (pow_nonneg hb0 (m+1-k))) + have ht' := mul_le_mul_of_nonneg_left hc (pow_nonneg hL k) + calc + _ = (3*b)^k * (((m+1).choose k : ℝ)*b^(m+1-k)) := by rw [mul_pow, ← he]; ring + _ ≤ (L*(1-b))^k * (((m+1).choose k : ℝ)*b^(m+1-k)) := ht + _ = L^k * (((m+1).choose k : ℝ)*(1-b)^k*b^(m+1-k)) := by rw [mul_pow]; ring + _ ≤ L^k := by simpa only [mul_one] using ht' + +lemma binomial_second_term (n : ℕ) (hn : 2 ≤ n) (b : ℝ) + (hb0 : 0 ≤ b) (hb1 : b ≤ 1) : + (n.choose 2 : ℝ) * (1-b)^2 * b^(n-2) ≤ 1 := by + have ht := Finset.single_le_sum + (s := Finset.range (n+1)) + (f := fun k => (1-b)^k * b^(n-k) * (n.choose k : ℝ)) + (a := 2) (fun k _ => by positivity) (by simp; omega) + have hs := add_pow (1-b) b n + rw [show 1-b+b = 1 by ring, one_pow] at hs + rw [← hs] at ht + nlinarith only [ht] + +/-- The rational polar slope controls the entire zeroth endpoint uniformly. -/ +theorem endpoint_power_half (m : ℕ) (hm : 1 ≤ m) (b h : ℝ) + (hb0 : 0 ≤ b) (hb1 : b ≤ 1) (_hh : 0 ≤ h) + (hslope : 3 * b ≤ (m : ℝ) * h * (1 - b)) : + 4*b^(m+1) ≤ h^2 := by + have hc := binomial_second_term (m+1) (by omega) b hb0 hb1 + have hchoose : ((m+1).choose 2 : ℝ) = (m : ℝ)*((m : ℝ)+1)/2 := by + rw [Nat.cast_choose_two] + push_cast + ring + have he : b^2*b^(m-1) = b^(m+1) := by + rw [← pow_add] + congr 1 + omega + have hs : 9*b^2 ≤ (m : ℝ)^2*h^2*(1-b)^2 := by + have hp := mul_self_le_mul_self (by positivity : 0 ≤ 3*b) hslope + nlinarith only [hp] + have hm0 : (0 : ℝ) < m := by exact_mod_cast (show 0 < m by omega) + have hn : 0 ≤ ((m+1).choose 2 : ℝ) := Nat.cast_nonneg _ + have hs' := mul_le_mul_of_nonneg_right hs (mul_nonneg hn (pow_nonneg hb0 (m-1))) + have hc' := mul_le_mul_of_nonneg_left hc (by positivity : 0 ≤ (m : ℝ)^2*h^2) + have hbpow : 9*((m+1).choose 2 : ℝ)*b^(m+1) ≤ (m : ℝ)^2*h^2 := by + calc + _ = (9*b^2)*(((m+1).choose 2 : ℝ)*b^(m-1)) := by rw [← he]; ring + _ ≤ ((m : ℝ)^2*h^2*(1-b)^2)*(((m+1).choose 2 : ℝ)*b^(m-1)) := hs' + _ = (m : ℝ)^2*h^2 * (((m+1).choose 2 : ℝ)*(1-b)^2*b^(m-1)) := by ring + _ ≤ (m : ℝ)^2*h^2 := by + simpa only [show m+1-2 = m-1 by omega, mul_one] using hc' + have hcoef : 4*(m : ℝ)^2 ≤ 9*((m+1).choose 2 : ℝ) := by rw [hchoose]; nlinarith + have ht := (mul_le_mul_of_nonneg_right hcoef (pow_nonneg hb0 (m+1))).trans hbpow + have hcancel : (m : ℝ)^2*(4*b^(m+1)) ≤ (m : ℝ)^2*h^2 := by nlinarith only [ht] + exact (mul_le_mul_iff_right₀ (sq_pos_of_pos hm0)).mp (by simpa only [mul_comm] using hcancel) + +/-- A norm endpoint form, suitable for actual complex means. -/ +theorem norm_endpoint_half (m : ℕ) (hm : 1 ≤ m) (z : ℂ) (b h : ℝ) + (hb0 : 0 ≤ b) (hb1 : b ≤ 1) (hh : 0 ≤ h) + (hslope : 3 * b ≤ (m : ℝ) * h * (1 - b)) (hz : ‖1 - z‖ ^ 2 ≤ b) : + ‖1-z‖^(m+1) ≤ h/2 := by + have hp := pow_le_pow_left₀ (sq_nonneg ‖1-z‖) hz (m+1) + have he : (‖1-z‖^2)^(m+1) = (‖1-z‖^(m+1))^2 := by rw [← pow_mul, ← pow_mul]; congr 1; omega + rw [he] at hp + have hb := endpoint_power_half m hm b h hb0 hb1 hh hslope + nlinarith only [hp, hb, hh, pow_nonneg (norm_nonneg (1-z)) (m+1)] + +/-- The actual complex endpoint is at most h/2 on raw polar, uniformly in degree. +In fact the proof only needs 0