OAI/Analysis/DiskMaximal/Kernels.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DyadicHats.tent line 30
2. lemma OAI.DyadicHats.tent_nonneg line 32
3. lemma OAI.DyadicHats.tent_le_one line 33
4. lemma OAI.DyadicHats.tent_pos_iff line 34
5. lemma OAI.DyadicHats.tent_eq_zero_of_one_le line 40
6. lemma OAI.DyadicHats.tent_of_nonneg line 42
7. lemma OAI.DyadicHats.tent_of_nonpos line 44
8. lemma OAI.DyadicHats.tent_neg line 47
9. lemma OAI.DyadicHats.lipschitz_tent line 49
10. theorem OAI.DyadicHats.tent_refine line 58
11. lemma OAI.DyadicHats.tent_floor line 83
12. lemma OAI.DyadicHats.tent_floor_succ line 85
13. lemma OAI.DyadicHats.tent_floor_partition line 88
14. lemma OAI.DyadicHats.tent_eq_zero_of_ne_floor line 91
15. lemma OAI.DyadicHats.summable_tent line 103
16. theorem OAI.DyadicHats.tsum_tent line 110

    Source documentation

    Partition of unity on the complete integer grid, including grid boundaries.

    theorem tsum_tent (x : ℝ) : (∑' j : ℤ, tent (x-j)) = 1 := by
    …

    Mentions: OAI.DyadicHats.tent

17. def OAI.DyadicHats.hat line 118

    Source documentation

    Actual Euclidean-plane product hats at a positive physical scale.

    def hat (r : ℝ) (p : ℤ × ℤ) (x : ℂ) : ℝ :=
    …

18. lemma OAI.DyadicHats.hat_nonneg line 120
19. lemma OAI.DyadicHats.hat_le_one line 122
20. lemma OAI.DyadicHats.continuous_hat line 126
21. lemma OAI.DyadicHats.summable_hat line 131
22. theorem OAI.DyadicHats.tsum_hat line 135
23. lemma OAI.DyadicHats.tent_half_integer line 141

    Source documentation

    One-dimensional refinement written with the actual interpolation weights.

    lemma tent_half_integer {j : ℤ} (hj : j ∉ Finset.Icc (-1) 1) : tent ((j:ℝ)/2) = 0 := by
    …

    Mentions: OAI.DyadicHats.tent

24. lemma OAI.DyadicHats.tent_half_refine line 152
25. lemma OAI.DyadicHats.tent_half_tsum_refine line 164
26. lemma OAI.DyadicHats.summable_tent_weight line 180
27. def OAI.DyadicHats.step line 188

    Source documentation

    Positive interpolation coefficients, indexed by coarse and fine grid indices.

    def step (p q : ℤ × ℤ) : ℝ :=
    …

28. lemma OAI.DyadicHats.step_nonneg line 190
29. lemma OAI.DyadicHats.step_column line 192
30. lemma OAI.DyadicHats.summable_step_hat line 200
31. theorem OAI.DyadicHats.hat_refine line 211

    Source documentation

    Exact planar hat refinement; no grid truncation is hidden in the identity.

    theorem hat_refine (r : ℝ) (p : ℤ × ℤ) (x : ℂ) :
        hat (2*r) p x = ∑' q : ℤ × ℤ, step p q*hat r q x := by
    …

    Mentions: OAI.DyadicHats.hat, OAI.DyadicHats.step

32. lemma OAI.PlanePotential.dim_complex line 235
33. lemma OAI.PlanePotential.volume_real_unit_ball line 237
34. lemma OAI.PlanePotential.integral_radial line 241
35. lemma OAI.PlanePotential.integrable_radial_iff line 248
36. lemma OAI.PlanePotential.radial_near_identity line 253
37. lemma OAI.PlanePotential.integrable_norm_rpow_near line 260
38. theorem OAI.PlanePotential.integral_norm_rpow_near line 273

    Source documentation

    Exact planar singular-kernel integral; the center point is not excluded by an unproved integrability convention.

    theorem integral_norm_rpow_near {a r : ℝ} (ha : -2 < a) (hr : 0 < r) :
        (∫ x in ball (0:ℂ) r, ‖x‖^a) = 2*Real.pi * (r^(a+2)/(a+2)) := by
    …

39. lemma OAI.PlanePotential.radial_far_identity line 289
40. lemma OAI.PlanePotential.integrable_norm_rpow_far line 296
41. theorem OAI.PlanePotential.integral_norm_rpow_far line 310
42. theorem OAI.PlanePotential.kernel_lp_three_halves line 331

    Source documentation

    Hölder followed by Tonelli gives the integral-kernel Minkowski estimate at p=3/2. Both measures and the actual joint kernel remain explicit.

    theorem kernel_lp_three_halves {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
        (μ : Measure α) (ν : Measure β) [SFinite μ] [SFinite ν]
        {K : α × β → ℝ≥0∞} (hK : Measurable K) {C : ℝ≥0∞}
        (hC : ∀ y, (∫⁻ x, (K (x,y))^(3/2:ℝ) ∂μ) ≤ C^(3/2:ℝ)) :
        (∫⁻ x, (∫⁻ y, K (x,y) ∂ν)^(3/2:ℝ) ∂μ) ≤ (C*ν univ)^(3/2:ℝ) := by
    …

43. structure OAI.FiniteLabels.Law line 374
44. instance OAI.FiniteLabels.(instance at line 379) line 379
45. def OAI.FiniteLabels.delta line 381
46. lemma OAI.FiniteLabels.law_le_one line 386
47. def OAI.FiniteLabels.move line 390
48. lemma OAI.FiniteLabels.move_apply line 398
49. def OAI.FiniteLabels.l1dist line 401
50. lemma OAI.FiniteLabels.l1dist_nonneg line 402
51. lemma OAI.FiniteLabels.l1dist_triangle line 403
52. theorem OAI.FiniteLabels.move_contract line 409

    Source documentation

    Stochastic matrices contract the l1 norm of every signed row difference.

    theorem move_contract (μ ν : Law ι) (P : ι → Law κ) :
        l1dist (move μ P) (move ν P) ≤ l1dist μ ν := by
    …

    Mentions: OAI.FiniteLabels.Law, OAI.FiniteLabels.l1dist, OAI.FiniteLabels.move

53. lemma OAI.FiniteLabels.move_rows line 428
54. lemma OAI.FiniteLabels.move_compare line 445
55. lemma OAI.FiniteLabels.expectation_difference line 449
56. def OAI.FiniteLabels.switchRow line 461
57. lemma OAI.FiniteLabels.switchRow_formula line 477
58. lemma OAI.FiniteLabels.delta_distance line 485
59. theorem OAI.FiniteLabels.switchRow_distance line 494

    Source documentation

    The row difference is paid by the actual switched mass, not by a bare Lipschitz constant. This is essential to the spatial comparison argument.

    theorem switchRow_distance [DecidableEq ι] (old : ι) (sample sample' : Law κ)
        (target : κ → ι) (p : κ → ℝ) (hp0 : ∀ z, 0 ≤ p z) (hp1 : ∀ z, p z ≤ 1) :
        l1dist (switchRow old sample target p hp0 hp1) (switchRow old sample' target p hp0 hp1)
          ≤ 2*∑ z, |sample z-sample' z| *p z := by
    …

    Mentions: OAI.FiniteLabels.Law, OAI.FiniteLabels.l1dist, OAI.FiniteLabels.switchRow

60. def OAI.PlanePotential.greenScalar line 528
61. def OAI.PlanePotential.green line 530
62. lemma OAI.PlanePotential.segment_support line 532
63. lemma OAI.PlanePotential.integrable_power_cutoff line 546
64. lemma OAI.PlanePotential.integral_power_cutoff line 551
65. lemma OAI.PlanePotential.singular_integral_bound line 557

    Source documentation

    A singular segment integral is genuinely integrable because of its geometric lower cutoff. The bound retains the exact power, rather than a supremum times 1.

    lemma singular_integral_bound {F : ℝ → ℝ} (hFm : Measurable F)
        {q δ B : ℝ} (hq : q < -1) (hδ : 0 < δ) (hB : 0 ≤ B)
        (hzero : ∀ t ∈ Ioc (0:ℝ) 1, t < δ → F t = 0)
        (hbound : ∀ t ∈ Ioc (0:ℝ) 1, |F t| ≤ B*t^q) :
        IntegrableOn F (Ioc (0:ℝ) 1) ∧
          |∫ t in Ioc (0:ℝ) 1, F t| ≤ B*(-(δ/2)^(q+1)/(q+1)) := by
    …

66. lemma OAI.PlanePotential.greenScalar_measurable line 591
67. lemma OAI.PlanePotential.green_measurable line 599
68. theorem OAI.PlanePotential.green_norm_bound line 604

    Source documentation

    Quantitative kernel size on every observation ball, with an explicit constant.

    theorem green_norm_bound {ψ : ℂ → ℝ} (hψm : Measurable ψ) {R X B : ℝ}
        (hψs : ∀ z, ψ z ≠ 0 → ‖z‖ ≤ R) (hψB : ∀ z, |ψ z| ≤ B)
        (hM : 0 < R+X) (hB : 0 ≤ B) {x y : ℂ} (hx : ‖x‖ ≤ X) (hxy : y ≠ x) :
        ‖green ψ x y‖ ≤ 2*B*(R+X)^2/‖y-x‖ := by
    …

    Mentions: OAI.PlanePotential.green

69. lemma OAI.PlanePotential.segment_integrand_measurable line 643
70. lemma OAI.PlanePotential.scalar_data line 650
71. theorem OAI.PlanePotential.green_difference_bound line 678

    Source documentation

    A difference bound proves the needed cancellation estimate without hiding any differentiation under the singular integral.

    theorem green_difference_bound {ψ : ℂ → ℝ} (hψm : Measurable ψ) {R X B L : ℝ}
        (hψs : ∀ z, ψ z ≠ 0 → ‖z‖ ≤ R) (hψB : ∀ z, |ψ z| ≤ B)
        (hψL : ∀ u v, |ψ u-ψ v| ≤ L*‖u-v‖)
        (hM : 0 < R+X) (hB : 0 ≤ B) (hL : 0 ≤ L)
        {x y z : ℂ} (hx : ‖x‖ ≤ X) (hzx : z ≠ x) (hyz : ‖y-z‖ ≤ ‖z-x‖/2) :
        ‖green ψ x y-green ψ x z‖ ≤
          (8*B*(R+X)^2+(64/3:ℝ)*L*(R+X)^3)*‖y-z‖/‖z-x‖^2 := by
    …

    Mentions: OAI.PlanePotential.green

72. theorem OAI.VectorRefinement.quadratic_defect line 773

    Source documentation

    Exact quadratic defect of a positive vector refinement, including zero parent mass.

    theorem quadratic_defect {ι E : Type*} [Fintype ι]
        [NormedAddCommGroup E] [InnerProductSpace ℝ E]
        (w a : ι → ℝ) (θ : ι → E) (n : E) (A : ℝ)
        (hn : ‖n‖ = 1) (hθ : ∀ i, ‖θ i‖ = 1)
        (href : A • n = ∑ i, (w i*a i) • θ i) :
        (∑ i, w i*a i)-A = (1/2:ℝ)*∑ i, w i*a i*‖θ i-n‖^2 := by
    …

73. lemma OAI.VectorRefinement.sq_norm_triangle line 788
74. theorem OAI.VectorRefinement.pair_defect_bound line 797

    Source documentation

    Two sufficiently represented children cannot have a large angular disagreement without spending the actual parent's triangle defect.

    theorem pair_defect_bound {ι E : Type*} [Fintype ι] [DecidableEq ι]
        [NormedAddCommGroup E] [InnerProductSpace ℝ E]
        (w a : ι → ℝ) (θ : ι → E) (n : E) (A : ℝ)
        (hw : ∀ i, 0 ≤ w i) (ha : ∀ i, 0 ≤ a i)
        (hn : ‖n‖ = 1) (hθ : ∀ i, ‖θ i‖ = 1)
        (href : A • n = ∑ i, (w i*a i) • θ i)
        {q s : ι} (hwaq : 1/4 ≤ w q) (hwas : 9/64 ≤ w s) (has : a q ≤ a s) :
        a q*‖θ q-θ s‖^2 ≤ 48*((∑ i, w i*a i)-A) := by
    …