OAI/Analysis/AncientFlat/Weighted/WeightedLocalCore.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FlatWeighted.sigma line 11
  2. def OAI.FlatWeighted.chart line 12
  3. def OAI.FlatWeighted.localDomain line 13
  4. def OAI.FlatWeighted.pullback line 15
  5. def OAI.FlatWeighted.YBound line 18
  6. def OAI.FlatWeighted.holderNorm line 21
  7. def OAI.FlatWeighted.yNorm line 24
  8. def OAI.FlatWeighted.normalizedSource line 27