EncodingHomogeneous.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.EncodingDegree.weightedHomogeneous_expansion line 15

Source documentation

A coefficient expansion has weighted degree given by the sum of the weights of its assigned vector blocks. The coefficients can be arbitrary.

theorem weightedHomogeneous_expansion (c : (S → K) → R) (blocks : S → B)
    (w : B → ℕ) :
    MvPolynomial.IsWeightedHomogeneous (fun x : B × K => w x.1)
      (∑ k : S → K, MvPolynomial.C (c k) *
        ∏ i : S, MvPolynomial.X (blocks i, k i))
      (∑ i : S, w (blocks i)) := by
…

theorem OAI.Problem346.EncodingDegree.blockHomogeneous_expansion line 30

Source documentation

The degree in one block is exactly the number of occurrences of that block.

theorem blockHomogeneous_expansion [DecidableEq B]
    (c : (S → K) → R) (blocks : S → B) (b : B) :
    MvPolynomial.IsWeightedHomogeneous
      (fun x : B × K => if x.1 = b then 1 else 0)
      (∑ k : S → K, MvPolynomial.C (c k) *
        ∏ i : S, MvPolynomial.X (blocks i, k i))
      (Finset.univ.filter (fun i => blocks i = b)).card := by
…

theorem OAI.Problem346.EncodingDegree.sum_weight_update line 42
Source documentation
Changing a single assigned block changes the weight by exactly the corresponding source/destination contribution. This form avoids truncated subtraction.
```
theorem sum_weight_update (blocks : S → B) (w : B → ℕ)
    (i : S) (b : B) :
    (∑ j : S, w ((Function.update blocks i b) j)) + w (blocks i) =
      (∑ j : S, w (blocks j)) + w b := by
…
```