OAI/Analysis/DiskMaximal/Localization.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NullLocalization.unitRegion line 57
  2. lemma OAI.NullLocalization.unitRegion_compact line 58
  3. lemma OAI.NullLocalization.unitRegion_measurable line 60
  4. lemma OAI.NullLocalization.unitRegion_finite line 61
  5. lemma OAI.NullLocalization.unit_poincare line 65

    Source documentation

    A fixed-radius Poincare inequality derived from the proved Green kernel, not added as a Sobolev axiom. The subsequent cutoff is one on the radius-four disk.

    lemma unit_poincare : ∃ P : ℝ, 0 ≤ P ∧ ∀ {g : ℂ → ℝ},
    ContDiff ℝ 1 g → HasCompactSupport g → ∃ c : ℝ,
    (∫ x in unitRegion, ‖g x-c‖) ≤ P*(∫ x in unitRegion, ‖gradient g x‖) := by
…

    Mentions: OAI.NullLocalization.unitRegion

  6. def OAI.NullLocalization.unitCutoff line 130
  7. lemma OAI.NullLocalization.unit_localization line 132
  8. def OAI.NullLocalization.region line 189
  9. lemma OAI.NullLocalization.region_measurable line 190
  10. lemma OAI.NullLocalization.integral_stretch line 193
  11. lemma OAI.NullLocalization.norm_toUnit line 199
  12. lemma OAI.NullLocalization.comp_stretch_compact line 202
  13. lemma OAI.NullLocalization.comp_toUnit_compact line 206
  14. lemma OAI.NullLocalization.gradient_toUnit line 210
  15. lemma OAI.NullLocalization.integral_gradient_toUnit line 219
  16. lemma OAI.NullLocalization.local_integral_gradient_stretch line 230
  17. lemma OAI.NullLocalization.physical_localization line 251
  18. lemma OAI.NullLocalization.band_sub_local line 279
  19. lemma OAI.NullLocalization.gradient_band_local line 306
  20. lemma OAI.NullLocalization.mem_cell_norm line 319
  21. lemma OAI.NullLocalization.smooth_local_band line 325
  22. lemma OAI.NullLocalization.region_indices line 359
  23. lemma OAI.NullLocalization.regions_overlap line 368
  24. def OAI.NullLocalization.touches line 377
  25. def OAI.NullLocalization.usedRegion line 379
  26. lemma OAI.NullLocalization.usedRegion_measurable line 383
  27. lemma OAI.NullLocalization.usedRegion_subset line 389
  28. lemma OAI.NullLocalization.usedRegion_budget line 407
  29. lemma OAI.NullLocalization.smooth_small_local_budget line 446