LocalMomentPairing.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual geometric local table agrees with the canonical pairing normalization, including coincident coordinates in the normal class.

theorem OAI.Problem335.MomentPairing.localGeometricMass_eq_moment line 16

theorem OAI.Problem335.MomentPairing.prod_localGeometricMass_eq line 29

Source documentation

No compatibility assumption is needed for this algebraic identity: the canonical class always chooses the normal branch precisely when p=q.

theorem prod_localGeometricMass_eq {γ : Type*} [DecidableEq γ] {L : ℕ}
    (side : Fin (L + 1) → Bool) (A B : ℝ)
    (endpoint : γ) (x : Fin L → Labels γ) :
    (∏ t, LocalMoments.localGeometricMass (side t) (if side t then A else B)
      (layerLabels endpoint x t).p (layerLabels endpoint x t).q
      (layerLabels endpoint x t).r) =
    pathGeometricMoment side A B endpoint (classifyWord endpoint x) x := by
…

Mentions: OAI.Problem335.LocalMoments.localGeometricMass, OAI.Problem335.MomentPairing.layerLabels, OAI.Problem335.MomentPairing.pathGeometricMoment, OAI.Problem335.MomentPairing.classifyWord

theorem OAI.Problem335.MomentPairing.prod_localGeometricMass_eq_normalized line 41

theorem OAI.Problem335.MomentPairing.sum_sources_local_moments_le line 53

Source documentation

Concrete input interface for occupation averaging: the geometric RHS is the actual local polynomial table, rather than an assumed pairing weight.

theorem sum_sources_local_moments_le {ι γ : Type*} [Fintype ι]
    [Fintype γ] [DecidableEq γ] {L : ℕ}
    (side : Fin (L + 1) → Bool) {A B D : ℝ}
    (hA : 0 < A) (hB : 0 ≤ B) (hD : 0 ≤ D) (endpoint : γ)
    (C : ι → (Fin L → Labels γ) → ℝ)
    (hexpect : ∀ x, Compatible endpoint x →
      (∑ i, C i x) ≤ D *
        ∏ t, LocalMoments.localGeometricMass (side t) (if side t then A else B)
          (layerLabels endpoint x t).p (layerLabels endpoint x t).q
          (layerLabels endpoint x t).r) :
    (∑ i, ∑ x : {x : Fin L → Labels γ // Compatible endpoint x}, C i x.1) ≤
      D * pathMean side A B ^ 2 *
…

Mentions: OAI.Problem335.MomentPairing.Compatible, OAI.Problem335.LocalMoments.localGeometricMass, OAI.Problem335.MomentPairing.layerLabels, OAI.Problem335.MomentPairing.pathMean