ActualFiniteStrips.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.stripCoordinate line 11
def OAI.SymmetricMahler.stripDomain line 14
def OAI.SymmetricMahler.stripTau line 17
def OAI.SymmetricMahler.stripMap line 20
lemma OAI.SymmetricMahler.verticalFiber_realPart line 24
lemma OAI.SymmetricMahler.strictMonoOn_planarPrimitive_any line 31
theorem OAI.SymmetricMahler.stripMap_injOn line 37
Source documentation
The finite-strip map is injective on its entire complex strip domain.
```
theorem stripMap_injOn (A : J → I → ℝ) (hA : Function.Injective (measurement A))
    {m : ℕ} (hm : 0 < m) : InjOn (stripMap A m) (stripDomain A) := by
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripMap, OAI.SymmetricMahler.stripDomain
lemma OAI.SymmetricMahler.stripDomain_realPart line 44
theorem OAI.SymmetricMahler.stripMap_pairing_bound line 51
Source documentation
The image functional bound uses the literal P and tau, with the uniform analytic estimate proved rather than supplied as a premise.
```
theorem stripMap_pairing_bound (A : J → I → ℝ) {m : ℕ} (hm : 2 ≤ m)
    {z : (I → ℝ) × (I → ℝ)} (hz : z ∈ stripDomain A) (hτ : stripTau A m z < 1)
    {v : I → ℝ} (hv : v ∈ stripBody A) :
    (∑ i, (stripMap A m z).2 i*v i) < 1+Fintype.card J*planarError m := by
…
```
Mentions: OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau, OAI.SymmetricMahler.stripBody, OAI.SymmetricMahler.stripMap, OAI.SymmetricMahler.planarError
def OAI.SymmetricMahler.coordinatePolar line 63
Source documentation
Polar body for the coordinate pairing.
Also declared: ComparatorChallenges/MahlerConjecture.lean:9 (same declaration text), ComparatorChallenges/SymmetricMahlerEquality.lean:12 (same declaration text).
```
def coordinatePolar (K : Set (I → ℝ)) : Set (I → ℝ) :=
…
```
theorem OAI.SymmetricMahler.normalized_stripMap_mem_polar line 68
Source documentation
Dividing the image's vertical component by 1+N epsilon places it in the literal polar body of the strip intersection.
```
theorem normalized_stripMap_mem_polar (A : J → I → ℝ) {m : ℕ} (hm : 2 ≤ m)
    {z : (I → ℝ) × (I → ℝ)} (hz : z ∈ stripDomain A) (hτ : stripTau A m z < 1) :
    (fun i => (stripMap A m z).2 i/(1+Fintype.card J*planarError m)) ∈
      coordinatePolar (stripBody A) := by
…
```
Mentions: OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau, OAI.SymmetricMahler.stripMap, OAI.SymmetricMahler.planarError, OAI.SymmetricMahler.coordinatePolar, OAI.SymmetricMahler.stripBody