OAI/Analysis/LipschitzHilbert/Phase/SourceAngularFrozenIntegration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The frozen long-tree integration keeps angular and spatial widths separate. Carrier removal supplies uniform reproduction on spatial cells.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.finite_angular_frozen_density_integral line 18
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.finite_angular_frozen_long_tree_bound line 80
  3. def OAI.LipschitzHilbert.SourceLabeledLattice.frozenWhitneyLocalAtWidth line 145
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenWhitneyLocalAtWidth_integrable line 152
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.angular_sum_subtype_product line 162
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.finite_angular_frozenWhitney_bound line 170
  7. def OAI.LipschitzHilbert.SourceLabeledLattice.frozenTreeValueAtWidth line 234
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.angular_frozen_tree_integrable_bound line 243