OAI/Analysis/SignedDisk/DiskGeometry2.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedDisk.DiskGeometry.pairCondition line 18
2. theorem OAI.SignedDisk.DiskGeometry.measurableSet_pairCondition line 22
3. theorem OAI.SignedDisk.DiskGeometry.volume_pairCondition line 31
4. def OAI.SignedDisk.DiskGeometry.pairMass line 50
5. theorem OAI.SignedDisk.DiskGeometry.measurable_pairMass line 53
6. def OAI.SignedDisk.DiskGeometry.rayIndicator line 57
7. theorem OAI.SignedDisk.DiskGeometry.measurable_rayIndicator line 60
8. theorem OAI.SignedDisk.DiskGeometry.lintegral_pairMass line 65

   Source documentation

   The first contribution to the Borel majorant is controlled by the two-point strip.

   theorem lintegral_pairMass (ν : Measure ℂ) [IsFiniteMeasure ν] {ρ δ : ℝ}
       (hρ : 0 < ρ) (hδ : 0 ≤ δ) (hδquarter : δ ≤ 1 / 4) :
       (∫⁻ x : ℂ, ∫⁻ z : ℂ, pairMass ν ρ δ x z ∂ν) ≤
         ENNReal.ofReal (156 * δ / ρ) * ν univ * ν univ := by
   …

   Mentions: OAI.SignedDisk.DiskGeometry.pairMass

9. theorem OAI.SignedDisk.DiskGeometry.lintegral_rayIndicator line 101

   Source documentation

   The second contribution is controlled by monotone ray jumps and polar coordinates.

   theorem lintegral_rayIndicator (ν S : Measure ℂ) [IsFiniteMeasure ν] [IsFiniteMeasure S]
       (ρ : ℝ) {T U v : ℝ} (hT : 0 ≤ T) (hU : 0 < U) (hv : 0 ≤ v) :
       (∫⁻ x : ℂ, ∫⁻ z : ℂ, rayIndicator S ρ T U v x z ∂ν) ≤
         (ENNReal.ofReal (6 * Real.pi) * ENNReal.ofReal (2 * v * (1 + T / U))) * ν univ := by
   …

   Mentions: OAI.SignedDisk.DiskGeometry.rayIndicator

10. theorem OAI.SignedDisk.DiskGeometry.bad_cap_bracket line 124

    Source documentation

    Failure of every cap forces the majorant bracket to be at least one.

    theorem bad_cap_bracket (S ν : Measure ℂ) [IsFiniteMeasure S] [IsFiniteMeasure ν]
        {x z : ℂ} {r ρ δ T U : ℝ} (hr : r ∈ Icc (1 : ℝ) 2)
        (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hδ : 0 < δ) (hδρ : δ ≤ ρ ^ 2 / 1600)
        (hT : 0 ≤ T) (hU : 0 < U) (hz : z ∈ thinShell x r δ)
        (hi : S (Metric.ball x (r - δ)) ≤ ENNReal.ofReal T)
        (hb : ENNReal.ofReal (2 * U) < (S + ν) (thinShell x r δ \ Metric.ball z ρ)) :
        1 ≤ (ENNReal.ofReal U)⁻¹ * pairMass ν ρ δ x z +
          rayIndicator S ρ T U (200 * δ / ρ ^ 2) x z := by
    …

    Mentions: OAI.SignedDisk.DiskGeometry.thinShell, OAI.SignedDisk.DiskGeometry.pairMass, OAI.SignedDisk.DiskGeometry.rayIndicator

11. def OAI.SignedDisk.DiskGeometry.shellMajorant line 169

    Source documentation

    A radius-independent Borel majorant combining separated shell pairs and ray jumps.

    def shellMajorant (ν S : Measure ℂ) (ρ δ T U : ℝ) (x : ℂ) : ℝ≥0∞ :=
    …

12. theorem OAI.SignedDisk.DiskGeometry.measurable_shellMajorant line 173
13. theorem OAI.SignedDisk.DiskGeometry.shellMajorant_eq_bracket line 178
14. theorem OAI.SignedDisk.DiskGeometry.lintegral_shellMajorant line 190

    Source documentation

    The majorant is integrable uniformly over all radii.

    theorem lintegral_shellMajorant (ν S : Measure ℂ) [IsFiniteMeasure ν] [IsFiniteMeasure S]
        {ρ δ T U : ℝ} (hρ : 0 < ρ) (hδ : 0 ≤ δ) (hδquarter : δ ≤ 1 / 4)
        (hT : 0 ≤ T) (hU : 0 < U) :
        (∫⁻ x, shellMajorant ν S ρ δ T U x) ≤
          (ENNReal.ofReal U)⁻¹ ^ 2 * (ENNReal.ofReal (156 * δ / ρ) * ν univ * ν univ) +
          (ENNReal.ofReal U)⁻¹ * ((ENNReal.ofReal (6 * Real.pi) *
            ENNReal.ofReal (2 * (200 * δ / ρ ^ 2) * (1 + T / U))) * ν univ) := by
    …

    Mentions: OAI.SignedDisk.DiskGeometry.shellMajorant

