FiniteDisplacement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-group displacement for arbitrary maps to ℓ₁

The finite-group displacement identity lem:finite-fourier holds for maps from any finite abelian group into TreeEdit.RealL1, the full space of absolutely summable real sequences. No injectivity or finite-support assumption is needed.

The proof combines finite scalar cuts, summable-coordinate aggregation, Parseval's identity and finite nonnegative summation.

theorem OAI.TreeEdit.BinaryLower.l1_bool_cut_representation line 29
Source documentation
Concrete finite-cut representation of any finite family of absolutely summable real sequences. The two constant cuts have zero weight. The final bound is the half ordered-pair form of the finite total-mass estimate.
```
theorem l1_bool_cut_representation {S : Type*} [Fintype S] [DecidableEq S]
    (F : S → RealL1) :
    ∃ a : (S → Bool) → ℝ, (∀ C, 0 ≤ a C) ∧
      (∀ x y, ‖F x - F y‖ = ∑ C, a C * BoolCuts.cutDistance C x y) ∧
      a (fun _ => false) = 0 ∧ a (fun _ => true) = 0 ∧
      (∑ C, a C) ≤ (∑ p : S × S, ‖F p.1 - F p.2‖) / 2 := by
…
```
Mentions: OAI.TreeEdit.RealL1, OAI.TreeEdit.BinaryLower.BoolCuts.cutDistance

theorem OAI.TreeEdit.BinaryLower.finite_group_displacement line 76

Source documentation

The finite-group displacement lemma, for the actual full ℓ₁ sequence space. Uniform probability averaging is denoted by 𝔼.

theorem finite_group_displacement {A : Type*} [AddCommGroup A] [Fintype A]
    (F : A → RealL1) :
    ∃ H : AddChar A ℂ → ℝ, (∀ χ, 0 ≤ H χ) ∧
      ∀ z, (𝔼 x, ‖F (x + z) - F x‖) =
        ∑ χ : AddChar A ℂ, ‖1 - χ z‖ ^ 2 * H χ := by
…

Mentions: OAI.TreeEdit.RealL1