LocalMomentWeights.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Normalization of the local geometric occupation moments in the four-path trace expansion. Missing derivative occupations are handled by local-polynomial identities, preserving the repeated-coordinate second moment rather than treating it as a product of independent moments.

def OAI.Problem335.LocalMomentWeights.moment line 17
Source documentation
isD denotes the nonzero-difference pairing. same is relevant only in its complementary pairing, where the two selected coordinates may coincide.
```
def moment (isV isD same : Bool) (A B : ℝ) : ℝ :=
…
```
def OAI.Problem335.LocalMomentWeights.scale line 25
Source documentation
The square of the first-moment factor at a layer.
```
def scale (isV : Bool) (A B : ℝ) : ℝ :=
…
```
def OAI.Problem335.LocalMomentWeights.weight line 29
Source documentation
The exact local weights after division by the first-moment square.
```
def weight (isV isD same : Bool) (alpha beta : ℝ) : ℝ :=
…
```
lemma OAI.Problem335.LocalMomentWeights.scale_pos line 35
lemma OAI.Problem335.LocalMomentWeights.weight_nonneg line 39
theorem OAI.Problem335.LocalMomentWeights.moment_eq_scale_mul_weight line 45
Source documentation
Repeated-coordinate geometric second moments give the additional term alpha⁻¹ or beta exactly.
```
theorem moment_eq_scale_mul_weight (isV isD same : Bool) {A B : ℝ}
    (hA : 0 < A) (hB : 0 ≤ B) :
    moment isV isD same A B =
      scale isV A B * weight isV isD same (A / (A + 1)) (B / (B + 1)) := by
…
```
Mentions: OAI.Problem335.LocalMomentWeights.moment, OAI.Problem335.LocalMomentWeights.scale, OAI.Problem335.LocalMomentWeights.weight
lemma OAI.Problem335.LocalMomentWeights.moment_div_scale line 55
lemma OAI.Problem335.LocalMomentWeights.mean_ratio line 63
Source documentation
The normalized means agree with the original degree/cardinality ratios.
```
lemma mean_ratio {a v : ℝ} (hv : 0 < v) (ha : 0 ≤ a) :
    (a / v) / (a / v + 1) = a / (a + v) := by
…
```

theorem OAI.Problem335.LocalMomentWeights.prod_moment_eq line 70

Source documentation

A pointwise normalization can be factored out of the entire layer product.

theorem prod_moment_eq {ι : Type*} (s : Finset ι)
    (isV isD same : ι → Bool) {A B : ℝ} (hA : 0 < A) (hB : 0 ≤ B) :
    (∏ i ∈ s, moment (isV i) (isD i) (same i) A B) =
      (∏ i ∈ s, scale (isV i) A B) *
      ∏ i ∈ s, weight (isV i) (isD i) (same i) (A / (A + 1)) (B / (B + 1)) := by
…

Mentions: OAI.Problem335.LocalMomentWeights.moment, OAI.Problem335.LocalMomentWeights.scale, OAI.Problem335.LocalMomentWeights.weight

theorem OAI.Problem335.LocalMomentWeights.prod_scale_eq line 79

Source documentation

The product of the local normalization factors is exactly mu^2.

theorem prod_scale_eq {ι : Type*} (s : Finset ι) (isV : ι → Bool) (A B : ℝ) :
    (∏ i ∈ s, scale (isV i) A B) =
      (A ^ (s.filter (fun i => isV i = true)).card *
        (B + 1) ^ (s.filter (fun i => isV i = false)).card) ^ 2 := by
…

Mentions: OAI.Problem335.LocalMomentWeights.scale

theorem OAI.Problem335.LocalMomentWeights.prod_moment_eq_mu_sq_mul line 95

Source documentation

Full local-weight normalization for a fixed four-path pairing pattern.

theorem prod_moment_eq_mu_sq_mul {ι : Type*} (s : Finset ι)
    (isV isD same : ι → Bool) {A B : ℝ} (hA : 0 < A) (hB : 0 ≤ B) :
    (∏ i ∈ s, moment (isV i) (isD i) (same i) A B) =
      (A ^ (s.filter (fun i => isV i = true)).card *
        (B + 1) ^ (s.filter (fun i => isV i = false)).card) ^ 2 *
      ∏ i ∈ s, weight (isV i) (isD i) (same i) (A / (A + 1)) (B / (B + 1)) := by
…

Mentions: OAI.Problem335.LocalMomentWeights.moment, OAI.Problem335.LocalMomentWeights.weight