Main.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Counterexamples to metric-entropy duality

The construction supplies actual finite-dimensional bodies and their least covering numbers from only the numerical parameters. The public statements retain arbitrary ambient translation centers and the literal polar.

theorem OAI.MetricEntropyDuality.entropyBudget_lt_of_rank line 27
theorem OAI.MetricEntropyDuality.exists_entropy_duality_counterexample_with_covers line 48
Source documentation
The strict counterexample together with actual finite-cover witnesses on both sides. Thus no empty-infimum convention is used for these numbers.
Distinct definitions of this name: ComparatorChallenges/MetricEntropyDuality.lean:45 (same statement text; different proof or body). Qualify references as OAI.MetricEntropyDuality.exists_entropy_duality_counterexample_with_covers@path.
```
theorem exists_entropy_duality_counterexample_with_covers
    (a b : ℝ) (ha : 1 ≤ a) (hb : 1 ≤ b) :
    ∃ n : ℕ, 0 < n ∧ ∃ K : Set (RealSpace (Fin n)),
      IsSymmetricConvexBody K ∧
      Coverable K (cube (Fin n)) ∧
      Coverable (polar (cube (Fin n))) (a⁻¹ • polar K) ∧
      b * Real.log (coveringNumber (polar (cube (Fin n))) (a⁻¹ • polar K) : ℝ) <
        Real.log (coveringNumber K (cube (Fin n)) : ℝ) := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.IsSymmetricConvexBody, OAI.MetricEntropyDuality.Coverable, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.coveringNumber
theorem OAI.MetricEntropyDuality.exists_entropy_duality_counterexample line 72
Source documentation
For every proposed real pair of duality constants, an actual full-dimensional symmetric compact convex body violates the inequality with the standard cube as covering body.
```
theorem exists_entropy_duality_counterexample
    (a b : ℝ) (ha : 1 ≤ a) (hb : 1 ≤ b) :
    ∃ n : ℕ, 0 < n ∧ ∃ K : Set (RealSpace (Fin n)),
      IsSymmetricConvexBody K ∧
      Real.log (coveringNumber K (cube (Fin n)) : ℝ) >
        b * Real.log (coveringNumber (polar (cube (Fin n))) (a⁻¹ • polar K) : ℝ) := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.IsSymmetricConvexBody, OAI.MetricEntropyDuality.coveringNumber, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.polar

theorem OAI.MetricEntropyDuality.exists_entropy_ratio_family line 84

Source documentation

For each fixed scale, the actual polar-to-primal logarithmic entropy ratio tends to zero along a family of growing positive dimensions.

theorem exists_entropy_ratio_family (a : ℝ) (ha : 1 ≤ a) :
    ∃ n : ℕ → ℕ, (∀ j, 0 < n j) ∧
      ∃ K : (j : ℕ) → Set (RealSpace (Fin (n j))),
        (∀ j, IsSymmetricConvexBody (K j) ∧
          Coverable (K j) (cube (Fin (n j))) ∧
          Coverable (polar (cube (Fin (n j)))) (a⁻¹ • polar (K j)) ∧
          0 < Real.log (coveringNumber (K j) (cube (Fin (n j))) : ℝ) ∧
          0 ≤ entropyRatio a (K j)) ∧
        Tendsto n atTop atTop ∧
        Tendsto (fun j => entropyRatio a (K j)) atTop (𝓝 0) := by
…

Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.IsSymmetricConvexBody, OAI.MetricEntropyDuality.Coverable, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.coveringNumber, OAI.MetricEntropyDuality.entropyRatio