LineExpansion.lean`

62 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CoordinateSweeps.MomentExpansion.tensorMoment line 19
Source comment
The moment functional of independent line variables, defined algebraically so only the finitely many moments actually used need be integrable.
```
def tensorMoment (m : L → ℕ → ℝ) : MvPolynomial L ℝ →ₗ[ℝ] ℝ :=
…
```
theorem OAI.CoordinateSweeps.MomentExpansion.tensorMoment_monomial line 23
theorem OAI.CoordinateSweeps.MomentExpansion.tensorMoment_one line 35
theorem OAI.CoordinateSweeps.MomentExpansion.tensorMoment_sum line 41
theorem OAI.CoordinateSweeps.MomentExpansion.tensorMoment_mul_disjoint line 48
theorem OAI.CoordinateSweeps.MomentExpansion.tensorMoment_X_pow line 73

theorem OAI.CoordinateSweeps.MomentExpansion.tensorMoment_prod_separated line 83

Source comment

Factorization of arbitrary polynomials, one for each distinct line.

theorem tensorMoment_prod_separated (m : L → ℕ → ℝ) (hm : ∀ l, m l 0 = 1)
    (S : Finset L) (p : L → MvPolynomial L ℝ) (hp : ∀ l ∈ S, (p l).vars ⊆ {l}) :
    tensorMoment m (∏ l ∈ S, p l) = ∏ l ∈ S, tensorMoment m (p l) := by
…

Mentions: OAI.CoordinateSweeps.MomentExpansion.tensorMoment

def OAI.CoordinateSweeps.MomentExpansion.shiftedMoment line 103
Source comment
The exact linear functional for a fixed subset of the non-good paths. Translation by -1 retains all correlations between repeated uses of a line.
```
def shiftedMoment (m : L → ℕ → ℝ) (r : L → ℕ) : MvPolynomial L ℝ →ₗ[ℝ] ℝ :=
…
```
def OAI.CoordinateSweeps.MomentExpansion.lineCenteredMoment line 108
theorem OAI.CoordinateSweeps.MomentExpansion.vars_X_centered_power line 117
theorem OAI.CoordinateSweeps.MomentExpansion.tensorMoment_X_centered_power line 126
theorem OAI.CoordinateSweeps.MomentExpansion.shiftedMoment_monomial line 142
Source comment
Repeated uses of one line are collected into a SINGLE mixed centered moment.
```
theorem shiftedMoment_monomial (m : L → ℕ → ℝ) (hm : ∀ l, m l 0 = 1)
    (r : L → ℕ) (d : L →₀ ℕ) (a : ℝ) :
    shiftedMoment m r (monomial d a) = a * ∏ l, lineCenteredMoment m l (r l) (d l) := by
…
```
Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.MomentExpansion.shiftedMoment, OAI.CoordinateSweeps.MomentExpansion.lineCenteredMoment
def OAI.CoordinateSweeps.MomentExpansion.NonnegCoeffs line 158
Source comment
Coefficientwise nonnegativity, used only for the positive centered expansion.
```
def NonnegCoeffs (p : MvPolynomial L ℝ) : Prop := ∀ d, 0 ≤ p.coeff d
…
```
theorem OAI.CoordinateSweeps.MomentExpansion.nonnegCoeffs_one line 161
theorem OAI.CoordinateSweeps.MomentExpansion.NonnegCoeffs.add line 167
theorem OAI.CoordinateSweeps.MomentExpansion.NonnegCoeffs.mul line 173
theorem OAI.CoordinateSweeps.MomentExpansion.nonnegCoeffs_X line 180
theorem OAI.CoordinateSweeps.MomentExpansion.nonnegCoeffs_prod line 186
theorem OAI.CoordinateSweeps.MomentExpansion.nonnegCoeffs_sum line 196
theorem OAI.CoordinateSweeps.MomentExpansion.shiftedMoment_abs_le_eval line 204
Source comment
Exact tensor moment estimate. Its potential premise is local in each line and each used degree, not independence of particle factors.
```
theorem shiftedMoment_abs_le_eval (m : L → ℕ → ℝ) (hm : ∀ l, m l 0 = 1)
    (r : L → ℕ) (p : MvPolynomial L ℝ) (hp : NonnegCoeffs p)
    (C t : ℝ)
    (hb : ∀ d ∈ p.support, ∀ l,
      |lineCenteredMoment m l (r l) (d l)| ≤ C^(r l) * t^(d l)) :
    |shiftedMoment m r p| ≤ C^(∑ l, r l) * MvPolynomial.eval (fun _ => t) p := by
