Mathlib.Analysis.WeightedCircularTube
Planar unit-circle tube infrastructure: radial power weights, uniform one-sided local mass bounds, finite positive annular normalizers, and reciprocal-scale separated nets.
Basic 8 core · 11 supporting This module supplies a neutral Euclidean-plane model of the unit circle, its inward and outward sides, and the radial power weight used for local volume calculations. ★ isCompact_unitCircle
Geometry and weights for a circular tube
This module supplies a neutral Euclidean-plane model of the unit circle, its inward and outward sides, and the radial power weight used for local volume calculations. The plane is represented by complex numbers, which carry the standard two-dimensional Euclidean metric and Lebesgue measure.
abbrev Plane reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
The Euclidean plane is represented by the complex numbers, equipped with their standard two-dimensional Euclidean metric and Lebesgue measure.
Definition (Lean source)
def
Plane :
Type
given by
ℂ
def unitCircle reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
The unit circle is the set of planar points whose Euclidean distance from the origin is one.
def radialOffset reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
For a planar point, its signed radial offset is its Euclidean distance from the origin minus one; it is negative inside the unit circle and positive outside it.
Definition (Lean source)
inductive CircleSide reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
The type of radial sides adjacent to the unit circle has an inside alternative, representing its interior, and an outside alternative, representing its strict exterior.
Definition (Lean source)
inductive
CircleSide :
Type
constructors
inside :
outside :
deriving DecidableEq
def region reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube.CircleSide
The region associated with a radial side is the closed interior of the unit circle for the inside side, and the strict exterior of the unit circle for the outside side.
Definition (Lean source)
def
given by
clause 1
| .inside => {z | radialOffset z ≤ 0}
clause 2
| .outside => {z | 0 < radialOffset z}
def powerWeight reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
For a real exponent parameter and a planar point, the radial power weight is the absolute radial offset raised to the power . On the unit circle itself the offset is zero, and zero to a negative power is zero by convention, so for exponents below two the weight is zero there rather than infinite; this affects only a Lebesgue-null set.
Definition (Lean source)
def sideBall reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
For a chosen radial side, a planar center, and a real radius, the one-sided ball is the open Euclidean ball with that center and radius, intersected with the region on the chosen side of the unit circle.
Definition (Lean source)
parameters
given by
ball x h ∩ side.region
theorem isCompact_unitCircle reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
The unit circle is compact in the Euclidean plane.
Formal statement
conclusion
Proof (Lean source)
theorem isCompact_unitCircle : IsCompact unitCircle := by
simpa only [unitCircle, sphere, Set.mem_ofPred_eq, dist_zero_right] using
(isCompact_sphere (0 : Plane) 1)
11 supporting declarations (lemmas, instances)
-
instDecidableEqCircleSideinstancederiving DecidableEq -
unitCircle_nonemptytheorem — The unit circle contains at least one planar point.conclusionunitCircle.NonemptyProof (Lean source)
theorem unitCircle_nonempty : unitCircle.Nonempty := by exact ⟨1, by simp [unitCircle]⟩ -
measurableSet_regiontheorem — For a chosen radial side, its radial region is Lebesgue measurable.Proof (Lean source)
theorem CircleSide.measurableSet_region (side : CircleSide) : MeasurableSet side.region := by cases side with | inside => exact measurableSet_le (continuous_norm.sub continuous_const).measurable measurable_const | outside => exact measurableSet_lt measurable_const (continuous_norm.sub continuous_const).measurable -
measurableSet_sideBalltheorem — For a chosen side, a planar center, and a radius, the corresponding one-sided ball is Lebesgue measurable.Proof (Lean source)
theorem measurableSet_sideBall (side : CircleSide) (x : Plane) (h : ℝ) : MeasurableSet (sideBall side x h) := by exact measurableSet_ball.inter (CircleSide.measurableSet_region side) -
continuous_powerWeighttheorem — When the exponent κ exceeds two, the radial power weight is continuous on the entire Euclidean plane, including the unit circle.Proof (Lean source)
theorem continuous_powerWeight {κ : ℝ} (hκ : 2 < κ) : Continuous (powerWeight κ) := by exact (Real.continuous_rpow_const (by linarith)).comp ((continuous_norm.sub continuous_const).abs) -
measurable_powerWeighttheorem — When the exponent κ exceeds two, the radial power weight is Lebesgue measurable.Proof (Lean source)
theorem measurable_powerWeight {κ : ℝ} (hκ : 2 < κ) : Measurable (powerWeight κ) := by exact (continuous_powerWeight hκ).measurable -
powerWeight_nonnegtheorem — For an exponent parameter and a planar point, the radial power weight is nonnegative.Proof (Lean source)
theorem powerWeight_nonneg (κ : ℝ) (z : Plane) : 0 ≤ powerWeight κ z := by exact Real.rpow_nonneg (abs_nonneg _) _ -
powerWeight_eq_zero_ifftheorem — When the exponent κ exceeds two, the radial power weight at a planar point vanishes exactly when that point is on the unit circle.Proof (Lean source)
theorem powerWeight_eq_zero_iff {κ : ℝ} (hκ : 2 < κ) (z : Plane) : powerWeight κ z = 0 ↔ z ∈ unitCircle := by rw [powerWeight, Real.rpow_eq_zero (abs_nonneg _) (by linarith)] simp only [abs_eq_zero, radialOffset, unitCircle, Set.mem_ofPred_eq, sub_eq_zero] -
integrableOn_powerWeight_sideBalltheorem — When the exponent κ exceeds two, the radial power weight is integrable over the one-sided ball determined by the chosen side, center, and radius.hypothesesconclusionProof (Lean source)
theorem integrableOn_powerWeight_sideBall {κ : ℝ} (hκ : 2 < κ) (side : CircleSide) (x : Plane) (h : ℝ) : IntegrableOn (powerWeight κ) (sideBall side x h) := by have hclosed : IntegrableOn (powerWeight κ) (closedBall x h) := (continuous_powerWeight hκ).locallyIntegrable.integrableOn_isCompact (isCompact_closedBall x h) exact Integrable.mono_measure hclosed (Measure.restrict_mono (inter_subset_left.trans ball_subset_closedBall) le_rfl) -
radialOffset_mul_of_mem_unitCircletheorem — If a complex multiplier lies on the unit circle, then multiplying any planar point by it preserves signed radial offset.Proof (Lean source)
theorem radialOffset_mul_of_mem_unitCircle {u : Plane} (hu : u ∈ unitCircle) (z : Plane) : radialOffset (u * z) = radialOffset z := by have hnorm : ‖u‖ = 1 := hu simp [radialOffset, hnorm] -
dist_mul_one_of_mem_unitCircletheorem — If a complex multiplier lies on the unit circle, then multiplication of a planar point by it preserves its distance from the reference point one.Proof (Lean source)
theorem dist_mul_one_of_mem_unitCircle {u : Plane} (hu : u ∈ unitCircle) (z : Plane) : dist (u * z) u = dist z 1 := by have hnorm : ‖u‖ = 1 := hu rw [dist_eq_norm, dist_eq_norm] calc ‖u * z - u‖ = ‖u * (z - 1)‖ := by ring_nf _ = ‖z - 1‖ := by rw [Complex.norm_mul, hnorm, one_mul]
Packing 4 core · 3 supporting This module constructs finite maximal separated subsets of the Euclidean unit circle and proves that their number of sites is proportional to the reciprocal of the separation scale. ★ unitCircle_maximalSeparated_card_bounds
Separated nets and packing bounds on the unit circle
This module constructs finite maximal separated subsets of the Euclidean unit circle and proves that their number of sites is proportional to the reciprocal of the separation scale. Its non-strict separation convention makes maximality imply coverage by open balls of the same radius.
def IsSeparatedAtLeast reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
For a real separation scale and a set of planar points, the property of being separated at least at that scale means that every two distinct points in the set are at distance at least the separation scale.
def IsMaximalSeparated reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
For a finite set of planar sites and a real separation scale, the property of being a maximal separated set on the unit circle means that the sites lie on the unit circle, are separated by at least that scale, and are maximal among all sets with both properties.
Definition (Lean source)
parameters
def
IsMaximalSeparated sites r :
Prop
given by
def CoversUnitCircle reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
For a finite set of planar sites and a real radius, the property of covering the unit circle means that every point of the unit circle belongs to an open ball of radius centred at one of the sites.
theorem unitCircle_maximalSeparated_card_bounds reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
There are positive universal constants with an ordered small-scale range such that every finite site set maximal at separation three times a positive scale in that range has open three-scale balls covering the unit circle and a number of sites comparable to the reciprocal scale.
Formal statement
conclusion
∃ cpack Cpack hstar : ℝ,
0 < cpack
cpack ≤ Cpack
0 < hstar
conclusion 1
Proof (Lean source)
theorem unitCircle_maximalSeparated_card_bounds :
∃ cpack Cpack hstar : ℝ,
0 < cpack ∧ cpack ≤ Cpack ∧ 0 < hstar ∧
∀ (h : ℝ) (sites : Finset Plane),
0 < h → h ≤ hstar → IsMaximalSeparated sites (3 * h) →
CoversUnitCircle sites (3 * h) ∧
cpack / h ≤ (sites.card : ℝ) ∧
(sites.card : ℝ) ≤ Cpack / h := by
refine ⟨1 / 4, 3, 1 / 6, by norm_num, by norm_num, by norm_num, ?_⟩
intro h sites hh hhsmall hmax
have hcover : CoversUnitCircle sites (3 * h) :=
unitCircle_maximalSeparated_covers (by positivity) hmax
exact ⟨hcover,
quarter_div_le_card_of_cover hh hhsmall hcover,
card_le_three_div_of_separated hh hhsmall hmax.prop.1 hmax.prop.2⟩
3 supporting declarations (lemmas, instances)
-
unitCircle_maximalSeparated_coverstheorem — When the separation radius is positive and a finite site set is inclusion-maximal at that non-strict separation radius, its open balls of that radius cover the unit circle.hypothesesconclusionCoversUnitCircle sites rProof (Lean source)
theorem unitCircle_maximalSeparated_covers {sites : Finset Plane} {r : ℝ} (hr : 0 < r) (hmax : IsMaximalSeparated sites r) : CoversUnitCircle sites r := by intro x hx by_contra hxcover simp only [mem_iUnion, mem_ball, not_exists] at hxcover have hxsites : x ∉ (sites : Set Plane) := by intro hxs have := hxcover x hxs simp [hr] at this have hsep : IsSeparatedAtLeast r (insert x (sites : Set Plane)) := by rw [IsSeparatedAtLeast, pairwise_insert] refine ⟨hmax.prop.2, ?_⟩ intro y hy hxy exact ⟨not_lt.mp (hxcover y hy), by simpa [dist_comm] using not_lt.mp (hxcover y hy)⟩ have hle : (sites : Set Plane) ⊆ insert x (sites : Set Plane) := subset_insert _ _ have hproper := hmax.eq_of_le ⟨Set.insert_subset hx hmax.prop.1, hsep⟩ hle exact hxsites (hproper ▸ mem_insert x (sites : Set Plane)) -
unitCircle_exists_finite_maximalSeparatedtheorem — At every positive separation radius, there exists a finite inclusion-maximal separated subset of the unit circle.Proof (Lean source)
theorem unitCircle_exists_finite_maximalSeparated {r : ℝ} (hr : 0 < r) : ∃ sites : Finset Plane, IsMaximalSeparated sites r := by let P : Set (Set Plane) := {s | s ⊆ unitCircle ∧ IsSeparatedAtLeast r s} obtain ⟨m, hm⟩ := zorn_subset P (by intro c hc hchain refine ⟨⋃₀ c, ?_, ?_⟩ · constructor · rintro x ⟨s, hs, hxs⟩ exact (hc hs).1 hxs · intro x hx y hy hxy obtain ⟨sx, hsx, hxsx⟩ := hx obtain ⟨sy, hsy, hxsy⟩ := hy rcases hchain.total hsx hsy with hsub | hsub · exact (hc hsy).2 (hsub hxsx) hxsy hxy · exact (hc hsx).2 hxsx (hsub hxsy) hxy · intro s hs exact subset_sUnion_of_mem hs) have hmfin : m.Finite := by let ε : ℝ≥0 := ⟨r / 3, by positivity⟩ obtain ⟨N, -, hNfin, hNcover⟩ := Metric.exists_finite_isCover_of_isCompact (s := unitCircle) (ε := ε) (by apply ne_of_gt change 0 < r / 3 linarith) isCompact_unitCircle let f : m → N := fun x => ⟨(hNcover (hm.prop.1 x.2)).choose, (hNcover (hm.prop.1 x.2)).choose_spec.1⟩ have hf : Injective f := by intro x y hxy apply Subtype.ext by_contra hne have hsep : r ≤ dist (x : Plane) y := hm.prop.2 x.2 y.2 hne have hxclose := (hNcover (hm.prop.1 x.2)).choose_spec.2 have hyclose := (hNcover (hm.prop.1 y.2)).choose_spec.2 change edist (x : Plane) (f x : Plane) ≤ (ε : ℝ≥0∞) at hxclose change edist (y : Plane) (f y : Plane) ≤ (ε : ℝ≥0∞) at hyclose have hdist : dist (x : Plane) y ≤ 2 * (r / 3) := by calc dist (x : Plane) y ≤ dist (x : Plane) (f x : Plane) + dist (f x : Plane) y := dist_triangle _ _ _ _ = dist (x : Plane) (f x : Plane) + dist (f y : Plane) y := by rw [hxy] _ ≤ r / 3 + r / 3 := by gcongr · rw [edist_dist, ENNReal.coe_nnreal_eq, ENNReal.ofReal_le_ofReal_iff (by positivity)] at hxclose change dist (x : Plane) (f x : Plane) ≤ r / 3 at hxclose exact hxclose · rw [edist_dist, ENNReal.coe_nnreal_eq, ENNReal.ofReal_le_ofReal_iff (by positivity)] at hyclose change dist (y : Plane) (f y : Plane) ≤ r / 3 at hyclose rw [dist_comm] exact hyclose _ = 2 * (r / 3) := by ring linarith letI : Finite N := Set.finite_coe_iff.mpr hNfin letI : Finite m := Finite.of_injective f hf exact Set.toFinite m refine ⟨hmfin.toFinset, ?_⟩ unfold IsMaximalSeparated rw [hmfin.coe_toFinset] change Maximal (fun s => s ∈ P) m exact hm -
unitCircle_exists_maximalSeparated_with_card_boundstheorem — There are positive universal constants with an ordered small-scale range such that at every positive scale in that range one can choose a finite site set maximal at separation three times that scale, whose open three-scale balls cover the unit circle and whose size is comparable to the reciprocal scale.conclusion∃ cpack Cpack hstar : ℝ,0 < cpackcpack ≤ Cpack0 < hstarconclusion 1h :ℝ0 < hh ≤ hstarIsMaximalSeparated sites (3 * h)CoversUnitCircle sites (3 * h)cpack / h ≤ (sites.card : ℝ)(sites.card : ℝ) ≤ Cpack / hProof (Lean source)
theorem unitCircle_exists_maximalSeparated_with_card_bounds : ∃ cpack Cpack hstar : ℝ, 0 < cpack ∧ cpack ≤ Cpack ∧ 0 < hstar ∧ ∀ (h : ℝ), 0 < h → h ≤ hstar → ∃ sites : Finset Plane, IsMaximalSeparated sites (3 * h) ∧ CoversUnitCircle sites (3 * h) ∧ cpack / h ≤ (sites.card : ℝ) ∧ (sites.card : ℝ) ≤ Cpack / h := by obtain ⟨cpack, Cpack, hstar, hcpos, hcC, hhstar, hbounds⟩ := unitCircle_maximalSeparated_card_bounds refine ⟨cpack, Cpack, hstar, hcpos, hcC, hhstar, ?_⟩ intro h hh hhstar' obtain ⟨sites, hmax⟩ := unitCircle_exists_finite_maximalSeparated (r := 3 * h) (by positivity) obtain ⟨hcover, hlower, hupper⟩ := hbounds h sites hh hhstar' hmax exact ⟨sites, hmax, hcover, hlower, hupper⟩
SideMass 4 core · 7 supporting This module proves uniform local-mass bounds for a radial power weight on both sides of the Euclidean unit circle. ★ unitCircle_powerWeighted_sideBall_bounds
Power-weighted mass on either side of the unit circle
This module proves uniform local-mass bounds for a radial power weight on both sides of the Euclidean unit circle. It also gives a finite, strictly positive normalizing integral on every nontrivial annular tube of width below one.
def sideBallMass reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
For a real exponent, a choice of the inside or outside of the unit circle, a planar centre, and a real radius, the weighted side-ball mass is the two-dimensional Lebesgue integral of the radial power weight with that exponent over the corresponding one-sided open ball. The integral is the real-valued Bochner integral, which is zero when the weight is not integrable there; the results below use it for exponents above two, where it is integrable.
Definition (Lean source)
parameters
def
sideBallMass κ side x h :
ℝ
given by
∫ z in sideBall side x h, powerWeight κ z ∂volume
theorem unitCircle_powerWeighted_sideBall_bounds reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
When the allowed exponent ceiling exceeds two and the maximum scale is positive and below one, there are positive constants, uniform over every unit-circle center, either radial side, all exponents strictly greater than two and at most that ceiling, and all positive scales up to that maximum, which bound one-sided weighted mass above and below by constant multiples of the scale to the exponent.
Formal statement
hypotheses
κMax h0 :
ℝ
hκMax :
2 < κMax
hh0pos :
0 < h0
hh0lt :
h0 < 1
conclusion
∃ c C : ℝ,
0 < c
c ≤ C
conclusion 1
c * h ^ κ ≤ sideBallMass κ side x h
sideBallMass κ side x h ≤ C * h ^ κ
Proof (Lean source)
theorem unitCircle_powerWeighted_sideBall_bounds
{κMax h0 : ℝ} (hκMax : 2 < κMax) (hh0pos : 0 < h0) (hh0lt : h0 < 1) :
∃ c C : ℝ, 0 < c ∧ c ≤ C ∧
∀ (κ : ℝ) (x : Plane) (side : CircleSide) (h : ℝ),
2 < κ → κ ≤ κMax → x ∈ unitCircle → 0 < h → h ≤ h0 →
c * h ^ κ ≤ sideBallMass κ side x h ∧
sideBallMass κ side x h ≤ C * h ^ κ := by
obtain ⟨c, C, hc, hcC, hbounds⟩ :=
reference_powerWeighted_sideBall_bounds hκMax hh0pos hh0lt
refine ⟨c, C, hc, hcC, ?_⟩
intro κ x side h hκ hκle hx hh hh0
rw [sideBallMass_eq_reference side hx]
exact hbounds κ side h hκ hκle hh hh0
def annularTube reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
For a real tube width, the annular tube is the set of planar points whose absolute radial distance from the unit circle is strictly less than .
Definition (Lean source)
def annularNormalizer reviewed
⚑ flagged
Causalean.Mathlib.Analysis.WeightedCircularTube
For a real exponent and a real tube width, the weighted annular normalizer is the two-dimensional Lebesgue integral of the radial power weight with that exponent over the annular tube of that width. The integral is the real-valued Bochner integral, which is zero when the weight is not integrable there; the results below use it for exponents above two, where it is integrable.
Definition (Lean source)
parameters
κ δ :
ℝ
def
annularNormalizer κ δ :
ℝ
given by
∫ z in annularTube δ, powerWeight κ z ∂volume
7 supporting declarations (lemmas, instances)
-
sideBallMass_integrabletheorem — When the exponent κ exceeds two, the radial power weight is integrable over the one-sided ball determined by the chosen side, center, and radius and hence its weighted mass is finite.hypothesesconclusionProof (Lean source)
theorem sideBallMass_integrable {κ : ℝ} (hκ : 2 < κ) (side : CircleSide) (x : Plane) (h : ℝ) : IntegrableOn (powerWeight κ) (sideBall side x h) := by exact integrableOn_powerWeight_sideBall hκ side x h -
sideBallMass_nonnegtheorem — When the exponent κ exceeds two, the weighted mass of the one-sided ball determined by the chosen side, center, and radius is nonnegative.hypothesesconclusion0 ≤ sideBallMass κ side x hProof (Lean source)
theorem sideBallMass_nonneg {κ : ℝ} (hκ : 2 < κ) (side : CircleSide) (x : Plane) (h : ℝ) : 0 ≤ sideBallMass κ side x h := by exact setIntegral_nonneg (measurableSet_sideBall side x h) (fun z _ => powerWeight_nonneg κ z) -
sideBallMass_eq_referencetheorem — For a chosen radial side and a center on the unit circle, rotating that center to the reference point one leaves its weighted side-ball mass unchanged.hypothesesconclusionsideBallMass κ side x h = sideBallMass κ side 1 hProof (Lean source)
theorem sideBallMass_eq_reference {κ h : ℝ} (side : CircleSide) {x : Plane} (hx : x ∈ unitCircle) : sideBallMass κ side x h = sideBallMass κ side 1 h := by let u : Circle := ⟨x, by simpa [unitCircle, Submonoid.unitSphere, mem_sphere, dist_zero_right] using hx⟩ let e : Plane ≃ₗᵢ[ℝ] Plane := rotation u have he_apply (z : Plane) : e z = x * z := rfl have he_meas : MeasurableEmbedding e := e.continuous.measurableEmbedding e.injective have he_pres : MeasurePreserving e volume volume := e.measurePreserving have hpre : e ⁻¹' sideBall side x h = sideBall side 1 h := by cases side with | inside => ext z change (dist (e z) x < h ∧ radialOffset (e z) ≤ 0) ↔ (dist z 1 < h ∧ radialOffset z ≤ 0) rw [he_apply, dist_mul_one_of_mem_unitCircle hx, radialOffset_mul_of_mem_unitCircle hx] | outside => ext z change (dist (e z) x < h ∧ 0 < radialOffset (e z)) ↔ (dist z 1 < h ∧ 0 < radialOffset z) rw [he_apply, dist_mul_one_of_mem_unitCircle hx, radialOffset_mul_of_mem_unitCircle hx] unfold sideBallMass rw [← he_pres.setIntegral_preimage_emb he_meas (powerWeight κ) (sideBall side x h), hpre] apply setIntegral_congr_fun (measurableSet_sideBall side 1 h) intro z hz change powerWeight κ (e z) = powerWeight κ z rw [he_apply] unfold powerWeight rw [radialOffset_mul_of_mem_unitCircle hx] -
reference_powerWeighted_sideBall_boundstheorem — When the allowed exponent ceiling exceeds two and the maximum scale is positive and below one, there are positive constants, uniform over both radial sides, all exponents between two and that ceiling, and all positive scales up to that maximum, which bound the reference one-sided weighted mass above and below by constant multiples of the scale to the exponent.hypothesesκMax h0 :ℝhκMax :2 < κMaxhh0pos :0 < h0hh0lt :h0 < 1conclusion∃ c C : ℝ,0 < cc ≤ Cconclusion 1c * h ^ κ ≤ sideBallMass κ side 1 hsideBallMass κ side 1 h ≤ C * h ^ κProof (Lean source)
theorem reference_powerWeighted_sideBall_bounds {κMax h0 : ℝ} (hκMax : 2 < κMax) (hh0pos : 0 < h0) (hh0lt : h0 < 1) : ∃ c C : ℝ, 0 < c ∧ c ≤ C ∧ ∀ (κ : ℝ) (side : CircleSide) (h : ℝ), 2 < κ → κ ≤ κMax → 0 < h → h ≤ h0 → c * h ^ κ ≤ sideBallMass κ side 1 h ∧ sideBallMass κ side 1 h ≤ C * h ^ κ := by refine ⟨Real.pi / 4 ^ κMax, pi, ?_, ?_, ?_⟩ · exact div_pos Real.pi_pos (Real.rpow_pos_of_pos (by norm_num) _) · have hpow : 1 ≤ (4 : ℝ) ^ κMax := Real.one_le_rpow (by norm_num) (by linarith) exact (div_le_iff₀ (Real.rpow_pos_of_pos (by norm_num) κMax)).2 (by nlinarith [Real.pi_pos]) · intro κ side h hκ hκle hh hh0 have hh1 : h < 1 := lt_of_le_of_lt hh0 hh0lt have hexp : 0 ≤ κ - 2 := by linarith have hsideint := integrableOn_powerWeight_sideBall hκ side (1 : Plane) h have hballint : IntegrableOn (powerWeight κ) (ball (1 : Plane) h) := by have hc : IntegrableOn (powerWeight κ) (closedBall (1 : Plane) h) := (continuous_powerWeight hκ).locallyIntegrable.integrableOn_isCompact (isCompact_closedBall (1 : Plane) h) exact Integrable.mono_measure hc (Measure.restrict_mono ball_subset_closedBall le_rfl) have hoff_upper : ∀ z ∈ ball (1 : Plane) h, powerWeight κ z ≤ h ^ (κ - 2) := by intro z hz have hoff : |radialOffset z| ≤ dist z 1 := by simpa [radialOffset, dist_eq_norm] using abs_norm_sub_norm_le z (1 : Plane) exact Real.rpow_le_rpow (abs_nonneg _) (hoff.trans (le_of_lt hz)) hexp have hmass_upper : sideBallMass κ side 1 h ≤ pi * h ^ κ := by have hset : sideBall side 1 h ⊆ ball (1 : Plane) h := inter_subset_left have hmono : sideBallMass κ side 1 h ≤ ∫ z in ball (1 : Plane) h, powerWeight κ z ∂volume := by exact setIntegral_mono_set hballint (Filter.Eventually.of_forall fun z => powerWeight_nonneg κ z) hset.eventuallyLE have hnorm := norm_setIntegral_le_of_norm_le_const (show volume (ball (1 : Plane) h) < ∞ from measure_ball_lt_top) (fun z hz => by rw [Real.norm_of_nonneg (powerWeight_nonneg κ z)] exact hoff_upper z hz) have hnonneg : 0 ≤ ∫ z in ball (1 : Plane) h, powerWeight κ z ∂volume := setIntegral_nonneg (s := ball (1 : Plane) h) measurableSet_ball (fun z _ => powerWeight_nonneg κ z) have hvol : volume.real (ball (1 : Plane) h) = h ^ 2 * pi := by simp [Measure.real, hh.le] rw [Real.norm_of_nonneg hnonneg, hvol] at hnorm calc sideBallMass κ side 1 h ≤ _ := hmono _ ≤ h ^ (κ - 2) * (h ^ 2 * pi) := hnorm _ = pi * h ^ κ := by rw [show κ = (κ - 2) + 2 by ring, Real.rpow_add hh, Real.rpow_two] ring_nf have hcompint : IntegrableOn (powerWeight κ) (comparisonBall side h) := Integrable.mono_measure hsideint (Measure.restrict_mono (comparisonBall_subset_sideBall side hh hh1) le_rfl) have hlower_point : ∀ z ∈ comparisonBall side h, (h / 4) ^ (κ - 2) ≤ powerWeight κ z := by intro z hz exact Real.rpow_le_rpow (by positivity) (comparisonBall_offset_lower side hh hh1 hz) hexp have hcomp_lower : pi * (h / 4) ^ κ ≤ ∫ z in comparisonBall side h, powerWeight κ z ∂volume := by have hfinite : volume (comparisonBall side h) ≠ ∞ := by exact (show volume (comparisonBall side h) < ∞ by cases side <;> exact measure_ball_lt_top).ne have hge := setIntegral_ge_of_const_le_real (show MeasurableSet (comparisonBall side h) by cases side <;> exact measurableSet_ball) hfinite hlower_point hcompint rw [comparisonBall_volume_real side hh] at hge calc pi * (h / 4) ^ κ = (h / 4) ^ (κ - 2) * ((h / 4) ^ 2 * pi) := by rw [show κ = (κ - 2) + 2 by ring, Real.rpow_add (by positivity), Real.rpow_two] ring_nf _ ≤ _ := hge have hcomp_mono : (∫ z in comparisonBall side h, powerWeight κ z ∂volume) ≤ sideBallMass κ side 1 h := by exact setIntegral_mono_set hsideint (Filter.Eventually.of_forall fun z => powerWeight_nonneg κ z) (comparisonBall_subset_sideBall side hh hh1).eventuallyLE have h4mono : (4 : ℝ) ^ κ ≤ 4 ^ κMax := Real.rpow_le_rpow_of_exponent_le (by norm_num) hκle have hdiv : h ^ κ / 4 ^ κMax ≤ h ^ κ / 4 ^ κ := div_le_div_of_nonneg_left (Real.rpow_nonneg hh.le κ) (Real.rpow_pos_of_pos (by norm_num) κ) h4mono have hscale : (pi / 4 ^ κMax) * h ^ κ ≤ pi * (h / 4) ^ κ := by calc (pi / 4 ^ κMax) * h ^ κ = pi * (h ^ κ / 4 ^ κMax) := by ring _ ≤ pi * (h ^ κ / 4 ^ κ) := mul_le_mul_of_nonneg_left hdiv Real.pi_pos.le _ = pi * (h / 4) ^ κ := by rw [Real.div_rpow hh.le (by norm_num : (0 : ℝ) ≤ 4)] exact ⟨hscale.trans (hcomp_lower.trans hcomp_mono), hmass_upper⟩ -
measurableSet_annularTubetheorem — For a tube width, the corresponding annular tube is Lebesgue measurable.Proof (Lean source)
theorem measurableSet_annularTube (δ : ℝ) : MeasurableSet (annularTube δ) := by exact measurableSet_lt ((continuous_norm.sub continuous_const).abs.measurable) measurable_const -
integrableOn_powerWeight_annularTubetheorem — When the exponent κ exceeds two and the tube width is below one, the radial power weight is integrable over that annular tube.Proof (Lean source)
theorem integrableOn_powerWeight_annularTube {κ δ : ℝ} (hκ : 2 < κ) (hδ : δ < 1) : IntegrableOn (powerWeight κ) (annularTube δ) := by have hsub : annularTube δ ⊆ closedBall (0 : Plane) 2 := by intro z hz have hoff : |radialOffset z| < 1 := lt_trans hz hδ have hnorm : ‖z‖ < 2 := by have := (le_abs_self (radialOffset z)).trans_lt hoff dsimp [radialOffset] at this linarith simpa [mem_closedBall, dist_zero_right] using hnorm.le have hclosed : IntegrableOn (powerWeight κ) (closedBall (0 : Plane) 2) := (continuous_powerWeight hκ).locallyIntegrable.integrableOn_isCompact (isCompact_closedBall (0 : Plane) 2) exact Integrable.mono_measure hclosed (Measure.restrict_mono hsub le_rfl) -
annularNormalizer_finite_postheorem — When the exponent κ exceeds two and the tube width is positive and below one, the radial power weight is integrable on that annular tube and its weighted normalizer is strictly positive.hypothesesκ δ :ℝhκ :2 < κhδpos :0 < δhδlt :δ < 1Proof (Lean source)
theorem annularNormalizer_finite_pos {κ δ : ℝ} (hκ : 2 < κ) (hδpos : 0 < δ) (hδlt : δ < 1) : IntegrableOn (powerWeight κ) (annularTube δ) ∧ 0 < annularNormalizer κ δ := by have hint := integrableOn_powerWeight_annularTube hκ hδlt refine ⟨hint, ?_⟩ obtain ⟨c, C, hc, hcC, hbounds⟩ := reference_powerWeighted_sideBall_bounds hκ hδpos hδlt have hb := (hbounds κ CircleSide.outside δ hκ (le_refl κ) hδpos (le_refl δ)).1 have hpowpos : 0 < δ ^ κ := Real.rpow_pos_of_pos hδpos κ have hsidepos : 0 < sideBallMass κ CircleSide.outside 1 δ := lt_of_lt_of_le (mul_pos hc hpowpos) hb have hsub : sideBall CircleSide.outside 1 δ ⊆ annularTube δ := by intro z hz rcases hz with ⟨hzball, hzside⟩ have hoffpos : 0 < radialOffset z := hzside have hoffle : |radialOffset z| ≤ dist z 1 := by simpa [radialOffset, dist_eq_norm] using abs_norm_sub_norm_le z (1 : Plane) exact lt_of_le_of_lt hoffle hzball have hmono : sideBallMass κ CircleSide.outside 1 δ ≤ annularNormalizer κ δ := by exact setIntegral_mono_set hint (Filter.Eventually.of_forall fun z => powerWeight_nonneg κ z) hsub.eventuallyLE exact hsidepos.trans_le hmono