OAI/Analysis/LipschitzHilbert/Trees/SourceCellPolynomial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial weights on the actual transverse cells of a tree. The exponent is kept symbolic so the fixed high order need not expand.

  1. theorem OAI.LipschitzHilbert.transverse_cell_polynomial_lower line 11
  2. theorem OAI.LipschitzHilbert.transverse_cell_polynomial_weight line 27
  3. theorem OAI.LipschitzHilbert.transverse_cell_weighted_norm line 36

    Source documentation

    Multiplication by the transverse polynomial supplies the precise power needed to absorb the density loss on that cell.

    theorem transverse_cell_weighted_norm {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (b W n y : ℝ) (q : ℕ) (hW : 0<W) (hy : |y-b-n*W|≤W/2) (v : E) :
    (1+|n|)^(2*q)*‖v‖≤32^q*‖polynomialWeight b (2*W) q y • v‖ := by
…

    Mentions: OAI.LipschitzHilbert.polynomialWeight

  4. theorem OAI.LipschitzHilbert.transverse_cell_weighted_norm_sq line 45

    Source documentation

    Squaring gives the exponent 4q in the cell-supremum energy.

    theorem transverse_cell_weighted_norm_sq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (b W n y : ℝ) (q : ℕ) (hW : 0<W) (hy : |y-b-n*W|≤W/2) (v : E) :
    (1+|n|)^(4*q)*‖v‖^2≤32^(2*q)*‖polynomialWeight b (2*W) q y • v‖^2 := by
…

    Mentions: OAI.LipschitzHilbert.polynomialWeight