…
```
Mentions: OAI.CoordinateSweeps.MomentExpansion.NonnegCoeffs, OAI.CoordinateSweeps.MomentExpansion.lineCenteredMoment, OAI.CoordinateSweeps.MomentExpansion.shiftedMoment
def OAI.CoordinateSweeps.MomentExpansion.pathExpansion line 238
Source comment
Positive expansion for a centered particle factor. This is a sum over NONEMPTY subsets of its stages; no independence of particle factors is used.
```
def pathExpansion (S : Finset J) (f : J → L) : MvPolynomial L ℝ :=
…
```
theorem OAI.CoordinateSweeps.MomentExpansion.pathExpansion_eq line 242
theorem OAI.CoordinateSweeps.MomentExpansion.pathExpansion_nonneg line 252
theorem OAI.CoordinateSweeps.MomentExpansion.pathExpansion_degree line 257
theorem OAI.CoordinateSweeps.MomentExpansion.pathExpansion_eval line 270
theorem OAI.CoordinateSweeps.MomentExpansion.pathExpansion_shift line 276
def OAI.CoordinateSweeps.MomentExpansion.goodExpansion line 283
Source comment
Combined centered expansion, with the actual same variable on a shared line.
```
def goodExpansion (G : Finset I) (path : I → J → L) : MvPolynomial L ℝ :=
…
```
theorem OAI.CoordinateSweeps.MomentExpansion.goodExpansion_nonneg line 287
theorem OAI.CoordinateSweeps.MomentExpansion.goodExpansion_degree line 292
theorem OAI.CoordinateSweeps.MomentExpansion.goodExpansion_eval line 298
theorem OAI.CoordinateSweeps.MomentExpansion.centered_power_le line 304
Source comment
Uniform estimate for (1+C*x)^b-1, retaining one small factor per particle.
```
theorem centered_power_le (C x : ℝ) (hC : 0 ≤ C) (hx : 0 ≤ x) (hx1 : x ≤ 1) (b : ℕ) :
    (1+C*x)^b-1 ≤ ((1+C)^b-1)*x := by
…
```
theorem OAI.CoordinateSweeps.MomentExpansion.goodExpansion_eval_le line 319
theorem OAI.CoordinateSweeps.MomentExpansion.goodExpansion_moment_le line 336
def OAI.CoordinateSweeps.MomentExpansion.incidenceCount line 357
theorem OAI.CoordinateSweeps.MomentExpansion.tensorMoment_path_monomial line 362
theorem OAI.CoordinateSweeps.MomentExpansion.shiftedMoment_goodExpansion_eq line 389
Source comment
Exact alternation identity. The summation set is the omitted subset of good particles, so its sign is (-1)^|A|. This is source (10)'s inside-expectation formula, with all shared-line correlations retained by the linear functional.
```
theorem shiftedMoment_goodExpansion_eq (m : L → ℕ → ℝ) (r : L → ℕ)
    (G : Finset I) (path : I → J → L) :
    shiftedMoment m r (goodExpansion G path) =
      ∑ A ∈ G.powerset, (-1 : ℝ)^A.card * ∏ l, m l (r l+incidenceCount (G\A) path l) := by
…
```
Mentions: OAI.CoordinateSweeps.MomentExpansion.shiftedMoment, OAI.CoordinateSweeps.MomentExpansion.goodExpansion, OAI.CoordinateSweeps.MomentExpansion.incidenceCount
theorem OAI.CoordinateSweeps.integral_gamma_eq line 421
theorem OAI.CoordinateSweeps.gamma_mgf line 435
theorem OAI.CoordinateSweeps.gamma_mgf_integrable line 448
theorem OAI.CoordinateSweeps.gamma_centered_mgf line 454
theorem OAI.CoordinateSweeps.gamma_centered_mgf_integrable line 467
theorem OAI.CoordinateSweeps.log_mgf_bound line 473
theorem OAI.CoordinateSweeps.gamma_centered_mgf_le line 485
theorem OAI.CoordinateSweeps.abs_pow_le_exp_sum line 493
Source comment
Pointwise exponential domination, used to obtain the actual centered moments without a separate probabilistic Chernoff axiom.
```
theorem abs_pow_le_exp_sum (x : ℝ) (u : ℕ) {t : ℝ} (ht : 0 < t) :
    |x|^u ≤ ((u : ℝ)/t)^u * (exp (t*x) + exp (-t*x)) := by