15. theorem OAI.SignedDisk.DiskGeometry.one_le_majorant_of_no_cap line 208

    Source documentation

    The majorant detects simultaneous failure of concentration at every cap.

    theorem one_le_majorant_of_no_cap (ν S : Measure ℂ) [IsFiniteMeasure ν] [IsFiniteMeasure S]
        {ρ δ T U : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hδ : 0 < δ)
        (hδρ : δ ≤ ρ ^ 2 / 1600) (hT : 0 ≤ T) (hU : 0 < U)
        {x : ℂ} {r : ℝ} (hr : r ∈ Icc (1 : ℝ) 2)
        (hν : ENNReal.ofReal U ≤ ν (thinShell x r δ))
        (hS : S (Metric.ball x (r - δ)) ≤ ENNReal.ofReal T)
        (hbad : ∀ z ∈ thinShell x r δ,
          ENNReal.ofReal (2 * U) < (S + ν) (thinShell x r δ \ Metric.ball z ρ)) :
        1 ≤ shellMajorant ν S ρ δ T U x := by
    …

    Mentions: OAI.SignedDisk.DiskGeometry.thinShell, OAI.SignedDisk.DiskGeometry.shellMajorant

16. theorem OAI.SignedDisk.DiskGeometry.shell_concentration line 236

    Source documentation

    Full radius-independent shell concentration, with explicit absolute constants.

    theorem shell_concentration (ν S : Measure ℂ) [IsFiniteMeasure ν] [IsFiniteMeasure S]
        {ρ δ T U : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hδ : 0 < δ)
        (hδρ : δ ≤ ρ ^ 2 / 1600) (hT : 0 ≤ T) (hU : 0 < U) :
        ∃ E : Set ℂ, MeasurableSet E ∧
          volume E ≤
            (ENNReal.ofReal U)⁻¹ ^ 2 * (ENNReal.ofReal (156 * δ / ρ) * ν univ * ν univ) +
            (ENNReal.ofReal U)⁻¹ * ((ENNReal.ofReal (6 * Real.pi) *
              ENNReal.ofReal (2 * (200 * δ / ρ ^ 2) * (1 + T / U))) * ν univ) ∧
          ∀ x ∉ E, ∀ r ∈ Icc (1 : ℝ) 2,
            ENNReal.ofReal U ≤ ν (thinShell x r δ) →
            S (Metric.ball x (r - δ)) ≤ ENNReal.ofReal T →
            ∃ z ∈ thinShell x r δ,
    …

    Mentions: OAI.SignedDisk.DiskGeometry.thinShell

17. def OAI.SignedDisk.DiskMoments.rotation line 273
18. lemma OAI.SignedDisk.DiskMoments.rotation_apply line 275
19. lemma OAI.SignedDisk.DiskMoments.rotation_zero line 279
20. lemma OAI.SignedDisk.DiskMoments.rotation_norm line 281
21. lemma OAI.SignedDisk.DiskMoments.integral_rotation line 284
22. lemma OAI.SignedDisk.DiskMoments.hasDerivAt_rotation line 295
23. theorem OAI.SignedDisk.DiskMoments.rotational_moment_zero line 305

    Source documentation

    The circulation moment of a smooth gradient on a disk vanishes.

    theorem rotational_moment_zero {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
        (x : ℂ) (r : ℝ) :
        (∫ z in Metric.ball 0 r, (fderiv ℝ g (x + z)) (Complex.I * z)) = 0 := by
    …

24. lemma OAI.SignedDisk.DiskMoments.integral_translate_ball line 347
25. lemma OAI.SignedDisk.DiskMoments.continuous_gradient line 357
26. lemma OAI.SignedDisk.DiskMoments.real_moment_integrand line 361
27. lemma OAI.SignedDisk.DiskMoments.imaginary_moment_integrand line 366
28. theorem OAI.SignedDisk.DiskMoments.imaginary_moment_zero line 373

    Source documentation

    The imaginary part of the actual complex disk moment is zero.

    theorem imaginary_moment_zero {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
        (x : ℂ) (r : ℝ) :
        (∫ y in Metric.ball x r, star (y - x) * gradient g y).im = 0 := by
    …

29. theorem OAI.SignedDisk.DiskMoments.hasDerivAt_integral_unitDisk line 391

    Source documentation

    Differentiate a disk average on its fixed unit-disk model.

    theorem hasDerivAt_integral_unitDisk {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
        (x : ℂ) (t : ℝ) :
        HasDerivAt (fun s : ℝ => ∫ z in Metric.ball (0 : ℂ) 1, g (x + s • z))
          (∫ z in Metric.ball (0 : ℂ) 1, (fderiv ℝ g (x + t • z)) z) t := by
    …

30. lemma OAI.SignedDisk.DiskMoments.integral_scale_ball line 432
31. def OAI.SignedDisk.DiskMoments.signedAverage line 440

    Source documentation

    Signed normalized average on a centered Euclidean disk in the complex plane.

    def signedAverage (g : ℂ → ℝ) (x : ℂ) (t : ℝ) : ℝ :=
    …

32. lemma OAI.SignedDisk.DiskMoments.signedAverage_fixedDomain line 443
33. lemma OAI.SignedDisk.DiskMoments.integral_fderiv_scale line 449
34. lemma OAI.SignedDisk.DiskMoments.integral_fderiv_moment_real line 464
35. theorem OAI.SignedDisk.DiskMoments.hasDerivAt_signedAverage line 478

    Source documentation

    The radial disk derivative is the real part of its complex moment.

    theorem hasDerivAt_signedAverage {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
        (x : ℂ) {t : ℝ} (ht : 0 < t) :
        HasDerivAt (signedAverage g x)
          ((∫ y in Metric.ball x t, star (y-x) * gradient g y).re / (Real.pi * t^3)) t := by
    …

    Mentions: OAI.SignedDisk.DiskMoments.signedAverage

36. lemma OAI.SignedDisk.DiskMoments.ball_ae_closedBall line 491
37. lemma OAI.SignedDisk.DiskMoments.continuous_integral_fderiv_unit line 498