OAI/Analysis/SignedDisk/Main.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedDisk.SobolevBand.band line 33
  2. lemma OAI.SignedDisk.SobolevBand.smooth_average_lipschitz line 35
  3. lemma OAI.SignedDisk.SobolevBand.smooth_band_lipschitz line 55
  4. lemma OAI.SignedDisk.SobolevBand.geometric_band_eq line 63
  5. lemma OAI.SignedDisk.SobolevBand.smooth_band_integrable_gradient line 69
  6. lemma OAI.SignedDisk.SobolevBand.smooth_dyadic_bound line 75
  7. lemma OAI.SignedDisk.WeakSobolev.HasGradient.comp_isometry line 91
  8. lemma OAI.SignedDisk.CenteredDiskEndpoint.hasGradient_iff_hasWeakGradient line 113
  9. def OAI.SignedDisk.CenteredDiskEndpoint.complexPlane line 147

    Source documentation

    The coordinate isometry preserves Euclidean, not max-product, norms.

    def complexPlane : ℂ ≃ₗᵢ[ℝ] Plane := Complex.orthonormalBasisOneI.repr

    Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane

  10. lemma OAI.SignedDisk.CenteredDiskEndpoint.integrable_comp_complexPlane line 149
  11. lemma OAI.SignedDisk.CenteredDiskEndpoint.integrable_comp_complexPlane_symm line 153
  12. lemma OAI.SignedDisk.CenteredDiskEndpoint.locallyIntegrable_comp_complexPlane line 157
  13. lemma OAI.SignedDisk.CenteredDiskEndpoint.gradientNorm_comp_complexPlane line 164
  14. lemma OAI.SignedDisk.CenteredDiskEndpoint.gradientNorm_comp_complexPlane_symm line 169
  15. lemma OAI.SignedDisk.SobolevBand.band_self line 181
  16. def OAI.SignedDisk.SobolevBand.diskKernel line 187

    Source documentation

    The normalized open-disk kernel, without an absolute value on the input.

    def diskKernel (a : ℝ) : ℂ → ℝ :=
…
  17. lemma OAI.SignedDisk.SobolevBand.diskKernel_nonneg line 190
  18. lemma OAI.SignedDisk.SobolevBand.diskKernel_integrable line 195
  19. lemma OAI.SignedDisk.SobolevBand.diskKernel_integral_abs line 198
  20. lemma OAI.SignedDisk.SobolevBand.diskKernel_convolution line 208
  21. lemma OAI.SignedDisk.SobolevBand.smooth_band_self_bound line 224
  22. theorem OAI.SignedDisk.SobolevBand.smooth_dyadic_bound_including_zero line 240

    Source documentation

    The natural index includes zero, with one absolute constant for both cases.

    theorem smooth_dyadic_bound_including_zero : ∃ C : ℝ, 0 ≤ C ∧
    ∀ {f : ℂ → ℝ}, ContDiff ℝ 1 f → HasCompactSupport f →
    ∀ {a : ℝ}, 0 < a → ∀ m : ℕ,
      (∫ x, ‖gradient (band f a ((2 : ℝ)^m*a)) x‖) ≤ C*(∫ x, ‖gradient f x‖) := by
…

    Mentions: OAI.SignedDisk.SobolevBand.band

  23. theorem OAI.SignedDisk.CenteredDiskEndpoint.plane_finiteDimensional line 264
  24. theorem OAI.SignedDisk.CenteredDiskEndpoint.plane_borelSpace line 266
  25. theorem OAI.SignedDisk.CenteredDiskEndpoint.plane_completeSpace line 268
  26. lemma OAI.SignedDisk.CenteredDiskEndpoint.signedAverage_comp_complexPlane line 270
  27. lemma OAI.SignedDisk.CenteredDiskEndpoint.signedBand_comp_complexPlane line 279
  28. lemma OAI.SignedDisk.CenteredDiskEndpoint.gradient_comp_complexPlane line 284
  29. theorem OAI.SignedDisk.CenteredDiskEndpoint.main_signed_finite_band line 296

    Distinct definitions of this name: ComparatorChallenges/SignedFiniteBand.lean:45 (same statement text; different proof or body). Qualify references as OAI.SignedDisk.CenteredDiskEndpoint.main_signed_finite_band@path.