…
```
theorem OAI.CoordinateSweeps.abs_pow_integrable line 502
theorem OAI.CoordinateSweeps.abs_pow_integral_le line 512

theorem OAI.CoordinateSweeps.gamma_abs_centered_moment_le line 525

Source comment

A centered gamma moment in the range needed by every light line.

theorem gamma_abs_centered_moment_le {a : ℝ} (ha : 0 < a) {u : ℕ}
    (hu : 1 ≤ u) (hua : 4*(u : ℝ) ≤ a) :
    (∫ x, |x-a|^u ∂gammaMeasure a 1) ≤
      (2 * exp 2 * Real.sqrt (a*u))^u := by
…

Mentions: OAI.CoordinateSweeps.a

theorem OAI.CoordinateSweeps.integral_gamma_congr line 569

Source comment

No restriction at the density's null endpoint is needed.

theorem integral_gamma_congr {a r : ℝ} (ha : 0 < a) (hr : 0 < r)
    {f g : ℝ → ℝ} (hfg : ∀ x, 0 < x → f x = g x) :
    (∫ x, f x ∂gammaMeasure a r) = ∫ x, g x ∂gammaMeasure a r := by
…

Mentions: OAI.CoordinateSweeps.a

theorem OAI.CoordinateSweeps.gamma_inverse_tilt line 579

Source comment

The exact inverse-power density tilt used, with all gamma laws concrete.

theorem gamma_inverse_tilt {a m : ℝ} (k : ℕ) (hak : (k : ℝ) < a)
    (f : ℝ → ℝ) :
    (∫ x, (m/x)^k * f x ∂gammaMeasure a 1) =
      (m^k * Gamma (a-k) / Gamma a) * (∫ x, f x ∂gammaMeasure (a-k) 1) := by
…

Mentions: OAI.CoordinateSweeps.a

theorem OAI.CoordinateSweeps.gamma_ratio_descFactorial line 600

Source comment

The gamma-ratio is the exact falling factorial, not an asymptotic.

theorem gamma_ratio_descFactorial {n k : ℕ} (hk : k ≤ n) :
    Gamma ((n : ℝ)+1-k) / Gamma ((n : ℝ)+1) = (n.descFactorial k : ℝ)⁻¹ := by
…

theorem OAI.CoordinateSweeps.gamma_light_line_identity line 613

Source comment

The first equality of manuscript (11).

theorem gamma_light_line_identity {m h u v : ℕ} (hm : 0 < m) (huv : h+u+v ≤ m) :
    (∫ x, ((m : ℝ)/x)^v * |(m : ℝ)/x-1|^u
      ∂gammaMeasure ((m-h : ℕ)+1) 1) =
      ((m : ℝ)^(u+v) / ((m-h).descFactorial (u+v) : ℝ)) *
      (∫ x, |1-x/(m : ℝ)|^u ∂gammaMeasure ((m-h : ℕ)+1-(u+v : ℕ)) 1) := by
…

theorem OAI.CoordinateSweeps.gamma_normalized_moment_le line 636

Source comment

Scale and bias estimate for the tilted gamma law.

theorem gamma_normalized_moment_le {a m η : ℝ} (ha : 0 < a) (hm : 0 < m)
    (hη : 0 ≤ η) (hη1 : η ≤ 1) {u : ℕ} (hu : 1 ≤ u)
    (hua : 4*(u : ℝ) ≤ a) (ham : a ≤ m) (huη : (u : ℝ) ≤ m*η)
    (hbias : |1-a/m| ≤ η) :
    (∫ x, |1-x/m|^u ∂gammaMeasure a 1) ≤
      (8 * exp 2 * Real.sqrt η)^u := by
…

Mentions: OAI.CoordinateSweeps.a

theorem OAI.CoordinateSweeps.light_prefactor_le line 719
Source comment
Uniform bound for the inverse-gamma prefactor, a light line cannot have more than half of its sites assigned.
```
theorem light_prefactor_le {m h k : ℕ} (hm : 0 < m) (hk : 2*(h+k) ≤ m) :
    (m : ℝ)^k / ((m-h).descFactorial k : ℝ) ≤ 2^k := by
