ReducedPublishedInputs.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Analytic hypotheses for the inverse Goldbach theorem

Tensorization gives finite Bonami. The progression estimate gives the two Mertens estimates and the principal smooth prime number theorem. Multiplicity-labelled zero enumerations give the fixed-test explicit formula.

theorem OAI.Ostmann.twoInfiniteSummandsImpossible_of_first_mertens line 25
theorem OAI.Ostmann.inverseGoldbach_of_first_mertens line 37
theorem OAI.Ostmann.twoInfiniteSummandsImpossible_of_reduced_published line 50
Source documentation
No independent Bonami, Mertens, or principal smooth PNT input remains.
```
theorem twoInfiniteSummandsImpossible_of_reduced_published
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (Z : ∀ χ, ComplexZeroEnumeration χ) (hD : PublishedComplexZeroDensity Z)
    (hR : PublishedComplexZeroRegion Z) (Pexplicit : PublishedSmoothExplicitFormula Z) :
    TwoInfiniteSummandsImpossible :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.ComplexZeroEnumeration, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.PublishedSmoothExplicitFormula, OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.inverseGoldbach_of_reduced_published line 62
Source documentation
The exact inverse Goldbach conclusion with the same reduced input list.
```
theorem inverseGoldbach_of_reduced_published
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (Z : ∀ χ, ComplexZeroEnumeration χ) (hD : PublishedComplexZeroDensity Z)
    (hR : PublishedComplexZeroRegion Z) (Pexplicit : PublishedSmoothExplicitFormula Z) :
    InverseGoldbach :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.ComplexZeroEnumeration, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.PublishedSmoothExplicitFormula
theorem OAI.Ostmann.twoInfiniteSummandsImpossible_of_analytic_core line 75
Source documentation
The analytic core implies the smoothness and absolute convergence needed for the fixed-test explicit formula.
```
theorem twoInfiniteSummandsImpossible_of_analytic_core
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (Z : ∀ χ, ComplexZeroEnumeration χ) (hD : PublishedComplexZeroDensity Z)
    (hR : PublishedComplexZeroRegion Z) (Pexplicit : SmoothExplicitFormulaCore Z) :
    TwoInfiniteSummandsImpossible :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.ComplexZeroEnumeration, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.SmoothExplicitFormulaCore, OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.inverseGoldbach_of_analytic_core line 87
Source documentation
The exact main theorem after the same analytic input reduction.
```
theorem inverseGoldbach_of_analytic_core
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (Z : ∀ χ, ComplexZeroEnumeration χ) (hD : PublishedComplexZeroDensity Z)
    (hR : PublishedComplexZeroRegion Z) (Pexplicit : SmoothExplicitFormulaCore Z) :
    InverseGoldbach :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.ComplexZeroEnumeration, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.SmoothExplicitFormulaCore

theorem OAI.Ostmann.twoInfiniteSummandsImpossible_of_explicit_formula line 99

Source documentation

Multiplicity-labelled zero enumerations give the ordinary zero count.

