LocalOccupationAverage.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.joinOccupation line 14

Source documentation

Reassemble two occupation vectors on the complementary variable classes.

def joinOccupation (side : σ → Bool)
    (M : {i // side i = true} → ℕ) (N : {i // ¬ side i = true} → ℕ) : σ → ℕ :=
…

theorem OAI.Problem335.joinOccupation_true line 19
theorem OAI.Problem335.joinOccupation_false line 25
theorem OAI.Problem335.factorialMonomial_joinOccupation line 30
def OAI.Problem335.partitionCompositionMean line 42
Source documentation
The actual finite uniform average, not an assumed moment functional.
```
def partitionCompositionMean (side : σ → Bool) (f : (σ → ℕ) → ℝ) (a b : ℕ) : ℝ := by
…
```
theorem OAI.Problem335.FactorialExpansion.partitionCompositionMean_eq line 53

theorem OAI.Problem335.FactorialExpansion.partition_geometric_monomial line 78

Source documentation

The two means give one coordinate-wise geometric factorial monomial.

theorem partition_geometric_monomial (side : σ → Bool) (d : σ → ℕ) (A B : ℝ) :
    (∏ i, (d i).factorial * (if side i = true then A else B) ^ d i : ℝ) =
      (∏ i : {i // side i = true}, ((d i).factorial : ℝ)) *
      (∏ i : {i // ¬ side i = true}, ((d i).factorial : ℝ)) *
      (A ^ (∑ i : {i // side i = true}, d i) *
       B ^ (∑ i : {i // ¬ side i = true}, d i)) := by
…

theorem OAI.Problem335.FactorialExpansion.partitionCompositionMean_le line 96

Source documentation

Upper occupation comparison for every concrete nonnegative factorial expansion. No total-order restriction is necessary for this upper bound.

theorem partitionCompositionMean_le (F : FactorialExpansion f S D)
    (side : σ → Bool) [Nonempty {i // side i = true}] [Nonempty {i // ¬ side i = true}]
    (a b : ℕ) :
    Problem335.partitionCompositionMean side (fun M => (f M : ℝ)) a b ≤
      ∑ j, (F.coeff j : ℝ) * ∏ i, ((F.degree j i).factorial : ℝ) *
        (if side i = true then (a : ℝ) / Fintype.card {i // side i = true}
         else (b : ℝ) / Fintype.card {i // ¬ side i = true}) ^ F.degree j i := by
…

Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.partitionCompositionMean