IndependentCoordinates.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.IndependentCoordinates.average line 12
Source documentation
The uniform average on a finite type, with value zero on an empty type.
```
def average {α : Type*} [Fintype α] (f : α → ℝ) : ℝ :=
…
```
theorem OAI.Problem335.IndependentCoordinates.average_equiv line 17
Source documentation
Uniform finite averages are unchanged by relabeling.
```
theorem average_equiv {α β : Type*} [Fintype α] [Fintype β]
    (e : α ≃ β) (f : β → ℝ) : average (fun x => f (e x)) = average f := by
…
```
Mentions: OAI.Problem335.IndependentCoordinates.average

theorem OAI.Problem335.IndependentCoordinates.average_prod line 22

Source documentation

Independent coordinates factor the average of a product.

theorem average_prod {ι : Type*} [Fintype ι] [DecidableEq ι] {α : ι → Type*}
    [∀ i, Fintype (α i)] (f : ∀ i, α i → ℝ) :
    average (fun x : ∀ i, α i => ∏ i, f i (x i)) = ∏ i, average (f i) := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average

def OAI.Problem335.IndependentCoordinates.fiberAssignmentEquiv line 31
Source documentation
Reorganize coordinates into the fibers of a grouping function.
```
def fiberAssignmentEquiv {σ ι α : Type*} (group : σ → ι) :
    (σ → α) ≃ (∀ i, {s // group s = i} → α) :=
…
```
theorem OAI.Problem335.IndependentCoordinates.fiberAssignmentEquiv_apply line 36

theorem OAI.Problem335.IndependentCoordinates.average_grouped_prod line 42

Source documentation

Factors on disjoint groups of coordinates have independent uniform averages. An unused group can be included with its factor set equal to one.

