SecondMomentPairing.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The exact four-path pairing classes are disjoint. Dropping the diagonal inequalities enlarges each class, and therefore increases every nonnegative weighted second-moment sum.

def OAI.Problem335.MomentPairing.layerLabels line 17
Source documentation
The four edge coordinates in a layer of endpoint-fixed paths.
```
def layerLabels {γ : Type*} {L : ℕ} (endpoint : γ)
    (x : Fin L → Labels γ) (t : Fin (L + 1)) : Labels (γ × γ) :=
…
```
def OAI.Problem335.MomentPairing.Compatible line 22
Source documentation
Compatibility of the four signed shifts, expressed independently in each layer.
```
def Compatible {γ : Type*} {L : ℕ} (endpoint : γ) (x : Fin L → Labels γ) : Prop :=
…
```
instance OAI.Problem335.MomentPairing.compatibleDecidable line 29
def OAI.Problem335.MomentPairing.classifyLayer line 36
Source documentation
Assign the zero difference to the normal class; all other compatible coordinate differences belong to the diagonal class.
```
def classifyLayer {γ : Type*} (x : Labels γ) : Kind := by
…
```
lemma OAI.Problem335.MomentPairing.classifyLayer_exact line 40
lemma OAI.Problem335.MomentPairing.classifyLayer_eq_of_exact line 49
def OAI.Problem335.MomentPairing.classifyWord line 57
Source documentation
The unique exact pairing word of a compatible quadruple.
```
def classifyWord {γ : Type*} {L : ℕ} (endpoint : γ)
    (x : Fin L → Labels γ) : Fin (L + 1) → Kind :=
…
```
lemma OAI.Problem335.MomentPairing.classifyWord_exact line 61
def OAI.Problem335.MomentPairing.toRelaxed line 68
Source documentation
Forgetting the noncoincidence requirement at diagonal layers embeds each compatible quadruple into its relaxed class.
```
def toRelaxed {γ : Type*} {L : ℕ} (endpoint : γ)
    (x : {x : Fin L → Labels γ // Compatible endpoint x}) :
    RelaxedPaths γ endpoint (classifyWord endpoint x.1) :=
…
```
Mentions: OAI.Problem335.MomentPairing.Compatible, OAI.Problem335.MomentPairing.classifyWord

def OAI.Problem335.MomentPairing.relaxedEncoding line 74

Source documentation

This encoding preserves all four paths, not just their pairing word.

def relaxedEncoding {γ : Type*} {L : ℕ} (endpoint : γ) :
    {x : Fin L → Labels γ // Compatible endpoint x} →
      Σ τ : Fin (L + 1) → Kind, RelaxedPaths γ endpoint τ :=
…

Mentions: OAI.Problem335.MomentPairing.Compatible

lemma OAI.Problem335.MomentPairing.relaxedEncoding_injective line 79

theorem OAI.Problem335.MomentPairing.sum_exact_le_sum_relaxed line 88

Source documentation

Summing over the exact classes is bounded by summing over all relaxed classes whenever the assigned relaxed weights are nonnegative.

theorem sum_exact_le_sum_relaxed {γ : Type*} [Fintype γ] [DecidableEq γ] {L : ℕ} (endpoint : γ)
    (W : (τ : Fin (L + 1) → Kind) → RelaxedPaths γ endpoint τ → ℝ)
    (hW : ∀ τ x, 0 ≤ W τ x) :
    (∑ x : {x : Fin L → Labels γ // Compatible endpoint x},
      W (classifyWord endpoint x.1) (toRelaxed endpoint x)) ≤
      ∑ τ : Fin (L + 1) → Kind, ∑ x : RelaxedPaths γ endpoint τ, W τ x := by
…

Mentions: OAI.Problem335.MomentPairing.Compatible, OAI.Problem335.MomentPairing.classifyWord, OAI.Problem335.MomentPairing.toRelaxed

def OAI.Problem335.MomentPairing.layerWeight line 112
Source documentation
Normal pairings retain their coordinate-coincidence factor. Diagonal pairings retain the assigned constant even after their inequality is dropped.
```
def layerWeight {γ : Type*} (c : ℝ) (τ : Kind) (x : Labels γ) : ℝ := by
…
```
lemma OAI.Problem335.MomentPairing.layerWeight_nonneg line 118

def OAI.Problem335.MomentPairing.pathWeight line 126

Source documentation

Product of the manuscript's normalized local geometric weights.

def pathWeight {γ : Type*} {L : ℕ} (isV : Fin (L + 1) → Bool)
    (α β : ℝ) (endpoint : γ) (τ : Fin (L + 1) → Kind)
    (x : Fin L → Labels γ) : ℝ :=
…

lemma OAI.Problem335.MomentPairing.pathWeight_nonneg line 131

theorem OAI.Problem335.MomentPairing.sum_compatible_pathWeight_le line 141

Source documentation

The exact weighted relaxation step in the four-path second-moment proof.

theorem sum_compatible_pathWeight_le {γ : Type*} [Fintype γ] [DecidableEq γ] {L : ℕ}
    (isV : Fin (L + 1) → Bool) {α β : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β)
    (endpoint : γ) :
    (∑ x : {x : Fin L → Labels γ // Compatible endpoint x},
      pathWeight isV α β endpoint (classifyWord endpoint x.1) x.1) ≤
    ∑ τ : Fin (L + 1) → Kind, ∑ x : RelaxedPaths γ endpoint τ,
      pathWeight isV α β endpoint τ x.1 := by
…

Mentions: OAI.Problem335.MomentPairing.Compatible, OAI.Problem335.MomentPairing.pathWeight, OAI.Problem335.MomentPairing.classifyWord

theorem OAI.Problem335.MomentPairing.sum_occupation_bound_le_relaxed line 162

Source documentation

A termwise occupation-moment bound can be summed before the pairing inequalities are relaxed; no independence of occupations is assumed here.

theorem sum_occupation_bound_le_relaxed {γ : Type*} [Fintype γ] [DecidableEq γ] {L : ℕ}
    (isV : Fin (L + 1) → Bool) {α β : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β)
    (endpoint : γ) (W : (Fin L → Labels γ) → ℝ)
    (hlocal : ∀ x, Compatible endpoint x →
      W x ≤ pathWeight isV α β endpoint (classifyWord endpoint x) x) :
    (∑ x : {x : Fin L → Labels γ // Compatible endpoint x}, W x.1) ≤
    ∑ τ : Fin (L + 1) → Kind, ∑ x : RelaxedPaths γ endpoint τ,
      pathWeight isV α β endpoint τ x.1 := by
…

Mentions: OAI.Problem335.MomentPairing.Compatible, OAI.Problem335.MomentPairing.pathWeight, OAI.Problem335.MomentPairing.classifyWord