OAI/Analysis/LipschitzHilbert/Packets/AnalyzedLineFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual analyzing coefficients, normalized once, define the line packet family used in concentration. Their local budget is proved.

  1. def OAI.LipschitzHilbert.PlanarPacketFamily.coefficientScale line 19
  2. theorem OAI.LipschitzHilbert.PlanarPacketFamily.coefficientScale_pos line 21
  3. def OAI.LipschitzHilbert.PlanarPacketFamily.analyzedLine line 24
  4. theorem OAI.LipschitzHilbert.PlanarPacketFamily.analyzedLine_localBudget line 58