SparseActivity.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Sparse activity in a finite branching construction

Sparse/dense Fourier-mass estimates for prop:finite-lower.

def OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.activeLeaves line 18

Source documentation

The number of active leaves in the full m-ary tree of height h. A node is represented by its list of child indices, starting at the root.

noncomputable def activeLeaves {m : ℕ} (A : List (Fin m) → Prop) : ℕ → ℕ
  | 0 => if A [] then 1 else 0
  | h + 1 => ∑ i : Fin m, activeLeaves (fun p => A (i :: p)) h

/-- There is no active internal node with fewer than `b` active children. -/

def OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.NoSparse line 23

Source documentation

There is no active internal node with fewer than b active children.

def NoSparse {m : ℕ} (b : ℕ) (A : List (Fin m) → Prop) : ℕ → Prop
  | 0 => True
  | h + 1 =>
      (A [] → b ≤ (Finset.univ.filter (fun i : Fin m => A [i])).card) ∧
      ∀ i : Fin m, NoSparse b (fun p => A (i :: p)) h

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.activeLeaves_lower line 29

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.weighted_active_bound line 56

Source documentation

A weighted version of the sparse/dense activity dichotomy. The exceptional set may overlap the inactive set. No disjointness assumptions on the tests used to bound exceptional mass are required.

theorem weighted_active_bound {ι : Type*} [Fintype ι]
    (H w μ : ι → ℝ) (active exceptional : ι → Prop)
    (M ε K : ℝ) (hK : 0 < K)
    (hH : ∀ i, 0 ≤ H i) (hw : ∀ i, 0 ≤ w i)
    (hμ : ∀ i, μ i ≤ 4)
    (hzero : ∀ i, ¬ active i → μ i = 0)
    (hdense : ∀ i, active i → ¬ exceptional i → K ≤ w i)
    (hleaf : 2 * ∑ i, w i * H i ≤ M)
    (hexceptional : (∑ i, if exceptional i then H i else 0) ≤ ε) :
    (∑ i, μ i * H i) ≤ 4 * (ε + M / (2 * K)) := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.weighted_detection_bound line 97

Source documentation

A nonnegative detector that accumulates at least one unit on every bad frequency bounds the total Fourier weight of those frequencies.

theorem weighted_detection_bound {ι σ : Type*} [Fintype ι] [Fintype σ]
    (H : ι → ℝ) (a : σ → ι → ℝ) (bad : ι → Prop)
    (hH : ∀ i, 0 ≤ H i) (ha : ∀ s i, 0 ≤ a s i)
    (hdetect : ∀ i, bad i → 1 ≤ ∑ s, a s i) :
    (∑ i, if bad i then H i else 0) ≤ ∑ s, ∑ i, a s i * H i := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.weighted_union_bound line 118

Source documentation

Union bound for nonnegative Fourier mass. Overlap between bad-node tests can only increase the sum on the right.

theorem weighted_union_bound {ι ν : Type*} [Fintype ι] [Fintype ν]
    (H : ι → ℝ) (bad : ν → ι → Prop) (hH : ∀ i, 0 ≤ H i) :
    (∑ i, if ∃ v, bad v i then H i else 0) ≤
      ∑ v, ∑ i, if bad v i then H i else 0 := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.exceptional_mass_of_detectors line 143

Source documentation

Combining detectors at all nodes gives the exceptional-character mass estimate used before the sparse/dense dichotomy.

theorem exceptional_mass_of_detectors {ι ν σ : Type*}
    [Fintype ι] [Fintype ν] [Fintype σ]
    (H : ι → ℝ) (a : ν → σ → ι → ℝ) (bad : ν → ι → Prop)
    (B : ν → ℝ) (hH : ∀ i, 0 ≤ H i)
    (ha : ∀ v s i, 0 ≤ a v s i)
    (hdetect : ∀ v i, bad v i → 1 ≤ ∑ s, a v s i)
    (hcost : ∀ v, (∑ s, ∑ i, a v s i * H i) ≤ B v) :
    (∑ i, if ∃ v, bad v i then H i else 0) ≤ ∑ v, B v := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.sum_level_budget line 160
