OAI/Algebra/DepthFive/FactorialOccupation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem335.FactorialExpansion.uniformMean line 14

    Source documentation

    Uniform weak-composition mean of an actual natural-valued function.

    def uniformMean (f : (σ → ℕ) → ℕ) (t : ℕ) : ℝ :=
…
  2. def OAI.Problem335.FactorialExpansion.geometricMean line 19

    Source documentation

    Product-geometric evaluation of a nonnegative factorial expansion.

    def geometricMean {f : (σ → ℕ) → ℕ} {S : Finset σ} {D : ℕ}
    (F : FactorialExpansion f S D) (G : ℝ) : ℝ :=
…

    Mentions: OAI.Problem335.FactorialExpansion

  3. theorem OAI.Problem335.FactorialExpansion.uniformMean_eq line 23
  4. theorem OAI.Problem335.FactorialExpansion.uniformMean_le_geometric line 33
  5. theorem OAI.Problem335.FactorialExpansion.exp_mul_geometric_le_uniformMean line 39
  6. def OAI.Problem335.FactorialExpansion.twoGroupMean line 51

    Source documentation

    Independent uniform means, keeping the two occupation totals fixed separately.

    def twoGroupMean (f : ((ι ⊕ κ) → ℕ) → ℕ) (a b : ℕ) : ℝ :=
…
  7. def OAI.Problem335.FactorialExpansion.twoGroupGeometricMean line 58
  8. theorem OAI.Problem335.FactorialExpansion.twoGroupMean_eq line 63
  9. theorem OAI.Problem335.FactorialExpansion.twoGroupMean_le_geometric line 78
  10. theorem OAI.Problem335.FactorialExpansion.exp_mul_geometric_le_twoGroupMean line 87