OAI/Analysis/Unitarizability/Parameters.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Dixmier.endpointCapacity line 12
2. def OAI.Dixmier.fiberDimension line 13
3. theorem OAI.Dixmier.dimension_ratio_bound line 16
4. theorem OAI.Dixmier.geometric_log_tendsto line 38

   Source documentation

   The logarithm contributes only a linear factor in the word length.

   theorem geometric_log_tendsto {a : ℝ} (ha : 0 ≤ a) (ha1 : a < 1)
       {d : ℝ} (hd : 0 < d) :
       Tendsto (fun ℓ : ℕ => a^ℓ * Real.log (2 * d^ℓ)) atTop (𝓝 0) := by
   …

5. theorem OAI.Dixmier.dimension_ratio_tendsto line 53

   Source documentation

   The dimension ratio tends to zero.

   theorem dimension_ratio_tendsto {d : ℕ} (hd : 2 ≤ d) {ρ : ℝ}
       (hρ : 0 ≤ ρ) (hρ1 : ρ < 1) :
       Tendsto (fun ℓ : ℕ => (fiberDimension d ρ ℓ : ℝ) / (d : ℝ)^ℓ) atTop (𝓝 0) := by
   …

   Mentions: OAI.Dixmier.fiberDimension

6. theorem OAI.Dixmier.endpointCapacity_pos line 74
7. theorem OAI.Dixmier.fiberDimension_pos line 79
8. theorem OAI.Dixmier.reciprocal_dimension_ratio_tendsto line 89

   Source documentation

   Reciprocal dimension ratio used by the direct-sum obstruction.

   theorem reciprocal_dimension_ratio_tendsto {d : ℕ} (hd : 2 ≤ d) {ρ : ℝ}
       (hρ : 0 < ρ) (hρ1 : ρ < 1) :
       Tendsto (fun ℓ : ℕ => (d : ℝ)^ℓ / (fiberDimension d ρ ℓ : ℝ)) atTop atTop := by
   …

   Mentions: OAI.Dixmier.fiberDimension

9. theorem OAI.Dixmier.energy_ratio_tendsto line 104

   Source documentation

   A kernel energy satisfying the cardinality lower bound has unbounded energy per fibre dimension.

   theorem energy_ratio_tendsto {d : ℕ} (hd : 2 ≤ d) {ρ : ℝ}
       (hρ : 0 < ρ) (hρ1 : ρ < 1) (E : ℕ → ℝ)
       (hE : ∀ ℓ, (d : ℝ)^ℓ ≤ E ℓ) :
       Tendsto (fun ℓ => E ℓ / (fiberDimension d ρ ℓ : ℝ)) atTop atTop := by
   …

   Mentions: OAI.Dixmier.fiberDimension