Source documentation
At each depth there are m^j nodes, each with reciprocal-size budget. Thus the total over k internal levels is exactly k times the level budget.
```
theorem sum_level_budget (m k : ℕ) (hm : m ≠ 0) (C : ℝ) :
    (∑ j : Fin k, ∑ _v : Fin (m ^ (j : ℕ)), C / (m : ℝ) ^ (j : ℕ)) = k * C := by
…
```

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.root_bound_of_detectors line 173

Source documentation

The finite obstruction's root estimate in terms of nonnegative Fourier weights and geometric detector bounds.

theorem root_bound_of_detectors {ι ν σ : Type*}
    [Fintype ι] [Fintype ν] [Fintype σ]
    (H w μ : ι → ℝ) (active : ι → Prop) (bad : ν → ι → Prop)
    (a : ν → σ → ι → ℝ) (B : ν → ℝ) (M ε K : ℝ)
    (hK : 0 < K) (hH : ∀ i, 0 ≤ H i) (hw : ∀ i, 0 ≤ w i)
    (hμ : ∀ i, μ i ≤ 4) (hzero : ∀ i, ¬ active i → μ i = 0)
    (hdense : ∀ i, active i → (¬ ∃ v, bad v i) → K ≤ w i)
    (hleaf : 2 * ∑ i, w i * H i ≤ M)
    (ha : ∀ v s i, 0 ≤ a v s i)
    (hdetect : ∀ v i, bad v i → 1 ≤ ∑ s, a v s i)
    (hcost : ∀ v, (∑ s, ∑ i, a v s i * H i) ≤ B v)
    (hbudget : (∑ v, B v) ≤ ε) :
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.support_mass_identity line 197

Source documentation

Counting active coordinates commutes with summing nonnegative Fourier weights. The identity itself does not require weight nonnegativity.

theorem support_mass_identity {ι κ : Type*} [Fintype ι] [Fintype κ]
    (H : ι → ℝ) (activeLeaf : κ → ι → Prop) :
    (∑ i, ((Finset.univ.filter (fun u => activeLeaf u i)).card : ℝ) * H i) =
      ∑ u, ∑ i, if activeLeaf u i then H i else 0 := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.leaf_mass_bound line 213

Source documentation

The per-leaf cyclic-average cost estimates imply the weighted leaf-mass bound. This is equation (finite-leaf-mass) before insertion of the tree costs.

theorem leaf_mass_bound {ι κ : Type*} [Fintype ι] [Fintype κ]
    (H : ι → ℝ) (activeLeaf : κ → ι → Prop) (C : κ → ℝ) (M : ℝ)
    (hleaf : ∀ u, 2 * (∑ i, if activeLeaf u i then H i else 0) ≤ C u)
    (hbudget : (∑ u, C u) ≤ M) :
    2 * (∑ i, ((Finset.univ.filter (fun u => activeLeaf u i)).card : ℝ) * H i) ≤ M := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.weighted_average_detection_bound line 225

Source documentation

Unnormalized version of the detector bound, directly usable with a short interval of J translates. The index type need not itself have size J; the explicit lower average and total cost are the necessary hypotheses.

theorem weighted_average_detection_bound {ι σ : Type*} [Fintype ι] [Fintype σ]
    (H : ι → ℝ) (a : σ → ι → ℝ) (bad : ι → Prop) (V : σ → ℝ)
    (J : ℝ) (hJ : 0 < J) (hH : ∀ i, 0 ≤ H i)
    (ha : ∀ s i, 0 ≤ a s i)
    (hdetect : ∀ i, bad i → J ≤ ∑ s, a s i)
    (hcost : ∀ s, (∑ i, a s i * H i) ≤ V s) :
    (∑ i, if bad i then H i else 0) ≤ (∑ s, V s) / J := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.character_multiplier_le_four line 255
