OAI/Algebra/DepthFive/OccupationExpansion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.factorialExpansionValue line 12

   Source documentation

   A finite expansion in the multivariate falling-factorial basis.

   def factorialExpansionValue {ι J : Type*} [Fintype ι]
       (s : Finset J) (c : J → ℝ) (d : J → ι → ℕ) (M : ι →₀ ℕ) : ℝ :=
   …

2. def OAI.Problem335.geometricExpansionValue line 17

   Source documentation

   The corresponding product-geometric factorial-moment expression.

   def geometricExpansionValue {ι J : Type*} [Fintype ι]
       (s : Finset J) (c : J → ℝ) (d : J → ι → ℕ) (G : ℝ) : ℝ :=
   …

3. def OAI.Problem335.compositionExpansionMean line 22

   Source documentation

   Average over the finite uniform weak-composition space.

   def compositionExpansionMean {ι J : Type*} [Fintype ι] [DecidableEq ι]
       (s : Finset J) (c : J → ℝ) (d : J → ι → ℕ) (t : ℕ) : ℝ :=
   …

4. theorem OAI.Problem335.compositionExpansionMean_eq line 29

   Source documentation

   Linearity and the exact occupation factorial-moment identity.

   theorem compositionExpansionMean_eq {ι J : Type*} [Fintype ι] [DecidableEq ι]
       [Nonempty ι] (s : Finset J) (c : J → ℝ) (d : J → ι → ℕ) (t : ℕ) :
       compositionExpansionMean s c d t =
         ∑ j ∈ s, (c j * ∏ i, (d j i).factorial : ℝ) *
           ((t.descFactorial (∑ i, d j i) : ℝ) /
             ((Fintype.card ι).ascFactorial (∑ i, d j i) : ℝ)) := by
   …

   Mentions: OAI.Problem335.compositionExpansionMean

5. theorem OAI.Problem335.compositionExpansionMean_le_geometric line 44

   Source documentation

   Upper geometric comparison, including zero total occupation and arbitrary orders.

   theorem compositionExpansionMean_le_geometric {ι J : Type*} [Fintype ι]
       [DecidableEq ι] [Nonempty ι] (s : Finset J) (c : J → ℝ) (d : J → ι → ℕ)
       (t : ℕ) (hc : ∀ j ∈ s, 0 ≤ c j) :
       compositionExpansionMean s c d t ≤
         geometricExpansionValue s c d ((t : ℝ) / Fintype.card ι) := by
   …

   Mentions: OAI.Problem335.compositionExpansionMean, OAI.Problem335.geometricExpansionValue

6. theorem OAI.Problem335.exp_mul_geometric_le_compositionExpansionMean line 55

   Source documentation

   The lower geometric comparison depends only on a uniform total-order bound.

   theorem exp_mul_geometric_le_compositionExpansionMean {ι J : Type*} [Fintype ι]
       [DecidableEq ι] [Nonempty ι] (s : Finset J) (c : J → ℝ) (d : J → ι → ℕ)
       {t H : ℕ} (ht : 0 < t) (hH : 2 * H ≤ t) (hc : ∀ j ∈ s, 0 ≤ c j)
       (hd : ∀ j ∈ s, ∑ i, d j i ≤ H) :
       Real.exp (-(H : ℝ) ^ 2 / t - (H : ℝ) ^ 2 / (2 * Fintype.card ι)) *
         geometricExpansionValue s c d ((t : ℝ) / Fintype.card ι) ≤
           compositionExpansionMean s c d t := by
   …

   Mentions: OAI.Problem335.geometricExpansionValue, OAI.Problem335.compositionExpansionMean

7. def OAI.Problem335.twoGroupCompositionExpansionMean line 68

   Source documentation

   Uniform averages in two independent weak-composition groups, with a shared term index.

   def twoGroupCompositionExpansionMean {ι κ J : Type*} [Fintype ι] [DecidableEq ι]
       [Fintype κ] [DecidableEq κ] (s : Finset J) (c : J → ℝ)
       (d : J → ι → ℕ) (e : J → κ → ℕ) (a b : ℕ) : ℝ :=
   …

8. def OAI.Problem335.twoGroupGeometricExpansionValue line 77

   Source documentation

   The product-geometric expression for a two-group factorial expansion.

   def twoGroupGeometricExpansionValue {ι κ J : Type*} [Fintype ι] [Fintype κ]
       (s : Finset J) (c : J → ℝ) (d : J → ι → ℕ) (e : J → κ → ℕ)
       (A B : ℝ) : ℝ :=
   …

9. theorem OAI.Problem335.twoGroupCompositionExpansionMean_eq line 83
10. theorem OAI.Problem335.twoGroupCompositionExpansionMean_le_geometric line 115

    Source documentation

    Actual upper occupation comparison for nonnegative two-group expansions.

    theorem twoGroupCompositionExpansionMean_le_geometric {ι κ J : Type*}
        [Fintype ι] [DecidableEq ι] [Nonempty ι]
        [Fintype κ] [DecidableEq κ] [Nonempty κ]
        (s : Finset J) (c : J → ℝ) (d : J → ι → ℕ) (e : J → κ → ℕ) (a b : ℕ)
        (hc : ∀ j ∈ s, 0 ≤ c j) :
        twoGroupCompositionExpansionMean s c d e a b ≤
          twoGroupGeometricExpansionValue s c d e
            ((a : ℝ) / Fintype.card ι) ((b : ℝ) / Fintype.card κ) := by
    …

    Mentions: OAI.Problem335.twoGroupCompositionExpansionMean, OAI.Problem335.twoGroupGeometricExpansionValue

11. theorem OAI.Problem335.exp_mul_geometric_le_twoGroupCompositionExpansionMean line 130

    Source documentation

    Actual uniform lower occupation comparison for nonnegative two-group expansions.

    theorem exp_mul_geometric_le_twoGroupCompositionExpansionMean {ι κ J : Type*}
        [Fintype ι] [DecidableEq ι] [Nonempty ι]
        [Fintype κ] [DecidableEq κ] [Nonempty κ]
        (s : Finset J) (c : J → ℝ) (d : J → ι → ℕ) (e : J → κ → ℕ)
        {a b H J₀ : ℕ} (ha : 0 < a) (hb : 0 < b) (hH : 2 * H ≤ a) (hJ : 2 * J₀ ≤ b)
        (hc : ∀ j ∈ s, 0 ≤ c j) (hd : ∀ j ∈ s, ∑ i, d j i ≤ H)
        (he : ∀ j ∈ s, ∑ i, e j i ≤ J₀) :
        Real.exp ((-(H : ℝ) ^ 2 / a - (H : ℝ) ^ 2 / (2 * Fintype.card ι)) +
            (-(J₀ : ℝ) ^ 2 / b - (J₀ : ℝ) ^ 2 / (2 * Fintype.card κ))) *
          twoGroupGeometricExpansionValue s c d e
            ((a : ℝ) / Fintype.card ι) ((b : ℝ) / Fintype.card κ) ≤
          twoGroupCompositionExpansionMean s c d e a b := by
    …

    Mentions: OAI.Problem335.twoGroupGeometricExpansionValue, OAI.Problem335.twoGroupCompositionExpansionMean