Lemma 7.5.2 is unprovable

Stream: Carleson

[Jeremy Tan]

I've just realised that Lemma 7.5.2 is unprovable. Take a look at the following:

import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.NNReal.Defs

namespace NNReal

open scoped NNReal

lemma div_self_eq_ite {x : ℝ≥0} : x / x = if 0 < x then 1 else 0 := by
  split_ifs with h
  · exact div_self h.ne'
  · simpa using h

lemma finset_sum_pos_iff {ι : Type*} {s : Finset ι} {f : ι → ℝ≥0} :
    0 < ∑ x ∈ s, f x ↔ ∃ x ∈ s, 0 < f x := by
  rw [← not_iff_not]; push_neg; simp

end NNReal

lemma χtilde_pos_iff : 0 < χtilde J x ↔ x ∈ ball (c J) (8 * D ^ s J) := by
  have := one_le_D (a := a)
  rw [χtilde, Real.toNNReal_pos, sub_pos, zpow_neg, inv_mul_lt_iff₀' (by positivity)]; rfl

/-- Part of Lemma 7.5.2. -/
lemma sum_χ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (x : X) :
    ∑ J ∈ 𝓙₅ t u₁ u₂, χ t u₁ u₂ J x = (𝓘 u₁ : Set X).indicator 1 x := by
  simp_rw [χ, ← Finset.sum_div, NNReal.div_self_eq_ite, indicator, Pi.one_apply]
  -- (if 0 < ∑ J' ∈ (t.𝓙₅ u₁ u₂).toFinset, χtilde J' x then 1 else 0) = if x ∈ ↑(𝓘 u₁) then 1 else 0
  refine if_congr ?_ rfl rfl
  simp_rw [NNReal.finset_sum_pos_iff, mem_toFinset, χtilde_pos_iff, ← exists_prop, ← mem_iUnion₂]
  revert x; simp_rw [← Set.ext_iff, ← union_𝓙₅ hu₁ hu₂ hu h2u]
  sorry -- ⋃ J ∈ 𝓙₅ t u₁ u₂, ball (c J) (8 * D ^ s J) = ⋃ J ∈ 𝓙₅ t u₁ u₂, ↑J

In the partial code for sum_χ every step is an equality or an iff, so the statement beside the sorry is equivalent to the original statement. But then it's easy to imagine a situation where there are parts of the ball (c J) (8 * D ^ s J)s lying outside all the ↑Js, since ↑J ⊆ ball (c J) (4 * D ^ s J). Therefore sum_χ is unprovable.

[Jeremy Tan]

Actually I've reduced sum_χ to proving that for all J ∈ 𝓙₅ t u₁ u₂ there's a tile p ∈ 𝔗 u₁ with ℐ p = J, but I don't know how to prove that.

[Jeremy Tan]

There's also a problem with Lemma 7.3.2 (local dens1 tree bound). There's an easily proven distance bound (really a ball inclusion, smul 9 p ≤ smul 1 q), but it is then written that $L\cap E(\mathfrak q)\subseteq E_2(9,\mathfrak p)$. The problem with this is that $E_2$ is an intersection involving the exceptional set $G$, which appears nowhere else in the proof, while $L\cap E(\mathfrak q)$ does not involve $G$

[Jeremy Tan]

And then for Lemma 7.6.3: (1) the proof doesn't work when n = 0 (since it assumes s₁ = C7_6_3 > 0, but it's -2 when n = 0), and (2) was ${\mathcal{I}}(\mathfrak q) \notin \mathcal{J}'$ intended in the second paragraph rather than ${\mathcal{I}}(\mathfrak u_1) \notin \mathcal{J}'$?

[Floris van Doorn]

In Lemma 7.5.2, doesn't equation (2.0.37) (referenced in the proof) show the subset-relation?

[Floris van Doorn]

Ah, I see with your second message you had the same idea. I asked my coauthors to help you further.

[Floris van Doorn]

This is the message Lars sent me:

About 7.3.2:
This is a slightly bigger mistake, I think it comes from changing
conventions whether E(p) is automatically contained in G or not.
We should assume that g \le 1_G in Lemma 7.3.1, and replace E(u) in the
proof by its intersection with G.
Then we can also add an intersection with G on the left hand side in
(7.3.2) and then the proof works. It is then probably necessary to add the
assumption g \le 1_G everywhere where Lemma 7.3.1 is used. In particular
in the Forest Proposition. This is ok, because it is finally only applied
to the indicator function of a subset of G, in the proof of Lemma 5.1.2.
About 7.5.2:
I agree that Equation (7.5.2) is wrong as written. The fix is to add in
the definition of \chi_J a case distinction that sets it to zero outside
of I(u_1). This does not affect the rest of the conclusions of the lemma,
because they only make statements about points in I(u_1).
About 7.6.3:
2) No, it is supposed to be I(u_1) \not\in J', the purpose of this
sentence is only to show that the partition J' of I(u_1) consists not just
of the single cube I(u_1). This implies that every cube in the partition
is strictly contained in I(u_1), which is what the next sentence says.

Discussion on 7.6.3(1) still ongoing.

Thanks for these questions/corrections. I'll make the appropriate fixes to the statements.

[Floris van Doorn]

Fixed the blueprint and some statements in fpvandoorn/carleson#245

[Floris van Doorn]

https://github.com/fpvandoorn/carleson/commit/58b57be765df3bf5b3ab3759c7ddd988ac38b1c4 addresses your concerns about Lemma 7.6.3(1). The argument was indeed not quite accurate for $n=0$.

[Jeremy Tan]

Regarding Lemma 7.3.2: "Let p' be the unique tile such that 𝓘 p' = L' and such that ¬Disjoint (Ω u) (Ω p')." I don't see how this actually holds

[Jeremy Tan]

Will claim Lemma 7.5.9 here. I noticed that displays (7.5.18), (7.5.19) include an unindexed $\mathfrak u$, but no other hypothesis of global_tree_control1_2 includes $\mathfrak u$, only $\mathfrak u_1$ or $\mathfrak u_2$. Which of these last two was intended in (7.5.18) and (7.5.19)?

[Floris van Doorn]

About 7.5.9: that was indeed stated unclearly in the blueprint, and the formalized statement was wrong.
Lars and I just pushed a fix for the blueprint and the formalized statement.

[Floris van Doorn]

For the question about 7.3.2: this follows from (2.0.13) & (2.0.14) & (2.0.15): by (2.0.15) $Q(u)\in \Omega(u)$. Then by (2.0.14) there is a unique tile $p'$ with $I(p')=L'$ and $Q(u)\in I(p')$. By (2.0.14) you also get the uniqueness of $p'$ with the non-disjointness condition. I believe we also need that $p'\in T(u)$, which should follow from (2.0.33).

[Jeremy Tan]

@Floris van Doorn Lemma 7.5.9 is now sorry-free. I still have that nagging issue with an undefined q' in Lemma 7.3.2