Occupied.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.RowColumn.occupied_numeric_absorb line 14

Source documentation

Absorption of the exact polynomial loss into the absolute occupied-board constant. This is used for both halves of the min.

lemma occupied_numeric_absorb (m n h s : ℕ) (hh : 1 ≤ h) (hs : s ≤ m*n) :
    16 * ((s : ℝ)+1)^((16*(m+n)+8)*h^2) * Real.exp ((m*n-s : ℕ) : ℝ) ≤
      Real.exp (128 * (((m+n+1 : ℕ) : ℝ)*(h : ℝ)^2 * Real.log ((m*n : ℕ)+2) +
        (m*n-s : ℕ))) := by
…

lemma OAI.RowColumn.occupied_factor_bound line 61
lemma OAI.RowColumn.occupied_count_bound line 81
lemma OAI.RowColumn.irreducible_nontrivial line 111
lemma OAI.RowColumn.empty_hook_dimension_le line 116
lemma OAI.RowColumn.hook_lineCost line 126
lemma OAI.RowColumn.hook_sectorAlgebra_bound line 133

theorem OAI.RowColumn.occupied_dimension_ratio line 154

Source documentation

The dimension-ratio half of the occupied main, now for the literal occupied subset and all prescribed row and column embeddings.

theorem occupied_dimension_ratio (m n : ℕ) (Ω : Finset (Board m n)) [Nonempty Ω]
    (a : YoungDiagram) (e : Ω ≃ Cell a) (h : ℕ) (hh : 1 ≤ h) (H : InHook a h)
    (r c u v : ℕ)
    (ρ : Representation ℂ (rowGroup Ω) (EuclideanSpace ℂ (Fin r)))
    (τ : Representation ℂ (columnGroup Ω) (EuclideanSpace ℂ (Fin c)))
    (hρ : IsUnitary ρ) (hτ : IsUnitary τ)
    (I : Fin u → EuclideanSpace ℂ (Fin r) →ₗᵢ[ℂ] hilbertSpace a)
    (J : Fin v → EuclideanSpace ℂ (Fin c) →ₗᵢ[ℂ] hilbertSpace a)
    (hI : ∀ i, Intertwines (V := EuclideanSpace ℂ (Fin r)) (W := hilbertSpace a)
…

Mentions: OAI.RowColumn.Board, OAI.RowColumn.InHook, OAI.RowColumn.rowGroup, OAI.RowColumn.columnGroup, OAI.RowColumn.Intertwines

theorem OAI.RowColumn.occupied_overlap_endpoint line 203
Source documentation
thm:occupied (weighted.tex:76–84), including the empty occupied subset, arbitrary deletion layout and every orthogonal multiplicity copy. The absolute constant is 128; dimensions, unnormalized trace and operator norm are literal.
Distinct definitions of this name: ComparatorChallenges/OccupiedOverlap.lean:260 (different declaration text). Qualify references as OAI.RowColumn.occupied_overlap_endpoint@path.
```
theorem occupied_overlap_endpoint : OccupiedOverlapEndpoint := by
…
```
Mentions: OAI.RowColumn.OccupiedOverlapEndpoint
theorem OAI.RowColumn.occupied_overlap line 274
Source documentation
The occupied row-column overlap bound.
Distinct definitions of this name: ComparatorChallenges/OccupiedOverlap.lean:263 (same statement text; different proof or body). Qualify references as OAI.RowColumn.occupied_overlap@path.
```
theorem RowColumn.occupied_overlap : RowColumn.OccupiedOverlapEndpoint :=
…
```
Mentions: OAI.RowColumn.OccupiedOverlapEndpoint