TreeSplitCoordinates.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Independent split coordinates on each actual leaf-product fiber

def OAI.Ostmann.splitSamplesAppendEquiv line 13
def OAI.Ostmann.treeLeafSplitEquiv line 30
Source documentation
Preorder split products are coordinates: root split first, followed by the left subtree and the right subtree. Each coordinate is an independent Haar unit even after the total leaf product is fixed.
```
noncomputable def treeLeafSplitEquiv {G : Type} [CommGroup G] : (n : ℕ) → (P : G) →
    TreeLeafFiber G n P ≃ SplitSamples G (2 ^ n - 1)
  | 0, P => treeLeafFiberZeroEquiv P
  | n + 1, P => by
      let k := 2 ^ n - 1
…
```
Mentions: OAI.Ostmann.TreeLeafFiber, OAI.Ostmann.SplitSamples, OAI.Ostmann.treeLeafFiberZeroEquiv

theorem OAI.Ostmann.treeLeafSplit_average line 49

Source documentation

Exact transport of the original conditional Haar average.

theorem treeLeafSplit_average {G : Type} [CommGroup G] [Fintype G]
    (n : ℕ) (P : G) (F : SplitSamples G (2 ^ n - 1) → ℝ) :
    (Fintype.card (TreeLeafFiber G n P) : ℝ)⁻¹ *
        (∑ x : TreeLeafFiber G n P, F (treeLeafSplitEquiv n P x)) =
      (Fintype.card G : ℝ)⁻¹ ^ (2 ^ n - 1) * ∑ y, F y := by
…

Mentions: OAI.Ostmann.SplitSamples, OAI.Ostmann.TreeLeafFiber, OAI.Ostmann.treeLeafSplitEquiv

theorem OAI.Ostmann.treeLeaf_sequentialSupport_le line 58

Source documentation

Adaptive support bounds therefore apply to the actual uniformly sampled leaves with their product fixed, before any validity restriction.

theorem treeLeaf_sequentialSupport_le {G : Type} [CommGroup G] [Fintype G]
    (test : List G → G → Prop) (ρ : ℝ) (hρ : 0 ≤ ρ)
    (htest : ∀ past, (Fintype.card G : ℝ)⁻¹ *
      (∑ x : G, if test past x then (1 : ℝ) else 0) ≤ ρ)
    (past : List G) (n : ℕ) (P : G) :
    (Fintype.card (TreeLeafFiber G n P) : ℝ)⁻¹ *
        (∑ x : TreeLeafFiber G n P,
          sequentialSupport test past (2 ^ n - 1) (treeLeafSplitEquiv n P x)) ≤
      ρ ^ (2 ^ n - 1) := by
…

Mentions: OAI.Ostmann.TreeLeafFiber, OAI.Ostmann.sequentialSupport, OAI.Ostmann.treeLeafSplitEquiv