PairingSourceAverage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The canonical finite source sum enters the normalized relaxed pairing bound with exactly one source dimension and no assumed occupation estimate.

theorem OAI.Problem335.MomentPairing.bidegree_source_average_eq_occupationPathMean line 18

theorem OAI.Problem335.MomentPairing.sum_bidegree_source_local_moments_le line 39

Source documentation

Concrete source reindexing, finite occupation comparison, normalization, and relaxation. In particular, the source cardinality occurs only once.

theorem sum_bidegree_source_local_moments_le
    (side : Fin (L + 1) → Bool)
    [Nonempty {v : Fin (L + 1) × (γ × γ) // side v.1 = true}]
    [Nonempty {v : Fin (L + 1) × (γ × γ) // ¬ side v.1 = true}]
    (a b : ℕ) (ha : 0 < a)
    [Fintype {d : (Fin (L + 1) × (γ × γ)) →₀ ℕ //
      Finsupp.weight (bidegreeWeight (fun v => side v.1)) d = (a, b)}]
    (endpoint : γ) :
    (∑ d : {d : (Fin (L + 1) × (γ × γ)) →₀ ℕ //
        Finsupp.weight (bidegreeWeight (fun v => side v.1)) d = (a, b)},
      ∑ x : {x : Fin L → Labels γ // Compatible endpoint x},
        ∏ t, LocalMoments.localPolynomial (side t) (fun y => d.val (t, y))
…

Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.MomentPairing.Compatible, OAI.Problem335.LocalMoments.localPolynomial