OAI/Analysis/DiskMaximal/Refinement.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LabelSwitches.active line 49

   Source documentation

   Whether a switch has occurred since the most recent exceptional level.

   def active (bad sw : ℕ → Bool) : ℕ → Bool
     | 0 => false
     | n+1 => if bad n then false else active bad sw n || sw n

2. def OAI.LabelSwitches.count line 53
3. lemma OAI.LabelSwitches.active_witness line 55
4. theorem OAI.LabelSwitches.count_le line 77
5. theorem OAI.LabelSwitches.count_energy line 109

   Source documentation

   Quantitative energy version. The exceptional set is the union of marks and levels with energy exceeding c. This includes an arbitrary birth offset.

   theorem count_energy (mark sw : ℕ → Bool) (E : ℕ → ℝ) (n : ℕ) {c : ℝ}
       (hc : 0 < c) (hE : ∀ i < n, 0 ≤ E i)
       (hsep : ∀ i j, i < j → j < n → sw i = true → sw j = true →
         ∃ k, i ≤ k ∧ k ≤ j ∧ (mark k = true ∨ c < E k)) :
       ((count sw n : ℕ) : ℝ) ≤ 1+2*((count mark n : ℕ) : ℝ)+(2/c)*∑ i ∈ range n, E i := by
   …

   Mentions: OAI.LabelSwitches.count

6. lemma OAI.PlanePotential.green_eq_zero_of_outside line 149

   Source documentation

   The global segment kernel vanishes off the region on which the actual finite density decomposition is valid.

   lemma green_eq_zero_of_outside {ψ : ℂ → ℝ} {R X : ℝ}
       (hs : ∀ z, ψ z ≠ 0 → ‖z‖ ≤ R) (hRX : R ≤ X) {x y : ℂ}
       (hx : ‖x‖ ≤ X) (hy : X < ‖y‖) : green ψ x y = 0 := by
   …

   Mentions: OAI.PlanePotential.green

7. lemma OAI.PlanePotential.green_gradient_representation line 171
8. theorem OAI.PlanePotential.green_finite_decomposition line 178
9. theorem OAI.PlanePotential.green_decomposition_norm line 201

   Source documentation

   The complete finite Minkowski step, after genuine kernel insertion.

   theorem green_decomposition_norm {ι : Type*} [Fintype ι]
       {ψ g : ℂ → ℝ} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ)
       (hg : ContDiff ℝ 1 g) {D R X Y B : ℝ}
       (hD : ∀ y, ‖fderiv ℝ g y‖ ≤ D) (hψ1 : ∫ z, ψ z = 1)
       (hψs : ∀ z, ψ z ≠ 0 → ‖z‖ ≤ R) (hψB : ∀ z, |ψ z| ≤ B)
       (hRX : R ≤ X) (hM : 0 < R+X) (hB : 0 ≤ B) (hXY : 0 < X+Y)
       (β : ι → ℂ → ℂ) (hβ : ∀ i, Integrable (β i))
       (hβs : ∀ i y, β i y ≠ 0 → ‖y‖ ≤ Y)
       (hdecomp : ∀ᵐ y, ‖y‖ ≤ X → gradient g y = ∑ i, β i y) :
       eLpNorm (fun x => g x-∫ z, ψ z*g z) (3/2) (volume.restrict {x : ℂ | ‖x‖ ≤ X}) ≤
         ∑ i, eLpNorm (fun x => ∫ y, ⟪green ψ x y,β i y⟫) (3/2)
           (volume.restrict {x : ℂ | ‖x‖ ≤ X}) := by
   …

   Mentions: OAI.PlanePotential.green

10. def OAI.RadiusEnvelope.envelope line 234

    Source documentation

    The signed envelope over the entire compact real-radius interval.

    def envelope (u : ℝ → E → ℝ) (a b : ℝ) (x : E) : ℝ :=
    …

11. lemma OAI.RadiusEnvelope.attains line 237
12. lemma OAI.RadiusEnvelope.le_envelope line 249
13. lemma OAI.RadiusEnvelope.lipschitz line 255
14. lemma OAI.RadiusEnvelope.zero_of_all_zero line 278
15. theorem OAI.RadiusEnvelope.fderiv_touching line 286

    Source documentation

    Differentiable touching holds for every attaining radius; no derivative of an argmax selector is taken.

    theorem fderiv_touching [NormedAddCommGroup E] [NormedSpace ℝ E] {u : ℝ → E → ℝ} {a b r : ℝ} {x : E}
        (hr : r ∈ Icc a b) (hc : ∀ y, ContinuousOn (fun t => u t y) (Icc a b))
        (he : envelope u a b x = u r x)
        (hd : DifferentiableAt ℝ (envelope u a b) x) (hu : DifferentiableAt ℝ (u r) x) :
        fderiv ℝ (envelope u a b) x = fderiv ℝ (u r) x := by
    …

    Mentions: OAI.RadiusEnvelope.envelope

