FactorialGeometricValue.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Finite geometric-moment evaluation of nonnegative factorial expansions.

def OAI.Problem335.geometricFactorialMonomial line 13
Source documentation
Independent geometric factorial moments, with a possibly different mean per coordinate.
```
def geometricFactorialMonomial (d : σ → ℕ) (G : σ → ℝ) : ℝ :=
…
```
def OAI.Problem335.FactorialExpansion.geometricValue line 19
Source documentation
The finite value to which occupation comparison bounds an expansion.
```
def geometricValue {f : (σ → ℕ) → ℕ} {S : Finset σ} {D : ℕ}
    (F : FactorialExpansion f S D) (G : σ → ℝ) : ℝ :=
…
```
Mentions: OAI.Problem335.FactorialExpansion
theorem OAI.Problem335.FactorialExpansion.geometricValue_weaken line 23
theorem OAI.Problem335.FactorialExpansion.geometricValue_reframe line 27
theorem OAI.Problem335.FactorialExpansion.geometricFactorialMonomial_single line 35
theorem OAI.Problem335.FactorialExpansion.geometricValue_add line 47
theorem OAI.Problem335.FactorialExpansion.geometricValue_mul line 57
Source documentation
Independence at disjoint coordinates is an exact algebraic identity of the finite factorial-moment values; no probability-space construction is needed.
```
@[simp] theorem geometricValue_mul {f g : (σ → ℕ) → ℕ} {S T : Finset σ} {D E : ℕ}
    (F : FactorialExpansion f S D) (H : FactorialExpansion g T E)
    (hST : Disjoint S T) (G : σ → ℝ) :
    (F.mul H hST).geometricValue G = F.geometricValue G * H.geometricValue G := by
…
```
Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.FactorialExpansion.geometricValue
theorem OAI.Problem335.FactorialExpansion.geometricValue_coordinate line 81
theorem OAI.Problem335.FactorialExpansion.geometricValue_occupation line 90
theorem OAI.Problem335.FactorialExpansion.geometricValue_successor line 93
theorem OAI.Problem335.FactorialExpansion.geometricValue_square line 97
theorem OAI.Problem335.FactorialExpansion.geometricValue_successorSquare line 101
theorem OAI.Problem335.FactorialExpansion.geometricValue_normalDerivative line 105
theorem OAI.Problem335.FactorialExpansion.geometricValue_normalMultiplication line 116
theorem OAI.Problem335.FactorialExpansion.geometricValue_distinctDerivative line 127
theorem OAI.Problem335.FactorialExpansion.geometricValue_distinctMultiplication line 133
theorem OAI.Problem335.FactorialExpansion.geometricValue_constant line 140

theorem OAI.Problem335.FactorialExpansion.geometricValue_congr_on line 146

Source documentation

The value depends only on the coordinates allowed by the expansion support.

theorem geometricValue_congr_on {f : (σ → ℕ) → ℕ} {S : Finset σ} {D : ℕ}
    (F : FactorialExpansion f S D) (G H : σ → ℝ)
    (heq : ∀ i ∈ S, G i = H i) : F.geometricValue G = F.geometricValue H := by
…

Mentions: OAI.Problem335.FactorialExpansion

theorem OAI.Problem335.FactorialExpansion.exists_prod_geometricValue line 162

Source documentation

Choose the finite product expansion together with its exact independent geometric factorial value.

theorem exists_prod_geometricValue {ι : Type*} (s : Finset ι)
    (f : ι → (σ → ℕ) → ℕ) (S : ι → Finset σ) (D : ι → ℕ)
    (F : ∀ i, FactorialExpansion (f i) (S i) (D i)) (G : σ → ℝ)
    (hdis : (s : Set ι).Pairwise fun i j => Disjoint (S i) (S j)) :
    ∃ H : FactorialExpansion (fun M => ∏ i ∈ s, f i M)
      (s.biUnion S) (∑ i ∈ s, D i),
      H.geometricValue G = ∏ i ∈ s, (F i).geometricValue G := by
…

Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.FactorialExpansion.geometricValue

