Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

redefine upperRadius #214

Closed
wants to merge 3 commits into from
+9 −4
Closed

redefine upperRadius #214

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
71e74fa
Redefine upperRadius
js2357 Jan 19, 2025
4eb14b1
Prove (with a sorry) le_upperRadius
js2357 Jan 19, 2025
250f473
shorten proof of le_upperRadius
js2357 Jan 19, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 8 additions & 3 deletions Carleson/Defs.lean
View file
Original file line number Diff line number Diff line change
@@ -190,14 +190,19 @@ def CZOperator (K : X → X → ℂ) (r : ℝ) (f : X → ℂ) (x : X) : ℂ :=
∫ y in {y | dist x y ∈ Ici r}, K x y * f y

/-- `R_Q(θ, x)` defined in (1.0.20). -/
def upperRadius [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (x : X) : ℝ≥0∞ :=
sSup { r : ℝ≥0∞ | dist_{x, r.toReal} θ (Q x) < 1 }
def upperRadius [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (x : X) : ℝ :=
sSup { r : ℝ | dist_{x, r} θ (Q x) < 1 }

lemma le_upperRadius [FunctionDistances ℝ X] {Q : X → Θ X} {θ : Θ X} {x : X} {r : ℝ}
(hr : dist_{x, r} θ (Q x) < 1) : r ≤ upperRadius Q θ x := by
have bdd : BddAbove { r : ℝ | dist_{x, r} θ (Q x) < 1 } := by sorry
exact (Real.le_sSup_iff bdd ⟨r, hr⟩).mpr fun ε hε ↦ ⟨r, hr, add_lt_iff_neg_left.mpr hε⟩

/-- The linearized maximally truncated nontangential Calderon Zygmund operator `T_Q^θ` -/
def linearizedNontangentialOperator [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X)
(K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
⨆ (R₁ : ℝ) (x' : X) (_ : dist x x' ≤ R₁),
‖∫ y in {y | ENNReal.ofReal (dist x' y) ∈ Ioo (ENNReal.ofReal R₁) (upperRadius Q θ x')},
‖∫ y in {y | dist x' y ∈ Ioo R₁ (upperRadius Q θ x')},
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

With upperRadius in ENNReal, I would write this as

⨆ (R₁ : ℝ≥0) (x' : X) (_ : dist x x' ≤ R₁),
  ‖∫ y in {y | (nndist x' y : ℝ≥0∞) ∈ Ioo (R₁ : ℝ≥0∞) (upperRadius Q θ x')}, K x' y * f y‖ₑ

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  1. I'm not sure we want that. With the original version, the left-hand inequality of the Ioo statement has ENNReal.ofReal on both sides, so it's relatively easy to translate back to a real-valued inequality. In your new version, one side has an NNReal being cast to ENNReal and the other side has a real being cast to ENNReal. I don't have time to give it much thought right now, but it feels like that would be less convenient.
  2. This isn't directly relevant to what I'm currently working on, because I think the reference to linearizedNontangentialOperator in the blueprint's proof of Lemma 7.2.2 is a mistake. I think it should be nontangentialOperator instead (as appears correctly at the end of the proof).
  3. My proof is almost done now (and the heavy lifting is completely finished), so it might make more sense to discuss this after I PR it. It will include a lot of API for sets of the form {y | ENNReal.ofReal (dist x' y) ∈ Ioo r R}.

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh oops, I expect that an occurrence of linearizedNontangentialOperator in chapter 7 is indeed a mistake. My bad! (See CONTRIBUTING.md for the translation of symbols.)
And I'm also not sure if what I suggested is the best option.

I do expect that ENNReal.ofReal (dist x' y) is more conventiently written as edist x' y (so my (nndist x' y : ℝ≥0∞) above should also use edist)

K x' y * f y‖₊

/-- The maximally truncated nontangential Calderon Zygmund operator `T_*` -/
2 changes: 1 addition & 1 deletion Carleson/ForestOperator/PointwiseEstimate.lean
View file
Original file line number Diff line number Diff line change
@@ -631,7 +631,7 @@ lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L
le_iSup₂_of_le (𝔰 p') ⟨s_ineq, scale_mem_Icc.2⟩ <| le_iSup_of_le ?_ ?_
· have : ((D : ℝ≥0∞) ^ (𝔰 p' - 1)).toReal = D ^ (s₂ - 1) := by
rw [sp', ← ENNReal.toReal_zpow]; simp
apply le_sSup; rwa [mem_setOf, dist_congr rfl this]
apply le_upperRadius; convert d1
· convert le_rfl; change (Icc (𝔰 p) _).toFinset = _; rw [sp, sp']
apply subset_antisymm
· rw [← Finset.toFinset_coe (t.σ u x), toFinset_subset_toFinset]