OAI/Analysis/LpDimension/ElectricalProjection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubpolynomialLp.conductorMatrix line 15
2. lemma OAI.SubpolynomialLp.conductorMatrix_gram line 19
3. lemma OAI.SubpolynomialLp.conductorMatrix_mul_apply line 34
4. lemma OAI.SubpolynomialLp.gram_heat_weighted line 41
5. lemma OAI.SubpolynomialLp.gram_heat_twice line 53
6. lemma OAI.SubpolynomialLp.vertexWeight_pos line 75
7. lemma OAI.SubpolynomialLp.graph_localization_positive line 89
8. lemma OAI.SubpolynomialLp.graph_localization_nonneg line 163
9. lemma OAI.SubpolynomialLp.orthogonal_sum_sq line 191
10. lemma OAI.SubpolynomialLp.symmetric_quadratic_bound_sq line 197
11. lemma OAI.SubpolynomialLp.graph_localization_quadratic line 246
12. lemma OAI.SubpolynomialLp.electrical_localization_complete line 266

    Source documentation

    The squared ℓ₂ form of electrical localization, for the complete graph used by the main upper-bound construction.

    lemma electrical_localization_complete (src dst : E → V) (c x : E → ℝ)
        (hc : ∀ e, 0 < c e)
        (hinc : ∀ i : V, ∃ e, src e = i ∨ dst e = i)
        (hconn : ∀ i j : V, i ≠ j → ∃ e,
          (src e = i ∧ dst e = j) ∨ (src e = j ∧ dst e = i)) :
        (∑ e, (∑ f, |gramProjection (conductorMatrix src dst c) e f| * x f)^2) ≤
          (2 * Real.log (Fintype.card V : ℝ))^2 * ∑ e, (x e)^2 := by
    …

    Mentions: OAI.SubpolynomialLp.gramProjection, OAI.SubpolynomialLp.conductorMatrix