OAI/Analysis/LpDimension/Retractions.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubpolynomialLp.weightedProjection line 15
2. def OAI.SubpolynomialLp.retractions line 20
3. lemma OAI.SubpolynomialLp.retractions_convex line 24
4. lemma OAI.SubpolynomialLp.gramProjection_factor line 35
5. lemma OAI.SubpolynomialLp.sqrt_diagonal_inv line 42
6. lemma OAI.SubpolynomialLp.weightedProjection_mem line 48
7. lemma OAI.SubpolynomialLp.hilbertMul_diagonal line 68
8. lemma OAI.SubpolynomialLp.weightedProjection_energy line 72
9. def OAI.SubpolynomialLp.matrixRowNorm line 97
10. lemma OAI.SubpolynomialLp.matrixRowNorm_nonneg line 100
11. lemma OAI.SubpolynomialLp.matrixRowNorm_convex line 104
12. lemma OAI.SubpolynomialLp.projectionEnergy_convex line 115
13. def OAI.SubpolynomialLp.normalizedGradient line 134
14. lemma OAI.SubpolynomialLp.scaled_normalizedGradient line 138
15. lemma OAI.SubpolynomialLp.weightedProjection_rows line 150
16. lemma OAI.SubpolynomialLp.controlled_retraction line 184

    Source documentation

    A simultaneous retraction substitute for the fixed-point reweighting: it supplies the exact row bound and all finitely many tensor-energy bounds needed by the two constructions.

    lemma controlled_retraction {J : Type uJ} {H : Type uH} [Fintype J] [Nonempty E]
        [NormedAddCommGroup H] [InnerProductSpace ℝ H]
        (src dst : E → V) (δ lam : E → ℝ) (hδ : ∀ e, 0 < δ e)
        (hlam : ∀ e, 0 < lam e) (hls : ∑ e, lam e = 1)
        (hcard : 2 ≤ Fintype.card V)
        (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))
        (x : J → E → H) (hx : ∀ j e, ‖x j e‖^2 ≤ 1) :
        ∃ P ∈ retractions (normalizedGradient src dst δ),
          (∀ e, matrixRowNorm P e ≤ 4*Real.log (Fintype.card V : ℝ)) ∧
          (∀ j, (∑ e, lam e * ‖hilbertMul P (x j) e‖^2) ≤ 4) := by
    …

    Mentions: OAI.SubpolynomialLp.retractions, OAI.SubpolynomialLp.normalizedGradient, OAI.SubpolynomialLp.matrixRowNorm, OAI.SubpolynomialLp.hilbertMul