Assumptions needed for Lemma 3.0.4

Stream: Carleson

[Jeremy Tan]

I'm looking at Lemma 3.0.4. In order to prove it I need finitary_carleson, which in turn needs ProofData.

But ProofData contains the fields

F_subset : F ⊆ ball (cancelPt X) (defaultD a ^ defaultS X / 4)
G_subset : G ⊆ ball (cancelPt X) (defaultD a ^ defaultS X / 4)

and currently defaultS (defined from PreProofData) does not take into account these two hypotheses. On the other hand, the blueprint says that "Let $S$ be the smallest integer such that the ranges of $\sigma_1$ and $\sigma_2$ are contained in $[-S,S]$ and $F$ and $G$ are contained in the ball $B(o,\frac14D^S)$."

Two questions:

1. Can I assume that F and G are bounded and measurable throughout the entire project? (Blueprint in section 2 and Lemma 1.0.3 says they are "bounded Borel sets", and I take "Borel" to imply "measurable". But Lemma 1.0.2 does not say F and G are bounded.) I think that with those assumptions in PreProofData I can define defaultS so as to satisfy F_subset and G_subset properly.
2. Can I also move hasBoundedStrongType_Tstar to KernelProofData? (This assumption is otherwise not in Truncation.lean, where Lemma 3.0.4 is stated.)

[Jeremy Tan]

i.e. I'm asking if I can do this:

class KernelProofData {X : Type*} (a : outParam ℕ) (K : outParam (X → X → ℂ))
    [PseudoMetricSpace X] where
  d : DoublingMeasure X (defaultA a)
  four_le_a : 4 ≤ a
  cf : CompatibleFunctions ℝ X (defaultA a)
  hcz : IsOneSidedKernel a K
  hasBoundedStrongType_Tstar : -- moved up
    HasBoundedStrongType (nontangentialOperator K · ·) 2 2 volume volume (C_Ts a)

class PreProofData {X : Type*} (a : outParam ℕ) (q : outParam ℝ) (K : outParam (X → X → ℂ))
  (σ₁ σ₂ : outParam (X → ℤ)) (F G : outParam (Set X)) [PseudoMetricSpace X] extends
    KernelProofData a K where
  c : IsCancellative X (defaultτ a)
  isBounded_F : IsBounded F -- new
  isBounded_G : IsBounded G -- new
  measurableSet_F : MeasurableSet F
  measurableSet_G : MeasurableSet G
  measurable_σ₁ : Measurable σ₁
  measurable_σ₂ : Measurable σ₂
  finite_range_σ₁ : (range σ₁).Finite
  finite_range_σ₂ : (range σ₂).Finite
  σ₁_le_σ₂ : σ₁ ≤ σ₂
  Q : SimpleFunc X (Θ X)
  q_mem_Ioc : q ∈ Ioc 1 2

[Jeremy Tan]

I see that tile_sum_operator's proof relies on G_subset critically, so I guess I'll have to add IsBounded G to PreProofData. On the other hand, volume_F_pos is not used at all and volume_G_pos is only used in two calc steps (one each in the proofs of the forest complement and union lemmas) – and the equations they appear in are still true when volume G = 0!

[Jeremy Tan]

In fpvandoorn/carleson#389 I make all the changes posited above – PreProofData gains new assumptions isBounded_F/G, which allows redefining defaultS such that F/G_subset are true. Thus PreProofData is renamed ProofData, having absorbed everything in ProofData that needed to be absorbed, and the former ProofData doesn't exist anymore

[Jeremy Tan]

It seems I can indeed make the assumption that F, G are bounded – metric_space_carleson is used only in two_sided_carleson, which is used only in real_carleson, which is used only in Lemma 11.6.4. The proof of the last one only applies real_carleson when F = Icc (-π) (3 * π) and G is a subset of Icc 0 (2 * π)

[Floris van Doorn]

metric_space_carleson is the main result of the project. We want to have it as general as possible, and not add additional assumptions to it, even if those assumptions are true when deriving classical_carleson. So we do not want to assume that F and G are bounded everywhere.

In chapter 3 we are showing that to derive metric_space_carleson, we can assume some additional assumptions (like boundedness of F and G) that are not present in the statement of the theorem.

[Floris van Doorn]

You are indeed correct that defaultS was misformalized, and that change is very welcome!

[Floris van Doorn]

