ProductReindex.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Reindexing real-valued expectations and Dirichlet energies on finite Boolean products.

theorem OAI.Problem313.Reindex.sum_weight_config line 16

Source documentation

A coordinate equivalence preserves each weighted real-valued expectation.

theorem sum_weight_config (e : ι ≃ κ) (p : ℝ)
    (f : (ι → Bool) → ℝ) (g : (κ → Bool) → ℝ)
    (hfg : ∀ x, g (config e x) = f x) :
    (∑ y, weight p y * g y) = ∑ x, weight p x * f x := by
…

Mentions: OAI.Problem313.Reindex.config, OAI.Problem313.Reindex.weight

theorem OAI.Problem313.Reindex.coordinate_energy_config line 27

Source documentation

The squared energy at a single coordinate is preserved by reindexing.

theorem coordinate_energy_config
    (e : ι ≃ κ) (p : ℝ) (f : (ι → Bool) → ℝ) (g : (κ → Bool) → ℝ)
    (hfg : ∀ x, g (config e x) = f x) (i : ι) :
    (∑ y, weight p y *
      (g (Function.update y (e i) true) - g (Function.update y (e i) false)) ^ 2) =
      ∑ x, weight p x *
        (f (Function.update x i true) - f (Function.update x i false)) ^ 2 := by
…

Mentions: OAI.Problem313.Reindex.config, OAI.Problem313.Reindex.weight

theorem OAI.Problem313.Reindex.energy_config line 39

Source documentation

The full Dirichlet energy is invariant under a finite coordinate equivalence.

theorem energy_config
    (e : ι ≃ κ) (p : ℝ) (f : (ι → Bool) → ℝ) (g : (κ → Bool) → ℝ)
    (hfg : ∀ x, g (config e x) = f x) :
    (∑ j, ∑ y, weight p y *
      (g (Function.update y j true) - g (Function.update y j false)) ^ 2) =
      ∑ i, ∑ x, weight p x *
        (f (Function.update x i true) - f (Function.update x i false)) ^ 2 := by
…

Mentions: OAI.Problem313.Reindex.config, OAI.Problem313.Reindex.weight

theorem OAI.Problem313.Reindex.centered_sum_config line 52

Source documentation

Centered second moments are invariant, for any specified center.

theorem centered_sum_config (e : ι ≃ κ) (p c : ℝ)
    (f : (ι → Bool) → ℝ) (g : (κ → Bool) → ℝ)
    (hfg : ∀ x, g (config e x) = f x) :
    (∑ y, weight p y * (g y - c) ^ 2) =
      ∑ x, weight p x * (f x - c) ^ 2 := by
…

Mentions: OAI.Problem313.Reindex.config, OAI.Problem313.Reindex.weight