SecondMomentNormalization.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Concrete normalization and reindexing of the geometric upper bound for four-path occupation moments.

def OAI.Problem335.MomentPairing.isDiagonal line 17
Source documentation
The diagonal flag used by the local geometric moment table.
```
def isDiagonal : Kind → Bool
  | .normal => false
  | .diagonal => true

/-- Coordinate coincidence in the normal pairing. -/
```
def OAI.Problem335.MomentPairing.coincides line 22
Source documentation
Coordinate coincidence in the normal pairing.
```
def coincides {γ : Type*} (x : Labels γ) : Bool := by
…
```
lemma OAI.Problem335.MomentPairing.localWeight_eq_layerWeight line 26
def OAI.Problem335.MomentPairing.pathMean line 35
Source documentation
The first-moment normalization for a fixed V/U layer partition.
```
def pathMean {L : ℕ} (isV : Fin (L + 1) → Bool) (A B : ℝ) : ℝ :=
…
```
lemma OAI.Problem335.MomentPairing.pathMean_pos line 39

def OAI.Problem335.MomentPairing.pathGeometricMoment line 45

Source documentation

The product of independent geometric local moments for a fixed pairing.

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

theorem OAI.Problem335.MomentPairing.pathGeometricMoment_eq line 52

Source documentation

Local normalizations multiply to precisely the square of the first moment.

theorem pathGeometricMoment_eq {γ : Type*} {L : ℕ}
    (isV : Fin (L + 1) → Bool) {A B : ℝ} (hA : 0 < A) (hB : 0 ≤ B)
    (endpoint : γ) (τ : Fin (L + 1) → Kind) (x : Fin L → Labels γ) :
    pathGeometricMoment isV A B endpoint τ x =
      pathMean isV A B ^ 2 *
        pathWeight isV (A / (A + 1)) (B / (B + 1)) endpoint τ x := by
…

Mentions: OAI.Problem335.MomentPairing.pathGeometricMoment, OAI.Problem335.MomentPairing.pathMean, OAI.Problem335.MomentPairing.pathWeight

theorem OAI.Problem335.MomentPairing.sum_compatible_geometricMoment_le line 67

Source documentation

Summing the geometric local moments over the exact compatible quadruples is bounded by the relaxed pairing sum with its common mu^2 normalization.

theorem sum_compatible_geometricMoment_le {γ : Type*} [Fintype γ] [DecidableEq γ]
    {L : ℕ} (isV : Fin (L + 1) → Bool) {A B : ℝ}
    (hA : 0 < A) (hB : 0 ≤ B) (endpoint : γ) :
    (∑ x : {x : Fin L → Labels γ // Compatible endpoint x},
      pathGeometricMoment isV A B endpoint (classifyWord endpoint x.1) x.1) ≤
    pathMean isV A B ^ 2 *
      ∑ τ : Fin (L + 1) → Kind, ∑ x : RelaxedPaths γ endpoint τ,
        pathWeight isV (A / (A + 1)) (B / (B + 1)) endpoint τ x.1 := by
…

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

theorem OAI.Problem335.MomentPairing.sum_sources_compatible_le line 82

Source documentation

After the actual occupation comparison has bounded each compatible quadruple, all source and path sums combine with only one source-size factor.

theorem sum_sources_compatible_le {ι γ : Type*} [Fintype ι]
    [Fintype γ] [DecidableEq γ] {L : ℕ}
    (isV : 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 *
        pathGeometricMoment isV A B endpoint (classifyWord endpoint x) x) :
    (∑ i, ∑ x : {x : Fin L → Labels γ // Compatible endpoint x}, C i x.1) ≤
      D * pathMean isV A B ^ 2 *
        ∑ τ : Fin (L + 1) → Kind, ∑ x : RelaxedPaths γ endpoint τ,
          pathWeight isV (A / (A + 1)) (B / (B + 1)) endpoint τ x.1 := by
…