LocalMomentPolynomials.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.LocalMoments.mass line 12
Source documentation
Squared local Fock coefficient, with true denoting differentiation.
```
def mass (derivative : Bool) (z : ℕ) : ℝ :=
…
```
def OAI.Problem335.LocalMoments.coefficient line 15
lemma OAI.Problem335.LocalMoments.mass_nonneg line 18
lemma OAI.Problem335.LocalMoments.coefficient_sq line 22
def OAI.Problem335.LocalMoments.fourCoefficient line 27
Source documentation
One layer's four factors in the second trace.
```
def fourCoefficient (derivative : Bool) (a b c d : ℕ) : ℝ :=
…
```
lemma OAI.Problem335.LocalMoments.normal_fourCoefficient line 32
Source documentation
The normal pairing has zero occupation shift.
```
lemma normal_fourCoefficient (derivative : Bool) (a b : ℕ) :
    fourCoefficient derivative a a b b = mass derivative a * mass derivative b := by
…
```
Mentions: OAI.Problem335.LocalMoments.fourCoefficient, OAI.Problem335.LocalMoments.mass
lemma OAI.Problem335.LocalMoments.derivative_diagonal_fourCoefficient line 41
Source documentation
Differentiating diagonal pairing: the second path receives one occupation.
```
lemma derivative_diagonal_fourCoefficient (a b : ℕ) :
    fourCoefficient true a (b + 1) a (b + 1) = (a : ℝ) * ((b : ℝ) + 1) := by
…
```
Mentions: OAI.Problem335.LocalMoments.fourCoefficient
lemma OAI.Problem335.LocalMoments.multiplication_diagonal_fourCoefficient line 50
Source documentation
Multiplying diagonal pairing, expressed without natural subtraction.
```
lemma multiplication_diagonal_fourCoefficient (a b : ℕ) :
    fourCoefficient false a b a b = ((a : ℝ) + 1) * ((b : ℝ) + 1) := by
…
```
Mentions: OAI.Problem335.LocalMoments.fourCoefficient
lemma OAI.Problem335.LocalMoments.multiplication_diagonal_fourCoefficient_pred line 58
lemma OAI.Problem335.LocalMoments.derivative_invalid line 67
Source documentation
The unavailable differentiation contribution vanishes identically.
```
@[simp] lemma derivative_invalid (b : ℕ) :
    (0 : ℝ) * ((b : ℝ) + 1) = 0 := zero_mul _
```
lemma OAI.Problem335.LocalMoments.multiplication_invalid line 72
Source documentation
If the multiplication shift would create a negative source occupation, its table contribution is zero.
```
@[simp] lemma multiplication_invalid (a : ℕ) :
    ((a : ℝ) + 1) * (0 : ℝ) = 0 := mul_zero _
```

lemma OAI.Problem335.LocalMoments.four_products_eq_product line 76

Source documentation

Move the four path products into a product of local four-factor entries.

lemma four_products_eq_product {ι : Type*} (s : Finset ι)
    (derivative : ι → Bool) (a b c d : ι → ℕ) :
    (∏ i ∈ s, coefficient (derivative i) (a i)) *
      (∏ i ∈ s, coefficient (derivative i) (b i)) *
      (∏ i ∈ s, coefficient (derivative i) (c i)) *
      (∏ i ∈ s, coefficient (derivative i) (d i)) =
    ∏ i ∈ s, fourCoefficient (derivative i) (a i) (b i) (c i) (d i) := by
…

Mentions: OAI.Problem335.LocalMoments.coefficient, OAI.Problem335.LocalMoments.fourCoefficient

lemma OAI.Problem335.LocalMoments.normal_layer line 86

Source documentation

Version of the normal pairing usable with occupation functions.

lemma normal_layer {σ : Type*} (derivative : Bool) (M M' : σ → ℕ) (i j : σ)
    (hi : M' i = M i) (hj : M' j = M j) :
    fourCoefficient derivative (M i) (M' i) (M j) (M' j) =
      mass derivative (M i) * mass derivative (M j) := by
…

Mentions: OAI.Problem335.LocalMoments.fourCoefficient, OAI.Problem335.LocalMoments.mass

lemma OAI.Problem335.LocalMoments.derivative_diagonal_layer line 92
lemma OAI.Problem335.LocalMoments.multiplication_diagonal_layer line 98
def OAI.Problem335.LocalMoments.multiplicationDiagonalTerm line 108
Source documentation
The multiplying diagonal term, extended by zero when its backward shift is invalid.
```
def multiplicationDiagonalTerm (a b : ℕ) : ℝ :=
…
```
lemma OAI.Problem335.LocalMoments.multiplicationDiagonalTerm_eq line 111
lemma OAI.Problem335.LocalMoments.square_fallingFactorial line 118
lemma OAI.Problem335.LocalMoments.successor_square_fallingFactorial line 124
def OAI.Problem335.LocalMoments.normalGeometricMass line 131
Source documentation
Geometric first/second-moment input, before normalization, for normal pairings.
```
def normalGeometricMass (derivative : Bool) (G : ℝ) (collision : Bool) : ℝ :=
…
```
def OAI.Problem335.LocalMoments.diagonalGeometricMass line 137
lemma OAI.Problem335.LocalMoments.derivative_normal_weight line 139
lemma OAI.Problem335.LocalMoments.multiplication_normal_weight line 148
lemma OAI.Problem335.LocalMoments.derivative_diagonal_weight line 156
lemma OAI.Problem335.LocalMoments.multiplication_diagonal_weight line 163