Source documentation
Every spectral multiplier of a finite-group character is at most four.
```
theorem character_multiplier_le_four {A : Type*} [AddCommGroup A] [Fintype A]
    (χ : AddChar A ℂ) (z : A) : ‖1 - χ z‖ ^ 2 ≤ 4 := by
…
```

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.character_root_bound line 264

Source documentation

Character-specialized root estimate. The root activity and multiplier are the actual complex character values, rather than unrelated predicates. This is the spectral aggregation step in the finite-tree obstruction.

theorem character_root_bound {A κ ν σ : Type*}
    [AddCommGroup A] [Fintype A] [Fintype κ] [Fintype ν] [Fintype σ]
    (H : AddChar A ℂ → ℝ) (root : A)
    (activeLeaf : κ → AddChar A ℂ → Prop) (bad : ν → AddChar A ℂ → Prop)
    (a : ν → σ → AddChar A ℂ → ℝ) (B : ν → ℝ) (C : κ → ℝ)
    (M ε K : ℝ) (hK : 0 < K) (hH : ∀ χ, 0 ≤ H χ)
    (hdense : ∀ χ, χ root ≠ 1 → (¬ ∃ v, bad v χ) →
      K ≤ ((Finset.univ.filter (fun u => activeLeaf u χ)).card : ℝ))
    (hleaf : ∀ u, 2 * (∑ χ, if activeLeaf u χ then H χ else 0) ≤ C u)
    (hleafBudget : (∑ u, C u) ≤ M)
    (ha : ∀ v s χ, 0 ≤ a v s χ)
    (hdetect : ∀ v χ, bad v χ → 1 ≤ ∑ s, a v s χ)
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.character_multiplier_average line 302
Source documentation
Full-period averaging detects a nontrivial character with multiplier two. Applied to a cyclic coordinate subgroup, this is the source's leaf test.
```
theorem character_multiplier_average {A : Type*} [AddCommGroup A] [Fintype A]
    (χ : AddChar A ℂ) :
    (∑ z : A, ‖1 - χ z‖ ^ 2) / (Fintype.card A : ℝ) =
      if χ = 0 then 0 else 2 := by
…
```

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.subgroup_average_spectral_mass line 323

Source documentation

Averaging the Fourier expansion along any finite subgroup homomorphism is twice the Fourier weight of characters nontrivial on that subgroup.

theorem subgroup_average_spectral_mass {A G : Type*}
    [AddCommGroup A] [Fintype A] [AddCommGroup G] [Fintype G]
    (φ : G →+ A) (H : AddChar A ℂ → ℝ) :
    (∑ z : G, ∑ χ : AddChar A ℂ, ‖1 - χ (φ z)‖ ^ 2 * H χ) /
        (Fintype.card G : ℝ) =
      2 * ∑ χ : AddChar A ℂ, if χ.compAddMonoidHom φ = 0 then 0 else H χ := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.zmod_character_eq_zero_iff line 346
Source documentation
A character on the finite cyclic group is trivial exactly when its value at the standard generator is one.
```
theorem zmod_character_eq_zero_iff (Q : ℕ) [NeZero Q]
    (χ : AddChar (ZMod Q) ℂ) : χ = 0 ↔ χ 1 = 1 := by
…
```

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.cyclic_average_spectral_mass line 360

Source documentation

The coordinate version of the full-period leaf test, expressed using the image of the cyclic generator. No injectivity of the subgroup map is needed.

theorem cyclic_average_spectral_mass {A : Type*}
    [AddCommGroup A] [Fintype A]
    (Q : ℕ) [NeZero Q] (φ : ZMod Q →+ A) (H : AddChar A ℂ → ℝ) :
    (∑ z : ZMod Q, ∑ χ : AddChar A ℂ, ‖1 - χ (φ z)‖ ^ 2 * H χ) /
        (Fintype.card (ZMod Q) : ℝ) =
      2 * ∑ χ : AddChar A ℂ, if χ (φ 1) = 1 then 0 else H χ := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.cyclic_active_mass_le line 375

Source documentation