def OAI.Problem335.LocalMoments.localGeometricMass line 201
Source documentation
Exact independent geometric expectation of the local table at a common mean.
```
def localGeometricMass (derivative : Bool) (G : ℝ) (p q r : σ) : ℝ :=
…
```
theorem OAI.Problem335.LocalMoments.geometricValue_localPolynomialExpansion line 205

theorem OAI.Problem335.LocalMoments.geometricValue_localPolynomialExpansion_of_eq line 221

Source documentation

Local evaluation when only the three relevant coordinate means agree.

theorem geometricValue_localPolynomialExpansion_of_eq (derivative : Bool)
    (p q r : σ) (G : σ → ℝ) (g : ℝ)
    (hp : G p = g) (hq : G q = g) (hr : G r = g) :
    (localPolynomialExpansion derivative p q r).geometricValue G =
      localGeometricMass derivative g p q r := by
…

Mentions: OAI.Problem335.LocalMoments.localPolynomialExpansion, OAI.Problem335.LocalMoments.localGeometricMass

theorem OAI.Problem335.LocalMoments.exists_localProduct_geometricValue line 239

Source documentation

The actual local-table product has an expansion whose geometric value is exactly the product of its local expected masses. This is the finite algebraic bridge from occupation comparison to the normalized pairing weights.

theorem exists_localProduct_geometricValue {ι : Type*} (layers : Finset ι)
    (derivative : ι → Bool) (p q r : ι → σ) (G : ℝ)
    (hdis : (layers : Set ι).Pairwise fun i j =>
      Disjoint ({p i, q i, r i} : Finset σ) {p j, q j, r j}) :
    ∃ F : FactorialExpansion (localProductNat layers derivative p q r)
      (layers.biUnion fun i => {p i, q i, r i}) (2 * layers.card),
      F.geometricValue (fun _ => G) =
        ∏ t ∈ layers, localGeometricMass (derivative t) G (p t) (q t) (r t) := by
…

Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.LocalMoments.localProductNat, OAI.Problem335.LocalMoments.localGeometricMass

theorem OAI.Problem335.LocalMoments.exists_localProduct_geometricValue_of_eq line 262

Source documentation

Different layers may have different geometric means. In particular this handles mean A on derivative layers and mean B on multiplication layers.

theorem exists_localProduct_geometricValue_of_eq {ι : Type*} (layers : Finset ι)
    (derivative : ι → Bool) (p q r : ι → σ) (G : σ → ℝ) (g : ι → ℝ)
    (hp : ∀ t ∈ layers, G (p t) = g t)
    (hq : ∀ t ∈ layers, G (q t) = g t)
    (hr : ∀ t ∈ layers, G (r t) = g t)
    (hdis : (layers : Set ι).Pairwise fun i j =>
      Disjoint ({p i, q i, r i} : Finset σ) {p j, q j, r j}) :
    ∃ F : FactorialExpansion (localProductNat layers derivative p q r)
      (layers.biUnion fun i => {p i, q i, r i}) (2 * layers.card),
      F.geometricValue G =
        ∏ t ∈ layers, localGeometricMass (derivative t) (g t) (p t) (q t) (r t) := by
…

Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.LocalMoments.localProductNat, OAI.Problem335.LocalMoments.localGeometricMass

theorem OAI.Problem335.LocalMoments.exists_layered_localProduct_geometricValue line 290

Source documentation

Layer-labelled coordinates automatically satisfy the local equal-mean and disjoint-support requirements.

theorem exists_layered_localProduct_geometricValue {ι κ : Type*}
    [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
    (layers : Finset ι) (derivative : ι → Bool) (p q r : ι → κ) (g : ι → ℝ) :
    ∃ F : FactorialExpansion
      (localProductNat layers derivative (fun i => (i, p i))
        (fun i => (i, q i)) (fun i => (i, r i)))
      (layers.biUnion fun i => {(i, p i), (i, q i), (i, r i)}) (2 * layers.card),
      F.geometricValue (fun x => g x.1) =
        ∏ t ∈ layers, localGeometricMass (derivative t) (g t)
          (t, p t) (t, q t) (t, r t) := by
…

Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.LocalMoments.localProductNat, OAI.Problem335.LocalMoments.localGeometricMass