16. lemma OAI.DiskMoments.signedAverage_lipschitz line 304
17. lemma OAI.DiskMoments.signedAverage_radius_continuousOn line 328
18. lemma OAI.DiskMoments.hasFDerivAt_signedAverage line 334
19. theorem OAI.DiskMoments.run_envelope_lipschitz line 358

    Source documentation

    Actual signed run envelopes: locally differentiable almost everywhere, over all radii in their compact interval.

    theorem run_envelope_lipschitz {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
        (hgc : HasCompactSupport g) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
        ∃ L : ℝ≥0, LipschitzWith L (RadiusEnvelope.envelope (fun r x => signedAverage g x r) a b) := by
    …

    Mentions: OAI.RadiusEnvelope.envelope, OAI.DiskMoments.signedAverage

20. lemma OAI.DiskMoments.signedAverage_eq_zero_of_outside line 369
21. theorem OAI.DiskMoments.run_envelope_hasCompactSupport line 385

    Source documentation

    Every radius in the run is retained, but a common compact spatial support still exists.

    theorem run_envelope_hasCompactSupport {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
        (hgc : HasCompactSupport g) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
        HasCompactSupport (RadiusEnvelope.envelope (fun r x => signedAverage g x r) a b) := by
    …

    Mentions: OAI.RadiusEnvelope.envelope, OAI.DiskMoments.signedAverage

22. theorem OAI.DiskMoments.run_envelope_ae_touching line 404

    Source documentation

    AE differentiability and universal touching of actual run gradients.

    theorem run_envelope_ae_touching {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
        (hgc : HasCompactSupport g) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
        ∀ᵐ x, ∀ r ∈ Icc a b,
          RadiusEnvelope.envelope (fun r x => signedAverage g x r) a b x = signedAverage g x r →
          fderiv ℝ (RadiusEnvelope.envelope (fun r x => signedAverage g x r) a b) x =
            (1/Real.pi) • ∫ z in Metric.ball 0 1, fderiv ℝ g (x+r • z) := by
    …

    Mentions: OAI.RadiusEnvelope.envelope, OAI.DiskMoments.signedAverage

23. def OAI.DyadicHats.point line 423
24. def OAI.DyadicHats.boxNorm line 424
25. lemma OAI.DyadicHats.boxNorm_nonneg line 426
26. lemma OAI.DyadicHats.boxNorm_le_norm line 427
27. lemma OAI.DyadicHats.norm_le_two_boxNorm line 429
28. lemma OAI.DyadicHats.boxNorm_add_le line 434
29. lemma OAI.DyadicHats.boxNorm_neg line 438
30. lemma OAI.DyadicHats.boxNorm_sub_comm line 439
31. lemma OAI.DyadicHats.hat_pos_iff line 442
32. lemma OAI.DyadicHats.hat_ne_zero_iff line 457
33. lemma OAI.DyadicHats.support_hat_subset line 465
34. lemma OAI.DyadicHats.hasCompactSupport_hat line 471
35. lemma OAI.DyadicHats.lipschitz_hat line 477

    Source documentation

    Globally uniform spatial Lipschitz bound for the literal bilinear hats.

    lemma lipschitz_hat {r : ℝ} (hr : 0 < r) (p : ℤ × ℤ) :
        LipschitzWith (Real.toNNReal (2/r)) (hat r p) := by
    …

    Mentions: OAI.DyadicHats.hat

36. lemma OAI.DyadicHats.step_locality line 510
37. def OAI.DyadicHats.children line 544

    Source documentation

    Literal nine-child support of an adjacent dyadic refinement row.

    def children (p : ℤ × ℤ) : Finset (ℤ × ℤ) :=
    …

38. lemma OAI.DyadicHats.tent_half_zero line 547
39. lemma OAI.DyadicHats.step_zero_of_not_child line 557
40. lemma OAI.DyadicHats.hat_refine_finite line 565
41. def OAI.DyadicHats.vectorMass line 572

    Source documentation

    The vector mass of the actual density, not an abstract additive tree.

    def vectorMass (h : ℂ → ℂ) (r : ℝ) (p : ℤ × ℤ) : ℂ := ∫ y, hat r p y • h y

    Mentions: OAI.DyadicHats.hat

42. def OAI.DyadicHats.scalarMass line 574
43. lemma OAI.DyadicHats.integrable_hat_smul line 576
44. lemma OAI.DyadicHats.vectorMass_refine line 582
45. lemma OAI.DyadicHats.scalarMass_le_integral line 593
46. lemma OAI.DyadicHats.sum_scalarMass_le line 601

    Source documentation

    Any finite set of roots carries at most the total L1 density, uniformly in the scale. This proves the full-grid mass budget once finite support is used.

    lemma sum_scalarMass_le {h : ℂ → ℂ} (hh : Integrable h) (r : ℝ) (S : Finset (ℤ × ℤ)) :
        ∑ p ∈ S, scalarMass h r p ≤ ∫ y, ‖h y‖ := by
    …

    Mentions: OAI.DyadicHats.scalarMass

47. lemma OAI.DyadicHats.scalarMass_refine_le line 618
48. def OAI.DyadicHats.boundedIndices line 626

    Source documentation

    A finite index set that contains every hat meeting a fixed bounded region.

    def boundedIndices (r R : ℝ) : Finset (ℤ × ℤ) :=
    …

49. lemma OAI.DyadicHats.mem_boundedIndices line 629
50. lemma OAI.DyadicHats.vectorMass_zero_of_not_index line 654
51. lemma OAI.DyadicHats.finite_vectorMass_support line 668

    Source documentation

    Compactly supported actual densities have finitely many nonzero vector masses at each positive scale.

    lemma finite_vectorMass_support {h : ℂ → ℂ} (hc : HasCompactSupport h) {r : ℝ} (hr : 0 < r) :
        (Function.support (vectorMass h r)).Finite := by
    …

    Mentions: OAI.DyadicHats.vectorMass

52. theorem OAI.LipschitzWith.integral_fderiv_mul_eq_neg line 692

    Source documentation

    Genuine integration by parts for Lipschitz weights and compact Lipschitz potentials. Differentiability is required only almost everywhere, and follows from Rademacher rather than being a new premise.

    theorem integral_fderiv_mul_eq_neg (hf : LipschitzWith L f) (hg : LipschitzWith K g)
        (hgc : HasCompactSupport g) (v : E) :
        (∫ x, fderiv ℝ f x v * g x ∂μ) = -∫ x, fderiv ℝ g x v * f x ∂μ := by
    …

53. theorem OAI.LipschitzWith.locallyIntegrable_gradient line 705

    Source documentation

    The total gradient version obtained from Riesz and measurable fderiv is locally integrable, including on the nondifferentiability set.

    theorem locallyIntegrable_gradient (hf : LipschitzWith L f) :
        LocallyIntegrable (gradient f) μ := by
    …

54. theorem OAI.LipschitzWith.integrable_gradient line 716
55. theorem OAI.LipschitzWith.integral_mul_fderiv_eq_neg line 723
56. def OAI.DyadicHats.indexBox line 739
57. abbrev OAI.DyadicHats.Grid line 741
58. lemma OAI.DyadicHats.parent_in_box line 743
59. lemma OAI.DyadicHats.grid_step_column line 769

    Source documentation

    Restriction to a finite box retains the exact column normalization of the positive dyadic refinement matrix; it does not normalize its rows.

    lemma grid_step_column (N : ℕ) (q : Grid N) : (∑ p : Grid N, step p q) = 1 := by
    …

    Mentions: OAI.DyadicHats.Grid, OAI.DyadicHats.step

60. lemma OAI.DyadicHats.mem_indexBox_of_le line 777
61. lemma OAI.DyadicHats.hat_mul_zero_outside line 787
62. lemma OAI.DyadicHats.density_partition_grid line 797
63. lemma OAI.DyadicHats.density_refine_grid line 805
64. lemma OAI.DyadicHats.integrable_hat_mul line 817
65. def OAI.DyadicHats.scale line 823
66. lemma OAI.DyadicHats.scale_pos line 824
67. lemma OAI.DyadicHats.scale_succ line 825
68. lemma OAI.DyadicHats.le_scale line 829
69. lemma OAI.DyadicHats.scale_index_bound line 833