A uniform upper bound on the displacement along a cyclic coordinate bounds twice the spectral mass active on that coordinate.

theorem cyclic_active_mass_le {A : Type*} [AddCommGroup A] [Fintype A]
    (Q : ℕ) [NeZero Q] (φ : ZMod Q →+ A) (H : AddChar A ℂ → ℝ) (C : ℝ)
    (hcost : ∀ z : ZMod Q, (∑ χ, ‖1 - χ (φ z)‖ ^ 2 * H χ) ≤ C) :
    2 * (∑ χ : AddChar A ℂ, if χ (φ 1) = 1 then 0 else H χ) ≤ C := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.root_bound_of_cyclic_leaf_tests line 392

Source documentation

Cyclic leaf-coordinate translation bounds imply the character root estimate.

theorem root_bound_of_cyclic_leaf_tests {A κ ν σ : Type*}
    [AddCommGroup A] [Fintype A] [Fintype κ] [Fintype ν] [Fintype σ]
    (Q : κ → ℕ) [∀ u, NeZero (Q u)] (φ : ∀ u, ZMod (Q u) →+ A)
    (H : AddChar A ℂ → ℝ) (root : A) (bad : ν → AddChar A ℂ → Prop)
    (a : ν → σ → AddChar A ℂ → ℝ) (B : ν → ℝ) (C : κ → ℝ)
    (M ε K : ℝ) (hK : 0 < K) (hH : ∀ χ, 0 ≤ H χ)
    (hdense : ∀ χ, χ root ≠ 1 → (¬ ∃ v, bad v χ) →
      K ≤ ((Finset.univ.filter (fun u => χ (φ u 1) ≠ 1)).card : ℝ))
    (hleaf : ∀ u (z : ZMod (Q u)),
      (∑ χ, ‖1 - χ (φ u z)‖ ^ 2 * H χ) ≤ C u)
    (hleafBudget : (∑ u, C u) ≤ M)
    (ha : ∀ v s χ, 0 ≤ a v s χ)
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.normalized_weighted_test_bound line 432

Source documentation

Normalizing finitely many tests preserves a uniform test budget.

theorem normalized_weighted_test_bound {ι σ : Type*}
    [Fintype ι] [Fintype σ] [Nonempty σ]
    (H : ι → ℝ) (a : σ → ι → ℝ) (B : ℝ)
    (hcost : ∀ s, (∑ i, a s i * H i) ≤ B) :
    (∑ s, ∑ i, (a s i / (Fintype.card σ : ℝ)) * H i) ≤ B := by
…

theorem OAI.TreeEdit.BinaryLower.TreeDistortion.FiniteMass.finite_spectral_root_bound line 452

Source documentation

Complete finite spectral aggregation with concrete leaf and internal translations. Geometry supplies the stated translation budgets; short-period averaging supplies hdetect; branching supplies hdense. No additional Fourier-mass or exceptional-union assertion is assumed.

theorem finite_spectral_root_bound {A κ ν σ : Type*}
    [AddCommGroup A] [Fintype A] [Fintype κ] [Fintype ν]
    [Fintype σ] [Nonempty σ]
    (Q : κ → ℕ) [∀ u, NeZero (Q u)] (φ : ∀ u, ZMod (Q u) →+ A)
    (H : AddChar A ℂ → ℝ) (root : A) (bad : ν → AddChar A ℂ → Prop)
    (shift : ν → σ → A) (B : ν → ℝ) (C : κ → ℝ)
    (M ε K : ℝ) (hK : 0 < K) (hH : ∀ χ, 0 ≤ H χ)
    (hdense : ∀ χ, χ root ≠ 1 → (¬ ∃ v, bad v χ) →
      K ≤ ((Finset.univ.filter (fun u => χ (φ u 1) ≠ 1)).card : ℝ))
    (hleaf : ∀ u (z : ZMod (Q u)),
      (∑ χ, ‖1 - χ (φ u z)‖ ^ 2 * H χ) ≤ C u)
    (hleafBudget : (∑ u, C u) ≤ M)
…