…
```

theorem OAI.CoordinateSweeps.gamma_light_line_bound line 743

Source comment

The light-line estimate (11), with an explicit absolute constant.

theorem gamma_light_line_bound {m h u v : ℕ} (hm : 0 < m) {η : ℝ}
    (hη : 0 ≤ η) (hηsmall : η ≤ 1/8)
    (hlight : ((h+u+v : ℕ) : ℝ) ≤ (m : ℝ)*η) :
    (∫ x, ((m : ℝ)/x)^v * |(m : ℝ)/x-1|^u
      ∂gammaMeasure ((m-h : ℕ)+1) 1) ≤
      (16 * exp 2)^(u+v) * (Real.sqrt η)^u := by
…

theorem OAI.CoordinateSweeps.gamma_light_line_bound_rpow line 802

Source comment

Exactly the power convention printed in manuscript (11).

theorem gamma_light_line_bound_rpow {m h u v : ℕ} (hm : 0 < m) {η : ℝ}
    (hη : 0 ≤ η) (hηsmall : η ≤ 1/8)
    (hlight : ((h+u+v : ℕ) : ℝ) ≤ (m : ℝ)*η) :
    (∫ x, ((m : ℝ)/x)^v * |(m : ℝ)/x-1|^u
      ∂gammaMeasure ((m-h : ℕ)+1) 1) ≤
      (16 * exp 2)^(u+v) * η^((u : ℝ)/2) := by
…

def OAI.CoordinateSweeps.MomentExpansion.fallingMoment line 821
Source comment
Source light-line factorial moment, with its exact finite-population shift.
```
def fallingMoment (m h n : ℕ) : ℝ := (m : ℝ)^n / ((m-h).descFactorial n : ℝ)
```
theorem OAI.CoordinateSweeps.MomentExpansion.fallingMoment_zero line 823
theorem OAI.CoordinateSweeps.MomentExpansion.fallingMoment_eq_integral line 827
Source comment
The algebraic moment is the ACTUAL inverse-gamma moment in every used degree.
```
theorem fallingMoment_eq_integral {m h n : ℕ} (hn : n ≤ m-h) :
    fallingMoment m h n =
      ∫ x, ((m : ℝ)/x)^n ∂gammaMeasure ((m-h : ℕ)+1) 1 := by
…
```
Mentions: OAI.CoordinateSweeps.MomentExpansion.fallingMoment
theorem OAI.CoordinateSweeps.MomentExpansion.fallingMoment_integrable line 839

theorem OAI.CoordinateSweeps.MomentExpansion.fallingCenteredMoment_eq_integral line 849

Source comment

Centered finite differences collect all occurrences of the SAME line.

theorem fallingCenteredMoment_eq_integral {L : Type*} (m h : L → ℕ) (l : L)
    (hm : 0 < m l) (v u : ℕ) (huv : v+u ≤ m l-h l) :
    lineCenteredMoment (fun l => fallingMoment (m l) (h l)) l v u =
      ∫ x, ((m l : ℝ)/x)^v * ((m l : ℝ)/x-1)^u
        ∂gammaMeasure ((m l-h l : ℕ)+1) 1 := by
…

Mentions: OAI.CoordinateSweeps.MomentExpansion.lineCenteredMoment, OAI.CoordinateSweeps.MomentExpansion.fallingMoment

theorem OAI.CoordinateSweeps.MomentExpansion.fallingCenteredMoment_abs_le line 880
Source comment
Source (11) now applies directly to the exact finite-difference moment. The gamma centered bound already existed; this bridge to Q's required moments is new.
```
theorem fallingCenteredMoment_abs_le {L : Type*} (m h : L → ℕ) (l : L)
    (hm : 0 < m l) (v u : ℕ) {η : ℝ} (hη : 0 ≤ η) (hηsmall : η ≤ 1/8)
    (hlight : ((h l+u+v : ℕ) : ℝ) ≤ (m l : ℝ)*η) :
    |lineCenteredMoment (fun l => fallingMoment (m l) (h l)) l v u| ≤
      (16 * exp 2)^v * ((16 * exp 2)*Real.sqrt η)^u := by
…
```
Mentions: OAI.CoordinateSweeps.MomentExpansion.lineCenteredMoment, OAI.CoordinateSweeps.MomentExpansion.fallingMoment

theorem OAI.CoordinateSweeps.MomentExpansion.goodExpansion_fallingMoment_le line 908

Source comment

Actual inverse-gamma specialization of the shared-line expansion.

theorem goodExpansion_fallingMoment_le {L I J : Type*}
    [Fintype L] [DecidableEq L] [Fintype J] [DecidableEq J]
    (m h r : L → ℕ) (hm : ∀ l, 0 < m l) (G : Finset I) (path : I → J → L)
    {η : ℝ} (hη : 0 ≤ η) (hηsmall : η ≤ 1/8)
    (hlight : ∀ l, ((h l+r l+(∑ i ∈ G, ∑ j : J, if path i j = l then 1 else 0) : ℕ) : ℝ)
      ≤ (m l : ℝ)*η) :
    |shiftedMoment (fun l => fallingMoment (m l) (h l)) r (goodExpansion G path)| ≤
      (16 * exp 2)^(∑ l, r l) * (1+16 * exp 2)^(Fintype.card J*G.card) *
        η^((G.card : ℝ)/2) := by
…

Mentions: OAI.CoordinateSweeps.MomentExpansion.shiftedMoment, OAI.CoordinateSweeps.MomentExpansion.fallingMoment, OAI.CoordinateSweeps.MomentExpansion.goodExpansion