OAI/Analysis/LipschitzHilbert/Trees/SourceWeightedEnvelopeKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Weighted tile envelopes are controlled by the actual strong maximal function. Only one quadratic top weight in each coordinate is needed.

  1. def OAI.LipschitzHilbert.topReciprocalWeight line 13
  2. theorem OAI.LipschitzHilbert.topReciprocalWeight_nonneg line 16
  3. theorem OAI.LipschitzHilbert.topReciprocalWeight_le_one line 20
  4. theorem OAI.LipschitzHilbert.topReciprocalWeight_measurable line 28
  5. theorem OAI.LipschitzHilbert.weighted_tile_envelope_transfer line 33
  6. theorem OAI.LipschitzHilbert.weighted_tile_kernel_bound line 48