theorem twoInfiniteSummandsImpossible_of_explicit_formula
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (e : ∀ χ, ℕ ≃ CharacterZeroCopy χ)
    (hD : PublishedComplexZeroDensity (fun χ => characterZeroEnumeration χ (e χ)))
    (hR : PublishedComplexZeroRegion (fun χ => characterZeroEnumeration χ (e χ)))
    (E : ℝ) (hE : 0 < E)
    (hformula : ∀ χ : PrimitiveComplexCharacter, ∀ X : ℝ, 2 ≤ X →
      ‖smoothMangoldtMean χ.modulus χ.character X +
        (∑' i, smoothZeroTerm (fun χ => characterZeroEnumeration χ (e χ)) χ X i) +
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.CharacterZeroCopy, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.characterZeroEnumeration, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.smoothMangoldtMean, OAI.Ostmann.smoothZeroTerm

theorem OAI.Ostmann.inverseGoldbach_of_explicit_formula line 119

Source documentation

The same explicit-formula-only reduction for manuscript Theorem 1.1.

theorem inverseGoldbach_of_explicit_formula
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (e : ∀ χ, ℕ ≃ CharacterZeroCopy χ)
    (hD : PublishedComplexZeroDensity (fun χ => characterZeroEnumeration χ (e χ)))
    (hR : PublishedComplexZeroRegion (fun χ => characterZeroEnumeration χ (e χ)))
    (E : ℝ) (hE : 0 < E)
    (hformula : ∀ χ : PrimitiveComplexCharacter, ∀ X : ℝ, 2 ≤ X →
      ‖smoothMangoldtMean χ.modulus χ.character X +
        (∑' i, smoothZeroTerm (fun χ => characterZeroEnumeration χ (e χ)) χ X i) +
…

theorem OAI.Ostmann.twoInfiniteSummandsImpossible_of_numbered_zeros line 139
Source documentation
A faithful numbering of the zeros gives the fixed-test explicit formula.
```
theorem twoInfiniteSummandsImpossible_of_numbered_zeros
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (e : ∀ χ, ℕ ≃ CharacterZeroCopy χ)
    (hD : PublishedComplexZeroDensity (fun χ => characterZeroEnumeration χ (e χ)))
    (hR : PublishedComplexZeroRegion (fun χ => characterZeroEnumeration χ (e χ))) :
    TwoInfiniteSummandsImpossible :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.CharacterZeroCopy, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.characterZeroEnumeration, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.inverseGoldbach_of_numbered_zeros line 152
Source documentation
The inverse Goldbach theorem using a faithful numbering of the zeros.
```
theorem inverseGoldbach_of_numbered_zeros
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (e : ∀ χ, ℕ ≃ CharacterZeroCopy χ)
    (hD : PublishedComplexZeroDensity (fun χ => characterZeroEnumeration χ (e χ)))
    (hR : PublishedComplexZeroRegion (fun χ => characterZeroEnumeration χ (e χ))) :
    InverseGoldbach :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.CharacterZeroCopy, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.characterZeroEnumeration, OAI.Ostmann.PublishedComplexZeroRegion
theorem OAI.Ostmann.twoInfiniteSummandsImpossible_of_remaining_published line 165
Source documentation
The zeros and smooth explicit formula come from the Dirichlet L-functions.
```
theorem twoInfiniteSummandsImpossible_of_remaining_published
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (hD : PublishedComplexZeroDensity actualCharacterZeros)
    (hR : PublishedComplexZeroRegion actualCharacterZeros) :
    TwoInfiniteSummandsImpossible :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.actualCharacterZeros, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.inverseGoldbach_of_remaining_published line 177
Source documentation
The inverse Goldbach theorem using the Dirichlet L-function zeros.
```
theorem inverseGoldbach_of_remaining_published
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (Hreal : PublishedRealZeroInput P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (hD : PublishedComplexZeroDensity actualCharacterZeros)
    (hR : PublishedComplexZeroRegion actualCharacterZeros) :
    InverseGoldbach :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.actualCharacterZeros, OAI.Ostmann.PublishedComplexZeroRegion
theorem OAI.Ostmann.twoInfiniteSummandsImpossible_of_actual_region line 190
Source documentation
The real Hadamard expansion gives the real-zero input from a low-height zero-free region.
```
theorem twoInfiniteSummandsImpossible_of_actual_region
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (hregion : ActualRealLowHeightRegion P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (hD : PublishedComplexZeroDensity actualCharacterZeros)
    (hR : PublishedComplexZeroRegion actualCharacterZeros) :
    TwoInfiniteSummandsImpossible :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.ActualRealLowHeightRegion, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.actualCharacterZeros, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.inverseGoldbach_of_actual_region line 202
Source documentation
The inverse Goldbach theorem using the real low-height zero-free region.
```
theorem inverseGoldbach_of_actual_region
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound)
    (hregion : ActualRealLowHeightRegion P0) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (hD : PublishedComplexZeroDensity actualCharacterZeros)
    (hR : PublishedComplexZeroRegion actualCharacterZeros) :
    InverseGoldbach :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.ActualRealLowHeightRegion, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.actualCharacterZeros, OAI.Ostmann.PublishedComplexZeroRegion
theorem OAI.Ostmann.twoInfiniteSummandsImpossible_without_real_zero_input line 215
Source documentation
Restricting the progression constant to the absolute low-height constant gives the real-character zero input.
```
theorem twoInfiniteSummandsImpossible_without_real_zero_input
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (hD : PublishedComplexZeroDensity actualCharacterZeros)
    (hR : PublishedComplexZeroRegion actualCharacterZeros) :
    TwoInfiniteSummandsImpossible := by
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.actualCharacterZeros, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.inverseGoldbach_without_real_zero_input line 229
Source documentation
The exact inverse Goldbach conclusion, with the real-character Hadamard and low-height zero-free-region hypotheses both removed.
```
theorem inverseGoldbach_without_real_zero_input
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (hD : PublishedComplexZeroDensity actualCharacterZeros)
    (hR : PublishedComplexZeroRegion actualCharacterZeros) :
    InverseGoldbach := by
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.actualCharacterZeros, OAI.Ostmann.PublishedComplexZeroRegion
theorem OAI.Ostmann.twoInfiniteSummandsImpossible_without_zero_region_inputs line 243
Source documentation
The progression estimate gives both zero regions using its real-zero Page uniqueness clause.
```
theorem twoInfiniteSummandsImpossible_without_zero_region_inputs
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (hD : PublishedComplexZeroDensity actualCharacterZeros) :
    TwoInfiniteSummandsImpossible :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.actualCharacterZeros, OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.inverseGoldbach_without_zero_region_inputs line 254
Source documentation
The exact inverse Goldbach conclusion with no independent zero-region, Hadamard, explicit-formula or Mertens hypothesis.
```
theorem inverseGoldbach_without_zero_region_inputs
    (P0 : PublishedProgressionInput) (ls : PublishedAdditiveLargeSieve)
    (hsize : PublishedSummandSizeBound) (hSiegel : PublishedSiegelBound)
    (sieve : PublishedQuadraticLargeSieve)
    (hD : PublishedComplexZeroDensity actualCharacterZeros) :
    InverseGoldbach :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedAdditiveLargeSieve, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.actualCharacterZeros