Main.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.TriangularCovering.small_abs_le_one line 12
theorem OAI.TriangularCovering.finiteFamily_expansion line 18
Source documentation
The area expansion with explicit uniform remainder constant 14.
```
theorem finiteFamily_expansion {ε : ℝ} (he : 0 < ε) (hsmall : ε ≤ η/2) :
    |totalArea (finiteFamily ε he)/H - (1/2-(13/6000:ℝ)*ε^2)| ≤ 14*ε^4 := by
…
```
Mentions: OAI.TriangularCovering.η, OAI.TriangularCovering.totalArea, OAI.TriangularCovering.finiteFamily, OAI.TriangularCovering.H
lemma OAI.TriangularCovering.finiteFamily_ratio_lt line 23
lemma OAI.TriangularCovering.finiteFamily_strict line 31
theorem OAI.TriangularCovering.main_asymptotic line 38
Source documentation
The asymptotic covering bound, including exact finite count and strict saving.
```
theorem main_asymptotic : MainAsymptotic := by
…
```
Mentions: OAI.TriangularCovering.MainAsymptotic
lemma OAI.TriangularCovering.relativeCost_le_totalArea line 44
theorem OAI.TriangularCovering.normalized_counterexample line 54
Source documentation
The normalized covering bound using perpendicular shadows.
```
theorem normalized_counterexample : NormalizedCounterexample := by
…
```
Mentions: OAI.TriangularCovering.NormalizedCounterexample
theorem OAI.TriangularCovering.main line 61
Source documentation
The minimum shadow area, asymptotic covering bound, and normalized counterexample.
Distinct definitions of this name: ComparatorChallenges/TriangularCovering.lean:65 (same statement text; different proof or body). Qualify references as OAI.TriangularCovering.main@path.
```
theorem main : A_min = H ∧ MainAsymptotic ∧ NormalizedCounterexample :=
…
```
Mentions: OAI.TriangularCovering.A_min, OAI.TriangularCovering.H, OAI.TriangularCovering.MainAsymptotic, OAI.TriangularCovering.NormalizedCounterexample