OAI/MathematicalPhysics/PEPSSubvolume/HarmonicWeights.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite geometric buffers with controlled quadratic weight.

  1. def OAI.PolynomialPEPS.Subvolume.HarmonicWeights.mass line 23
  2. lemma OAI.PolynomialPEPS.Subvolume.HarmonicWeights.mass_nonneg line 25
  3. lemma OAI.PolynomialPEPS.Subvolume.HarmonicWeights.mass_doubling line 29
  4. lemma OAI.PolynomialPEPS.Subvolume.HarmonicWeights.mass_ge_blocks line 50
  5. def OAI.PolynomialPEPS.Subvolume.HarmonicWeights.weight line 62
  6. lemma OAI.PolynomialPEPS.Subvolume.HarmonicWeights.mass_pos line 64
  7. lemma OAI.PolynomialPEPS.Subvolume.HarmonicWeights.weight_pos line 71
  8. lemma OAI.PolynomialPEPS.Subvolume.HarmonicWeights.sum_weight line 77
  9. lemma OAI.PolynomialPEPS.Subvolume.HarmonicWeights.weight_le line 88
  10. lemma OAI.PolynomialPEPS.Subvolume.HarmonicWeights.energy_mass line 96
  11. theorem OAI.PolynomialPEPS.Subvolume.HarmonicWeights.buffer_weights line 114