theorem average_grouped_prod {σ ι α : Type*}
    [Fintype σ] [Fintype ι] [Fintype α] [DecidableEq σ] [DecidableEq ι]
    (group : σ → ι) (f : ∀ i, ({s // group s = i} → α) → ℝ) :
    average (fun x : σ → α => ∏ i, f i (fun s => x s)) =
      ∏ i, average (f i) := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average

theorem OAI.Problem335.IndependentCoordinates.average_pair_eq line 53
Source documentation
One independent pair of uniform labels agrees with probability 1 / card α.
```
theorem average_pair_eq {α : Type*} [Fintype α] [DecidableEq α] :
    average (fun x : α × α => if x.1 = x.2 then (1 : ℝ) else 0) =
      (Fintype.card α : ℝ)⁻¹ := by
…
```
Mentions: OAI.Problem335.IndependentCoordinates.average
theorem OAI.Problem335.IndependentCoordinates.average_add line 63
theorem OAI.Problem335.IndependentCoordinates.average_const line 67
theorem OAI.Problem335.IndependentCoordinates.average_const_mul line 71
def OAI.Problem335.IndependentCoordinates.pairEq line 76
Source documentation
The indicator that two labels agree.
```
def pairEq {α : Type*} [DecidableEq α] (x : α × α) : ℝ :=
…
```
def OAI.Problem335.IndependentCoordinates.allPairsEq line 80
Source documentation
Simultaneous agreement of card κ independent label pairs.
```
def allPairsEq {κ α : Type*} [Fintype κ] [DecidableEq α]
    (x : κ → α × α) : ℝ := ∏ i, pairEq (x i)
```
Mentions: OAI.Problem335.IndependentCoordinates.pairEq
theorem OAI.Problem335.IndependentCoordinates.average_allPairsEq line 83
theorem OAI.Problem335.IndependentCoordinates.average_equality_correction line 92

theorem OAI.Problem335.IndependentCoordinates.average_grouped_equality_corrections line 100

Source documentation

The precise independence identity used for nonadjacent derivative layers. The fibers of group are the disjoint sets of free endpoints of those layers.

theorem average_grouped_equality_corrections {σ ι α : Type*}
    [Fintype σ] [Fintype ι] [Fintype α]
    [DecidableEq σ] [DecidableEq ι] [DecidableEq α] [Nonempty α]
    (group : σ → ι) (c : ι → ℝ) :
    average (fun x : σ → α × α =>
      ∏ i, (1 + c i * allPairsEq (fun s : {s // group s = i} => x s))) =
    ∏ i, (1 + c i * (Fintype.card α : ℝ)⁻¹ ^ Fintype.card {s // group s = i}) := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average, OAI.Problem335.IndependentCoordinates.allPairsEq

theorem OAI.Problem335.IndependentCoordinates.average_selected_grouped_prod line 114

Source documentation

Coordinates assigned to none are unused and integrate out.

theorem average_selected_grouped_prod {σ ι α : Type*}
    [Fintype σ] [Fintype ι] [Fintype α] [Nonempty α]
    [DecidableEq σ] [DecidableEq ι]
    (group : σ → Option ι)
    (f : ∀ i, ({s // group s = some i} → α) → ℝ) :
    average (fun x : σ → α => ∏ i, f i (fun s => x s)) =
      ∏ i, average (f i) := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average

theorem OAI.Problem335.IndependentCoordinates.average_selected_equality_corrections line 130

Source documentation

Equality corrections for selected disjoint endpoint groups. Other vertices may be assigned to none, and their choices do not affect the expectation.

theorem average_selected_equality_corrections {σ ι α : Type*}
    [Fintype σ] [Fintype ι] [Fintype α]
    [DecidableEq σ] [DecidableEq ι] [DecidableEq α] [Nonempty α]
    (group : σ → Option ι) (c : ι → ℝ) :
    average (fun x : σ → α × α =>
      ∏ i, (1 + c i * allPairsEq (fun s : {s // group s = some i} => x s))) =
    ∏ i, (1 + c i * (Fintype.card α : ℝ)⁻¹ ^
      Fintype.card {s // group s = some i}) := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average, OAI.Problem335.IndependentCoordinates.allPairsEq

theorem OAI.Problem335.IndependentCoordinates.average_ignore_right line 145
Source documentation
Extra independent coordinates that do not appear in the integrand cancel.
```
theorem average_ignore_right {α β : Type*} [Fintype α] [Fintype β]
    [Nonempty β] (f : α → ℝ) :
    average (fun x : α × β => f x.1) = average f := by
…
```
Mentions: OAI.Problem335.IndependentCoordinates.average
def OAI.Problem335.IndependentCoordinates.restrictAssignmentEquiv line 158
Source documentation
Split all assignments into their values on an embedded coordinate set and on its complement.
```
def restrictAssignmentEquiv {σ τ α : Type*} (j : τ → σ)
    (hj : Function.Injective j) :
    (σ → α) ≃ (τ → α) × ({s // s ∉ Set.range j} → α) := by
…
```
theorem OAI.Problem335.IndependentCoordinates.restrictAssignmentEquiv_fst line 168

theorem OAI.Problem335.IndependentCoordinates.average_precomp_injective line 173

Source documentation

Uniform assignments restrict uniformly to any subset of coordinates.

theorem average_precomp_injective {σ τ α : Type*}
    [Fintype σ] [Fintype τ] [Fintype α] [Nonempty α]
    [DecidableEq σ] [DecidableEq τ]
    (j : τ → σ) (hj : Function.Injective j) (f : (τ → α) → ℝ) :
    average (fun x : σ → α => f (fun t => x (j t))) = average f := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average

theorem OAI.Problem335.IndependentCoordinates.average_sigma_prod line 185

Source documentation

A sigma-indexed family of labels is the product of its fiber families.

theorem average_sigma_prod {ι α : Type*} {κ : ι → Type*}
    [Fintype ι] [Fintype α] [∀ i, Fintype (κ i)]
    [DecidableEq ι] [∀ i, DecidableEq (κ i)]
    (f : ∀ i, (κ i → α) → ℝ) :
    average (fun x : (Σ i, κ i) → α => ∏ i, f i (fun t => x ⟨i, t⟩)) =
      ∏ i, average (f i) := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average

theorem OAI.Problem335.IndependentCoordinates.average_embedded_prod line 198

Source documentation

Finite factors on an injectively embedded disjoint family of coordinates factor under uniform averaging.

theorem average_embedded_prod {σ ι α : Type*} {κ : ι → Type*}
    [Fintype σ] [Fintype ι] [Fintype α] [∀ i, Fintype (κ i)] [Nonempty α]
    [DecidableEq σ] [DecidableEq ι] [∀ i, DecidableEq (κ i)]
    (j : ∀ i, κ i → σ) (hj : Function.Injective (Sigma.uncurry j))
    (f : ∀ i, (κ i → α) → ℝ) :
    average (fun x : σ → α => ∏ i, f i (fun t => x (j i t))) =
      ∏ i, average (f i) := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average

theorem OAI.Problem335.IndependentCoordinates.sigma_val_injective line 210

Source documentation

Pairwise disjoint subsets give an injective family of coordinate inclusions.

theorem sigma_val_injective {σ ι : Type*} (s : ι → Finset σ)
    (hs : Pairwise (fun i j => Disjoint (s i) (s j))) :
    Function.Injective (fun x : Σ i, s i => (x.2 : σ)) := by
…

theorem OAI.Problem335.IndependentCoordinates.average_disjoint_finset_prod line 224

Source documentation

Factors depending on pairwise disjoint finite coordinate sets are independent.

theorem average_disjoint_finset_prod {σ ι α : Type*}
    [Fintype σ] [Fintype ι] [Fintype α] [Nonempty α]
    [DecidableEq σ] [DecidableEq ι]
    (s : ι → Finset σ) (hs : Pairwise (fun i j => Disjoint (s i) (s j)))
    (f : ∀ i, (s i → α) → ℝ) :
    average (fun x : σ → α => ∏ i, f i (fun t => x t)) =
      ∏ i, average (f i) := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average

theorem OAI.Problem335.IndependentCoordinates.average_disjoint_equality_corrections line 235

Source documentation

The endpoint-coincidence average for pairwise disjoint free-endpoint sets.

theorem average_disjoint_equality_corrections {σ ι α : Type*}
    [Fintype σ] [Fintype ι] [Fintype α]
    [DecidableEq σ] [DecidableEq ι] [DecidableEq α] [Nonempty α]
    (s : ι → Finset σ) (hs : Pairwise (fun i j => Disjoint (s i) (s j)))
    (c : ι → ℝ) :
    average (fun x : σ → α × α =>
      ∏ i, (1 + c i * allPairsEq (fun t : s i => x t))) =
    ∏ i, (1 + c i * (Fintype.card α : ℝ)⁻¹ ^ (s i).card) := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average, OAI.Problem335.IndependentCoordinates.allPairsEq

def OAI.Problem335.IndependentCoordinates.restrictDependentAssignmentEquiv line 251

Source documentation

Dependent-coordinate version of restriction to an embedded coordinate set.

def restrictDependentAssignmentEquiv {σ τ : Type*} (β : σ → Type*)
    (j : τ → σ) (hj : Function.Injective j) :
    (∀ s, β s) ≃ (∀ t, β (j t)) × (∀ s : {s // s ∉ Set.range j}, β s) := by
…

theorem OAI.Problem335.IndependentCoordinates.restrictDependentAssignmentEquiv_fst line 261

theorem OAI.Problem335.IndependentCoordinates.average_precomp_injective_dependent line 268

Source documentation

Marginals of a uniform finite product are uniform, allowing different coordinate types at different vertices.

theorem average_precomp_injective_dependent {σ τ : Type*} {β : σ → Type*}
    [Fintype σ] [Fintype τ] [∀ s, Fintype (β s)] [∀ s, Nonempty (β s)]
    [DecidableEq σ] [DecidableEq τ]
    (j : τ → σ) (hj : Function.Injective j) (f : (∀ t, β (j t)) → ℝ) :
    average (fun x : ∀ s, β s => f (fun t => x (j t))) = average f := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average

theorem OAI.Problem335.IndependentCoordinates.average_sigma_prod_dependent line 280
theorem OAI.Problem335.IndependentCoordinates.average_embedded_prod_dependent line 292

theorem OAI.Problem335.IndependentCoordinates.average_disjoint_finset_prod_dependent line 307

Source documentation

Disjoint coordinate families remain independent when vertex alphabets vary.

theorem average_disjoint_finset_prod_dependent {σ ι : Type*} {β : σ → Type*}
    [Fintype σ] [Fintype ι] [∀ s, Fintype (β s)] [∀ s, Nonempty (β s)]
    [DecidableEq σ] [DecidableEq ι]
    (s : ι → Finset σ) (hs : Pairwise (fun i j => Disjoint (s i) (s j)))
    (f : ∀ i, (∀ t : s i, β t) → ℝ) :
    average (fun x : ∀ s, β s => ∏ i, f i (fun t => x t)) =
      ∏ i, average (f i) := by
…

Mentions: OAI.Problem335.IndependentCoordinates.average