The above means that chapter 3 might need a bit more thought when formalizing. Throughout chapters 4-7 we assume a large number of hypotheses (ProofData). In chapter 3, most lemmas have their own set of hypotheses, and sometimes we might apply a lemma many times with different sets F/G, so this might require defining some new structures to deal with these arguments (as you can see in fpvandoorn/carleson#363).

[Floris van Doorn]

It's possible that we never actually use volume F > 0 or volume G > 0 in chapters 4-7, but please don't remove them from ProofData yet, since we're not yet done with the argument. Note that we can easily get these assumptions by case distinction. metric_space_carleson is easily proven if either of these assumptions is false.

[Floris van Doorn]

In Lemma 3.0.4 the F and G are still bounded. This is implicit in the formulation of the lemma, and I might have misformalized it. In Lemma 3.0.2 we do not assume that F and G are bounded, and the proof explicitly gives an argument that works without this assumption.

[Floris van Doorn]

That said, we should indeed assume IsBounded F and IsBounded G in PreProofData, so that we can correctly define S.

[Jeremy Tan]

@Floris van Doorn I started on Lemma 3.0.4 proper, but I cannot claim it and cannot make progress because I am running into instance diamonds.

import Carleson.FinitaryCarleson
import Carleson.MetricCarleson.Basic

open scoped NNReal
open MeasureTheory Set ENNReal Filter Topology ShortVariables Bornology Metric Complex

noncomputable section

variable {X : Type*} {a : ℕ} [MetricSpace X] {q q' : ℝ≥0} {C : ℝ} {F G : Set X} {K : X → X → ℂ}
variable [KernelProofData a K] {x : X} {θ : Θ X} {R₁ R₂ : ℝ} {Q : SimpleFunc X (Θ X)}
variable {F G : Set X} {f : X → ℂ} {s : ℤ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)]

/-- The operator T_{2, σ₁, σ₂} introduced in Lemma 3.0.4. -/
def T_lin (Q : SimpleFunc X (Θ X)) (σ₁ σ₂ : X → ℤ) (f : X → ℂ) (x : X) : ℂ :=
  ∑ s ∈ Finset.Icc (σ₁ x) (σ₂ x), ∫ y, Ks s x y * f y * exp (I * Q x y)

theorem finitary_carleson_step (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')
    (bF : IsBounded F) (bG : IsBounded G) (mF : MeasurableSet F) (mG : MeasurableSet G)
    (mσ₁ : Measurable σ₁) (mσ₂ : Measurable σ₂) (rσ₁ : (range σ₁).Finite) (rσ₂ : (range σ₂).Finite)
    (lσ : σ₁ ≤ σ₂) (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1) :
    ∃ G' ⊆ G, IsBounded G' ∧ MeasurableSet G' ∧ 2 * volume G' ≤ volume G ∧
    ∫⁻ x in G \ G', ‖T_lin Q σ₁ σ₂ f x‖ₑ ≤
    C2_0_1 a q * (volume G) ^ (q' : ℝ)⁻¹ * (volume F) ^ (q : ℝ)⁻¹ := by
  rcases eq_zero_or_pos (volume G) with vG | vG
  · use ∅, empty_subset _, isBounded_empty, MeasurableSet.empty
    simp only [measure_empty, mul_zero, zero_le, diff_empty, true_and]
    rw [setLIntegral_measure_zero _ _ vG]; exact zero_le _
  rcases eq_zero_or_pos (volume F) with vF | vF
  · use ∅, empty_subset _, isBounded_empty, MeasurableSet.empty
    simp only [measure_empty, mul_zero, zero_le, diff_empty, true_and]
    suffices ∀ x, ‖T_lin Q σ₁ σ₂ f x‖ₑ = 0 by
      rw [lintegral_congr this, lintegral_zero]; exact zero_le _
    intro x; rw [enorm_eq_zero]; refine Finset.sum_eq_zero fun s ms ↦ integral_eq_zero_of_ae ?_
    classical
    convert ite_ae_eq_of_measure_zero (fun y ↦ Ks s x y * f y * exp (I * Q x y)) 0 F vF using 1
    ext y; symm; rw [ite_eq_left_iff]; intro ny
    specialize nf y; simp_rw [indicator_of_notMem ny, norm_le_zero_iff] at nf
    simp [nf]
  rename_i msx kpd cancel
  haveI PD : ProofData a q K σ₁ σ₂ F G :=
    ⟨cancel, bF, bG, mF, mG, vF, vG, mσ₁, mσ₂, rσ₁, rσ₂, lσ, Q, hq⟩
  have : kpd = PD.toKernelProofData := by
    sorry
  obtain ⟨G₁, mG₁, vG₁, hG₁⟩ := finitary_carleson X
  refine ⟨G ∩ G₁, inter_subset_left, bG.subset inter_subset_left, mG.inter (by convert mG₁), ?_, ?_⟩
  · refine le_trans ?_ (by convert vG₁); gcongr
    convert measure_mono (μ := volume) (@inter_subset_right _ G G₁) <;> exact this.symm
  · simp_rw [diff_self_inter, T_lin]
    specialize hG₁ f (by convert mf; exact this.symm) nf
    simp_rw [toFinset_Icc, show nnq = q by rfl] at hG₁
    convert hG₁ using 1
    · rfl
    · congr; rw [eq_sub_iff_add_eq]; norm_cast
      exact hqq'.symm.inv_add_inv_eq_one

[Jeremy Tan]

The various converts are due to an instance equality problem I don't know how to solve, namely kpd = PD.toKernelProofData (where kpd is the instance declared outside the lemma). I don't know how to make them the same at instance creation

[Jeremy Tan]

(fpvandoorn/carleson#394)

[Jeremy Tan]

I've also got another total mismatch below:

    convert hG₁ using 1
    · congr! with _ x s ms _ y
      sorry -- ⇑(Q x) = ⇑(ProofData.Q x)
    · congr; rw [eq_sub_iff_add_eq]; norm_cast
      exact hqq'.symm.inv_add_inv_eq_one

[Jeremy Tan]

Actually, ignore all my rambling above, this works:

theorem finitary_carleson_step (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')
    (bF : IsBounded F) (bG : IsBounded G) (mF : MeasurableSet F) (mG : MeasurableSet G)
    (mσ₁ : Measurable σ₁) (mσ₂ : Measurable σ₂) (rσ₁ : (range σ₁).Finite) (rσ₂ : (range σ₂).Finite)
    (lσ : σ₁ ≤ σ₂) (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1) :
    ∃ G' ⊆ G, IsBounded G' ∧ MeasurableSet G' ∧ 2 * volume G' ≤ volume G ∧
    ∫⁻ x in G \ G', ‖T_lin Q σ₁ σ₂ f x‖ₑ ≤
    C2_0_1 a q * (volume G) ^ (q' : ℝ)⁻¹ * (volume F) ^ (q : ℝ)⁻¹ := by
  rcases eq_zero_or_pos (volume G) with vG | vG
  · use ∅, empty_subset _, isBounded_empty, MeasurableSet.empty
    simp only [measure_empty, mul_zero, zero_le, diff_empty, true_and]
    rw [setLIntegral_measure_zero _ _ vG]; exact zero_le _
  rcases eq_zero_or_pos (volume F) with vF | vF
  · use ∅, empty_subset _, isBounded_empty, MeasurableSet.empty
    simp only [measure_empty, mul_zero, zero_le, diff_empty, true_and]
    suffices ∀ x, ‖T_lin Q σ₁ σ₂ f x‖ₑ = 0 by
      rw [lintegral_congr this, lintegral_zero]; exact zero_le _
    intro x; rw [enorm_eq_zero]; refine Finset.sum_eq_zero fun s ms ↦ integral_eq_zero_of_ae ?_
    classical
    convert ite_ae_eq_of_measure_zero (fun y ↦ Ks s x y * f y * exp (I * Q x y)) 0 F vF using 1
    ext y; symm; rw [ite_eq_left_iff]; intro ny
    specialize nf y; simp_rw [indicator_of_notMem ny, norm_le_zero_iff] at nf
    simp [nf]
  letI PD : ProofData a q K σ₁ σ₂ F G :=
    ⟨‹_›, bF, bG, mF, mG, vF, vG, mσ₁, mσ₂, rσ₁, rσ₂, lσ, Q, hq⟩
  obtain ⟨G₁, mG₁, vG₁, hG₁⟩ := finitary_carleson X
  refine ⟨G ∩ G₁, inter_subset_left, bG.subset inter_subset_left, mG.inter mG₁, ?_, ?_⟩
  · refine le_trans ?_ vG₁; gcongr; exact inter_subset_right
  · simp_rw [diff_self_inter, T_lin]
    specialize hG₁ f mf nf
    simp_rw [toFinset_Icc, show nnq = q by rfl] at hG₁
    convert hG₁ using 4; rw [eq_sub_iff_add_eq]; norm_cast
    exact hqq'.symm.inv_add_inv_eq_one

[Jeremy Tan]

What's the difference between haveI and letI that caused my problem?

[Markus Himmel]

Jeremy Tan said:

What's the difference between haveI and letI that caused my problem?

The difference is the same as between have and let: have "forgets" everything after the := and only remembers that it is a term of the given type, so it is usually only suitable for proofs, not data.

By the way, have you tried just using let instead of letI? Lean 3 and Lean 4 both have something called haveI, but they do completely different things: In Lean 3, the "I" is for "instance", because haveI resets the instance cache to make sure that an instance introduced by haveI can be found in the rest of the proof. In Lean 4, there is no instance cache anymore, so using have works just fine for instances. In Lean 4, the "I" is for "inline", and roughly speaking it inlines the value of the have into the resulting proof term instead of preserving the have construct into the proof term.

Of course, we generally don't care about how proof terms look, so Lean 4's haveI and letI are rarely useful in proofs. I think the main use case for haveI and letI is in theorem statements and definitions, where you do want precise control over terms. There you can use haveI and letI if it is useful to give something a name when writing down the statement, but you don't want the name to appear in the final statement:

theorem foo :
  letI a := 5
  a = 5 := rfl

/- foo : 5 = 5 -/
#check foo

theorem bar :
  let a := 5
  a = 5 := rfl

/-
bar :
  let a := 5;
  a = 5
-/
#check bar

[Floris van Doorn]

I'm in bed with a fever, so it will probably take a few days until I can help you.

[Jeremy Tan]

There's not much of a problem adapting finitary_carleson for the L304 setting now; it's now setting up the recursion and monotone convergence theorem. I will ping if I do need help there

[Jeremy Tan]

I've got everything done for Lemma 3.0.4 except the measurability of T_lin:

AEMeasurable ((G \ (slice CP bG mG (n + 1)).G).indicator fun x ↦ ‖T_lin CP.Q σ₁ σ₂ f x‖ₑ) volume

This looks intractable. T_lin is a function from X to the complexes that is a summation of functions, where the summation bounds depend on the input – Finset.(ae)measurable_sum can only handle bounds independent of the input – and there's a Bochner integral inside, whereas I don't see any lemmas to prove measurability of Bochner integrals. Is there a way forward?

[Jeremy Tan]

I got through the outer sum. There's still the inner Bochner integral left:

Measurable fun z ↦ ∫ (y : X), Ks i z y * f y * cexp (I * Q z y)

Can anyone help me with this?

[Michael Rothgang]

I'll try to take a look soon. That may only be tomorrow morning, though (it's already past end of workday for me).

[Jeremy Tan]

@Michael Rothgang In the end I didn't need any help; all that was needed was a swap to StronglyMeasurable, applying StronglyMeasurable.integral_prod_right and swapping back (as has been done in a few other places in Carleson).

Lemma 3.0.4 is now completely proved

[Michael Rothgang]

I took a first look at your PR now. It's bedtime for me now; i'll continue tomorrow.

[Jeremy Tan]

The proof of Lemma 3.0.3 is very off. There's a $T_{1,x}$ mentioned, but as defined $T_{s_1,s_2}$ expects both of its subscripts to be integers, whereas x : X.

As well as that, $\sigma_2$'s construction is said to be "similar" to $\sigma_1$'s, but they look very different in the blueprint. There is a $\max_{\vartheta\in\tilde\Theta}$ expression where $\vartheta$ is not referenced at all

[Jeremy Tan]

And what exactly is $T_{1,s_1,s_2}$?

[Jeremy Tan]

Floris van Doorn said:

I'm in bed with a fever, so it will probably take a few days until I can help you.

Have you recovered yet?

[Floris van Doorn]

The proof is indeed written a bit messily.
$T_{1,s_1, s_2}$ is the same thing as $T_{s_1, s_2}$, just inconsistently named.
The first displayed equation of the proof defines $T_{1,x}$ (so the $:=$ should be $=:$), and so is different from $T_{s_1, s_2}$.
The $\max_{\theta\in\tilde\Theta}$ can be removed.

[Jeremy Tan]

I am having severe problems interpreting the proof of Lemma 3.0.2.

At this point the proof appeals to bounding a set average by the MB function, but it does not give the collection of balls to be used. I cannot figure out a usable collection – the obvious choice would be MB volume (edgeScales a R₁ R₂).toSet (fun _ ↦ x) (D ^ ·) (F.indicator (1 : X → ℝ)) x where edgeScales = {s₁ - 1, s₁ - 2, s₂ + 1, s₂ + 2}, but then the centre function is dependent on x and I can't prove its measurability among other things.

Furthermore, it says to "apply the triangle inequality and estimate (3.0.1) separately with $T_{R_1,R_2,R}$ replaced by (3.0.5) and by each summand of (3.0.6)", but I cannot move the sum of (3.0.6) out of the supremum because its bounds depend on $R_1,R_2$ indirectly through $s_1,s_2$.

How am I to proceed?

image.png

[Jeremy Tan]

I have pushed my progress to fpvandoorn/carleson#418

[Jeremy Tan]

I also do not think bounding the average by MB is correct here. ball x (D ^ s) has to be in MB's ball collection for every x, so X or one of its subsets would have to be countable. But of course, X is uncountable in the cases we're interested in here

[Jeremy Tan]

hold on… maybe globalMaximalFunction is the right function here, not MB

[Floris van Doorn]

In the blueprint, $M$ without subscripts is globalMaximalFunction, which does not depend on a collection of balls anymore. Does that answer your first raised question?

[Floris van Doorn]

Ah, I just see you last message

[Floris van Doorn]

Jeremy Tan said:

Furthermore, it says to "apply the triangle inequality and estimate (3.0.1) separately with $T_{R_1,R_2,R}$ replaced by (3.0.5) and by each summand of (3.0.6)", but I cannot move the sum of (3.0.6) out of the supremum because its bounds depend on $R_1,R_2$ indirectly through $s_1,s_2$.

Within the supremum, you can do the estimate from the displayed equation in your screenshot. The RHS doesn't depend on $R_1$ or $R_2$ anymore, so the supremum goes away.

[Jeremy Tan]

I had a look at the remaining proofs on the road to Lemma 1.0.2 after completing fpvandoorn/carleson#418.

As it is after that PR, Lemma 1.0.3 (linearized_metric_carleson) has the hypothesis (hT : HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·) 2 2 volume volume (C_Ts a)), and the blueprint says that this condition (1.0.23) is a weaker condition than (1.0.18), (hT : HasBoundedStrongType (nontangentialOperator K · ·) 2 2 volume volume (C_Ts a)) found in Lemma 1.0.2 (metric_carleson). I believe this is true. But to prove Lemma 1.0.3 I need Lemma 3.0.2, which requires KernelProofData a K, which (after one of my earlier PRs) includes (1.0.18). As (1.0.18) is indeed used in Lemma 7.2.2, I initially had no idea what to do.

But then I looked at all the remaining blueprint proofs (3.0.1, 1.0.3, 1.0.2) and saw that neither linearizedNontangentialOperator nor (1.0.23) is used in any one of them, or indeed anywhere in the entire blueprint proof.

My question is thus can I delete linearizedNontangentialOperator and replace (1.0.23) with (1.0.18) in the Lean statement of linearized_metric_carleson?

[Jeremy Tan]

In fact, since metric_carleson assumes everything in KernelProofData, I can replace many typeclass instances in the statements of Lemmas 3.0.1, 1.0.3 and 1.0.2 by [KernelProofData a K]

[Jeremy Tan]

fpvandoorn/carleson#419 cleans up the variables according to the above plan

[Floris van Doorn]

No, we don't want to make that change, we want to keep the main results as strong as possible, and making this changes makes theorem 1.0.3 weaker (since you're assuming a stronger hypothesis).

There is indeed a problem that we're using (1.0.18) in Lemma 7.2.2. I expect this is a left-over from an older version of the blueprint, when we didn't prove theorem 1.0.3 along the way. What we can do instead is to add (1.0.23) in KernelProofData, and then fix the proof of Lemma 7.2.2 (I'll ask Lars about this).

[Floris van Doorn]

The proof of Lemma 7.2.2 is already written to use (1.0.23) instead of (1.0.18), and so it should be an easy modification to prove it assuming only (1.0.23) (if the formalized proof follows the blueprint closely).
I added this as task 159. cc @James Sundstrom, who formalized the proof.

I see in fpvandoorn/carleson#221 that James made a modification to the blueprint to line it up with the formalized statement, while it should have been the other way around. I should have caught that during review.

[Jeremy Tan]

@Floris van Doorn In fpvandoorn/carleson#423 I rewrite L7.2.2's proof to use (1.0.23), with all the necessary changes, and still I can't completely close the proof. I dug up the blueprint proof just before fpvandoorn/carleson#225 (the PR that actually changed the proof to use (1.0.18)) and found out that the following integral is unaccounted for:

∫ (y : X) in EAnnulus.cc x' (ENNReal.ofReal R₂) (ENNReal.ofReal R₂), K x' y * f y

In order for the proof to close I need this integral to be zero, which means the set EAnnulus.cc x' (ENNReal.ofReal R₂) (ENNReal.ofReal R₂) = sphere x' R₂ needs to have measure zero. But I can't prove this

[Jeremy Tan]

hold on, I might be able to shuffle some strict and non-strict bounds (I like to think out loud)

[Jeremy Tan]

The restoration of the proof using (1.0.23) is now complete in fpvandoorn/carleson#423. What a hack job that was

[Floris van Doorn]

Thanks for your work, that is really nice!