RelaxedWordBridge.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.MomentPairing.relaxedWordWeight_eq_isolatedWeight line 13

Source documentation

The averaged pairing summand is exactly the canonical Boolean-word weight.

theorem relaxedWordWeight_eq_isolatedWeight {L : ℕ}
    (isV w : Fin (L + 1) → Bool) (N α β : ℝ) :
    relaxedWordWeight isV N α β (fun i => boolKindEquiv (w i)) =
      IsolatedWeight.weight (BalancedSchedule.internalEdges (L + 1))
        (Finset.univ.filter (fun i => isV i = true))
        BalancedSchedule.adjacent α⁻¹ β N⁻¹ w := by
…

Mentions: OAI.Problem335.MomentPairing.relaxedWordWeight, OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.BalancedSchedule.internalEdges, OAI.Problem335.BalancedSchedule.adjacent

theorem OAI.Problem335.MomentPairing.sum_relaxedWordWeight_eq_isolatedWeight line 57

Source documentation

Reindexing all pairing words through the canonical Boolean equivalence.

theorem sum_relaxedWordWeight_eq_isolatedWeight {L : ℕ}
    (isV : Fin (L + 1) → Bool) (N α β : ℝ) :
    (∑ τ : Fin (L + 1) → Kind, relaxedWordWeight isV N α β τ) =
      ∑ w : Fin (L + 1) → Bool,
        IsolatedWeight.weight (BalancedSchedule.internalEdges (L + 1))
          (Finset.univ.filter (fun i => isV i = true))
          BalancedSchedule.adjacent α⁻¹ β N⁻¹ w := by
…

Mentions: OAI.Problem335.MomentPairing.relaxedWordWeight, OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.BalancedSchedule.internalEdges, OAI.Problem335.BalancedSchedule.adjacent