ComponentFactorial.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Factorial costs of components in the arrangement graph

theorem OAI.Ostmann.component_factorial_le line 15
Source documentation
Assigning a*m labeled positions to a blocks gives the factorial inequality used in the count of bad arrangements.
```
theorem component_factorial_le (a m : ℕ) :
    (a * m).factorial ≤ m.factorial ^ a * a ^ (a * m) := by
…
```
theorem OAI.Ostmann.component_log_cost line 35

theorem OAI.Ostmann.component_entropy_bound line 45

Source documentation

The sum of a-1 is exactly the number of leaves minus the number of components, so the entropy cost is controlled by this deficit.

theorem component_entropy_bound {I : Type*} [Fintype I]
    (a : I → ℕ) (r : ℕ) (ha : ∀ i, 1 ≤ a i) (hsum : ∑ i, a i = r) :
    (∑ i, (a i : ℝ) * Real.log (a i)) ≤
      ((r : ℝ) - Fintype.card I) * (Real.log r + 1) := by
…

theorem OAI.Ostmann.component_factorial_product_bound line 63

Source documentation

Product of the component assignment counts, with the cost expressed through the deficit in the number of components.

theorem component_factorial_product_bound {I : Type*} [Fintype I]
    (a : I → ℕ) (r m : ℕ) (ha : ∀ i, 1 ≤ a i) (hsum : ∑ i, a i = r) :
    (∏ i, ((a i * m).factorial : ℝ)) ≤
      (m.factorial : ℝ) ^ r *
        Real.exp ((m : ℝ) * ((r : ℝ) - Fintype.card I) * (Real.log r + 1)) := by
…