Skip to content

Commit

Permalink
progress on 6.1.3
Browse files Browse the repository at this point in the history
  • Loading branch information
@mariainesdff
mariainesdff committed Aug 9, 2024
1 parent 27ad24e commit 4f239f7
Showing 1 changed file with 91 additions and 191 deletions.
282 changes: 91 additions & 191 deletions Carleson/AntichainOperator.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -224,186 +224,6 @@ lemma MaximalBoundAntichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤
have h0 : (∑ (p ∈ 𝔄), T p f x) = (∑ (p ∈ 𝔄), 0) := Finset.sum_congr rfl (fun p hp ↦ hx p hp)
simp only [h0, Finset.sum_const_zero, nnnorm_zero, ENNReal.coe_zero, zero_le]

--TODO: delete
-- lemma 6.1.2
lemma MaximalBoundAntichain' {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) (𝔄 : Set (𝔓 X)))
(ha : 1 ≤ a) {F : Set X} {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (x : X) :
‖∑ (p ∈ 𝔄), T p f x‖₊ ≤ (C_6_1_2 a) * MB volume 𝔄 𝔠 (fun 𝔭 ↦ 8*D ^ 𝔰 𝔭) f x := by
by_cases hx : ∃ (p : 𝔄), T p f x ≠ 0
· obtain ⟨p, hpx⟩ := hx
have hxE : x ∈ E ↑p := mem_of_indicator_ne_zero hpx
have hne_p : ∀ b ∈ 𝔄, b ≠ ↑p → T b f x = 0 := by
intro p' hp' hpp'
by_contra hp'x
exact hpp' (E_disjoint h𝔄 hp' p.2 ⟨x, mem_of_indicator_ne_zero hp'x, hxE⟩)
have hdist_cp : dist x (𝔠 p) ≤ 4*D ^ 𝔰 p.1 := le_of_lt (mem_ball.mp (Grid_subset_ball hxE.1))
have hdist_y : ∀ {y : X} (hy : Ks (𝔰 p.1) x y ≠ 0),
dist x y ∈ Icc ((D ^ ((𝔰 p.1) - 1) : ℝ) / 4) (D ^ (𝔰 p.1) / 2) := fun hy ↦
dist_mem_Icc_of_Ks_ne_zero hy
have hdist_cpy : ∀ (y : X) (hy : Ks (𝔰 p.1) x y ≠ 0), dist (𝔠 p) y ≤ 8*D ^ 𝔰 p.1 := by
intro y hy
calc dist (𝔠 p) y
≤ dist (𝔠 p) x + dist x y := dist_triangle (𝔠 p.1) x y
_ ≤ 4*D ^ 𝔰 p.1 + dist x y := by simp only [add_le_add_iff_right, dist_comm, hdist_cp]
_ ≤ 4*D ^ 𝔰 p.1 + D ^ 𝔰 p.1 /2 := by
simp only [add_le_add_iff_left, (mem_Icc.mpr (hdist_y hy)).2]
_ ≤ 8*D ^ 𝔰 p.1 := by
rw [div_eq_inv_mul, ← add_mul]
exact mul_le_mul_of_nonneg_right (by norm_num) (by positivity)
-- 6.1.6, 6.1.7
have hKs : ∀ (y : X) (hy : Ks (𝔰 p.1) x y ≠ 0), ‖Ks (𝔰 p.1) x y‖₊ ≤
(2 : ℝ≥0) ^ (5*a + 101*a^3) / volume.real (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)) := by
intro y hy
have h : ‖Ks (𝔰 p.1) x y‖₊ ≤ (2 : ℝ≥0)^(a^3) / volume.real (ball x (D ^ (𝔰 p.1 - 1)/4)) := by
have hxy : x ≠ y := by
intro h_eq
rw [h_eq, Ks_def, ne_eq, mul_eq_zero, not_or, dist_self, mul_zero, psi_zero] at hy
simp only [Complex.ofReal_zero, not_true_eq_false, and_false] at hy
apply le_trans (NNReal.coe_le_coe.mpr kernel_bound)
simp only [NNReal.coe_div, NNReal.coe_pow, NNReal.coe_ofNat, Nat.cast_pow]
rw [← NNReal.val_eq_coe, measureNNReal_val]
exact div_le_div_of_nonneg_left (pow_nonneg zero_le_two _)
(measure_ball_pos_real x _ (div_pos (zpow_pos_of_pos (defaultD_pos _) _) zero_lt_four))
(measureReal_mono (Metric.ball_subset_ball (hdist_y hy).1)
(measure_ball_ne_top x (dist x y)))
apply le_trans h
rw [zpow_sub₀ (by simp), zpow_one, div_div]
-- 4*D = (2 ^ (100 * a ^ 2 + 2))
-- volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
/- have hvol : volume.real (ball x ((↑(D * 4)) * (↑D ^ 𝔰 p.1 / (↑D * 4)))) ≤
2 ^ (100 * a ^ 3 + 2*a) * volume.real (ball x (↑D ^ 𝔰 p.1 / (↑D * 4))) := by
have : D * 4 = 2 ^ (100 * a ^ 2 + 2) := by rw [pow_add]; rfl
rw [this]
simp only [Nat.cast_pow, Nat.cast_ofNat]
apply le_trans (DoublingMeasure.volume_ball_two_le_same_repeat _ _ _)
simp only [defaultA, Nat.cast_pow, Nat.cast_ofNat, NNReal.coe_pow, NNReal.coe_ofNat,
defaultD, defaultκ]
apply le_of_eq
ring
have hvol' : volume.real (ball x ((↑D ^ 𝔰 p.1))) ≤
2 ^ (100 * a ^ 3 + 2*a) * volume.real (ball x (↑D ^ 𝔰 p.1 / (↑D * 4))) := by
apply le_trans _ hvol
field_simp -/
have heq : (2 : ℝ≥0∞) ^ (a : ℝ) ^ 3 / volume (ball x (↑D ^ 𝔰 p.1 / (↑D * 4))) =
2 ^ (2*a + 101*a^3) /
(2 ^ (100 * a ^ 3 + 2*a) * volume (ball x (↑D ^ 𝔰 p.1 / (↑D * 4)))) := by
have h20 : (2 : ℝ≥0∞) ^ (100 * a ^ 3 + 2 * a) ≠ 0 :=
Ne.symm (NeZero.ne' (2 ^ (100 * a ^ 3 + 2 * a)))
have h2top : (2 : ℝ≥0∞) ^ (100 * a ^ 3 + 2 * a) ≠ ⊤ := Ne.symm (ne_of_beq_false rfl)
have hD0 : 0 < (D : ℝ) ^ 𝔰 p.1 / (↑D * 4) := by
simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat, Nat.ofNat_pos,
mul_pos_iff_of_pos_right, pow_pos, div_pos_iff_of_pos_right]
exact zpow_pos_of_pos (pow_pos zero_lt_two (100 * a ^ 2)) (𝔰 p.1)
conv_lhs => rw [← one_mul (volume (ball x (↑D ^ 𝔰 p.1 / (↑D * 4))))]
rw [← ENNReal.div_self (a := (2 : ℝ≥0∞) ^ (100 * a ^ 3 + 2*a)) h20 h2top,
← ENNReal.mul_div_right_comm,
← ENNReal.div_mul _ (mul_ne_zero h20 (ne_of_gt (measure_ball_pos _ _ hD0)))
(mul_ne_top h2top (measure_ball_ne_top x _)) h20 h2top, mul_comm, mul_div]
congr
rw [← Nat.cast_pow, ENNReal.rpow_natCast, ← pow_add]
ring
calc (2 : ℝ≥0) ^ a ^ 3 / volume.real (ball x ((D : ℝ) ^ 𝔰 p.1 / (↑D * 4)))
_ = 2 ^ a ^ 3 / volume.real (ball x ((1 / ((D : ℝ) * 32)) * (8 * D ^ 𝔰 p.1))) := by sorry--ring_nf
_ = 2 ^ a ^ 3 * 2 ^ (5 * a + 100 * a ^ 3) / (2 ^ (5 * a + 100 * a ^ 3) *
volume.real (ball x ((1 / ((D : ℝ) * 32)) * (8 * D ^ 𝔰 p.1)))) := by sorry
_ ≤ 2 ^ a ^ 3 * 2 ^ (5 * a + 100 * a ^ 3) / volume.real (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)) := by
apply div_le_div_of_nonneg_left
· sorry
· sorry
· have heq : 2 ^ (100 * a ^ 2) * 2 ^ 5 * (1 / (↑D * 32) * (8 * (D : ℝ) ^ 𝔰 p.1)) =
(8 * ↑D ^ 𝔰 p.1) := by sorry
have ha : (defaultA a : ℝ) ^ (100 * a ^ 2 + 5) = 2 ^ (5 * a + 100 * a ^ 3) := by
simp only [defaultA, Nat.cast_pow, Nat.cast_ofNat]
ring
have h_le := DoublingMeasure.volume_ball_two_le_same_repeat (𝔠 p.1)
((1 / ((D : ℝ) * 32)) * (8 * D ^ 𝔰 p.1)) (100*a^2 + 5)

rw [← heq, ← pow_add]
apply le_trans h_le
rw [ha]
rw [_root_.mul_le_mul_left]
simp only [measureReal_def]
rw [ENNReal.toReal_le_toReal]
sorry
sorry
--simp? [Real.volume_ball]
sorry

--have hD : D = 2^(100*a^2) := rfl
/- apply ENNReal.div_le_div (le_refl _)
have heq : 2 ^ (100 * a ^ 2) * 2 ^ 5 * (1 / (↑D * 32) * (8 * (D : ℝ) ^ 𝔰 p.1)) =
(8 * ↑D ^ 𝔰 p.1) := by sorry
have h_le := DoublingMeasure.volume_ball_two_le_same_repeat (𝔠 p.1)
((1 / ((D : ℝ) * 32)) * (8 * D ^ 𝔰 p.1)) (100*a^2 + 5)
rw [← heq]
apply le_trans h_le -/

sorry
_ = 2 ^ (5 * a + 101 * a ^ 3) / volume.real (ball (𝔠 p.1) (8 * ↑D ^ 𝔰 p.1)) := by ring_nf


/- simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat, ne_eq, pow_eq_zero_iff',
OfNat.ofNat_ne_zero, mul_eq_zero, not_false_eq_true, pow_eq_zero_iff, false_or, false_and] -/
/- rw [← one_mul (volume (ball x (↑D ^ 𝔰 p.1 / (↑D * 4))))]
rw [← ENNReal.div_self (a := (2 : ℝ≥0∞) ^ (100 * a ^ 3 + 2*a))]
sorry
sorry -/

/- calc ‖Ks (𝔰 p.1) x y‖₊
≤ (2 : ℝ≥0)^(a^3) / volume (ball (𝔠 p.1) (D/4 ^ (𝔰 p.1 - 1))) := by
done
_ ≤ (2 : ℝ≥0)^(5*a + 101*a^3) / volume (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)) :=
sorry -/
calc (‖∑ (p ∈ 𝔄), T p f x‖₊ : ℝ≥0∞)
= ↑‖T p f x‖₊:= by rw [Finset.sum_eq_single_of_mem p.1 p.2 hne_p]
/- _ ≤ ↑‖∫ (y : X), cexp (↑((coeΘ (Q x)) x) - ↑((coeΘ (Q x)) y)) * Ks (𝔰 p.1) x y * f y‖₊ := by
simp only [T, indicator, if_pos hxE, mul_ite, mul_zero, ENNReal.coe_le_coe,
← NNReal.coe_le_coe, coe_nnnorm]
sorry -/
_ ≤ ∫⁻ (y : X), ‖cexp (↑((coeΘ (Q x)) x) - ↑((coeΘ (Q x)) y)) * Ks (𝔰 p.1) x y * f y‖₊ := by
/- simp only [T, indicator, if_pos hxE, mul_ite, mul_zero, ENNReal.coe_le_coe,
← NNReal.coe_le_coe, coe_nnnorm] -/
/- simp only [T, indicator, if_pos hxE]
apply le_trans (MeasureTheory.ennnorm_integral_le_lintegral_ennnorm _)
apply MeasureTheory.lintegral_mono
intro z w -/
simp only [T, indicator, if_pos hxE]
apply le_trans (MeasureTheory.ennnorm_integral_le_lintegral_ennnorm _)
apply lintegral_mono
intro z w
simp only [nnnorm_mul, coe_mul, some_eq_coe', Nat.cast_pow,
Nat.cast_ofNat, zpow_neg, mul_ite, mul_zero]
sorry
_ ≤ (2 : ℝ≥0)^(5*a + 101*a^3) * ⨍⁻ y, ‖f y‖₊ ∂volume.restrict (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)) := by
sorry
_ ≤ (C_6_1_2 a) * (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)).indicator (x := x)
(fun _ ↦ ⨍⁻ y, ‖f y‖₊ ∂volume.restrict (ball (𝔠 p.1) (8*D ^ 𝔰 p.1))) := by
simp only [coe_ofNat, indicator, mem_ball, mul_ite, mul_zero]
rw [if_pos]
apply mul_le_mul_of_nonneg_right _ (zero_le _)
· rw [C_6_1_2]; norm_cast
apply pow_le_pow_right one_le_two
calc
_ ≤ 5 * a ^ 3 + 101 * a ^ 3 := by
gcongr; exact le_self_pow (by linarith [four_le_a X]) (by omega)
_ = 106 * a ^ 3 := by ring
_ ≤ 107 * a ^ 3 := by gcongr; norm_num
· exact lt_of_le_of_lt hdist_cp
(mul_lt_mul_of_nonneg_of_pos (by linarith) (le_refl _) (by linarith)
(zpow_pos_of_pos (defaultD_pos a) _))
_ ≤ (C_6_1_2 a) * MB volume 𝔄 𝔠 (fun 𝔭 ↦ 8*D ^ 𝔰 𝔭) f x := by
rw [mul_le_mul_left _ _, MB, maximalFunction, inv_one, ENNReal.rpow_one, le_iSup_iff]
simp only [mem_image, Finset.mem_coe, iSup_exists, iSup_le_iff,
and_imp, forall_apply_eq_imp_iff₂, ENNReal.rpow_one]
exact (fun _ hc ↦ hc p.1 p.2)
· exact C_6_1_2_ne_zero a
· exact coe_ne_top
· simp only [ne_eq, Subtype.exists, exists_prop, not_exists, not_and, Decidable.not_not] at hx
have h0 : (∑ (p ∈ 𝔄), T p f x) = (∑ (p ∈ 𝔄), 0) := Finset.sum_congr rfl (fun p hp ↦ hx p hp)
simp only [h0, Finset.sum_const_zero, nnnorm_zero, ENNReal.coe_zero, zero_le]

lemma _root_.Set.eq_indicator_one_mul {F : Set X} {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
f = (F.indicator 1) * f := by
ext y
Expand All @@ -418,24 +238,104 @@ lemma _root_.Set.eq_indicator_one_mul {F : Set X} {f : X → ℂ} (hf : ∀ x,
/-- Constant appearing in Lemma 6.1.3. -/
noncomputable def C_6_1_3 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := 2^(111*a^3)*(q-1)⁻¹

-- lemma 6.1.3
lemma Dens2Antichain {𝔄 : Finset (𝔓 X)}
(h𝔄 : IsAntichain (·≤·) (𝔄 : Set (𝔓 X))) {f : X → ℂ}
(hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) {g : X → ℂ} (hg : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
(x : X) :
‖∫ x, ((starRingEnd ℂ) (g x)) * ∑ (p ∈ 𝔄), T p f x‖₊ ≤
(C_6_1_3 a nnq) * (dens₂ (𝔄 : Set (𝔓 X))) * (snorm f 2 volume) * (snorm f 2 volume) := by
namespace ShortVariables

-- q tilde in def. 6.1.9.
scoped notation "q'" => 2*nnq/(nnq + 1)

end ShortVariables

-- lemma 6.1.3, inequality 6.1.10
lemma Dens2Antichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) (𝔄 : Set (𝔓 X))) (ha : 4 ≤ a)
{f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) {g : X → ℂ} (hg : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
(x : X) : ‖∫ x, ((starRingEnd ℂ) (g x)) * ∑ (p ∈ 𝔄), T p f x‖₊ ≤
(C_6_1_3 a nnq) * (dens₂ (𝔄 : Set (𝔓 X))) ^ ((q' : ℝ)⁻¹ - 2⁻¹) *
(snorm f 2 volume) * (snorm g 2 volume) := by
have hf1 : f = (F.indicator 1) * f := eq_indicator_one_mul hf
set q' := 2*nnq/(1 + nnq) with hq'
have hq0 : 0 < nnq := nnq_pos X
have h1q' : 1 ≤ q' := by -- Better proof?
rw [hq', one_le_div (add_pos_iff.mpr (Or.inl zero_lt_one)), two_mul, add_le_add_iff_right]
rw [one_le_div (add_pos_iff.mpr (Or.inr zero_lt_one)), two_mul, add_le_add_iff_left]
exact le_of_lt (q_mem_Ioc X).1
have hqq' : q' ≤ nnq := by -- Better proof?
rw [hq', div_le_iff (add_pos (zero_lt_one) hq0), mul_comm, mul_le_mul_iff_of_pos_left hq0,
rw [add_comm, div_le_iff (add_pos (zero_lt_one) hq0), mul_comm, mul_le_mul_iff_of_pos_left hq0,
← one_add_one_eq_two, add_le_add_iff_left]
exact (nnq_mem_Ioc X).1.le
sorry
have hq'_inv : (q' - 1)⁻¹ ≤ 3 * (nnq - 1)⁻¹ := by
have : (q' - 1)⁻¹ = (nnq + 1)/(nnq -1) := by
nth_rewrite 2 [← div_self (a := nnq + 1) (by simp)]
rw [← NNReal.sub_div, inv_div]
congr 1
rw [two_mul, NNReal.sub_def, NNReal.coe_add, NNReal.coe_add, add_sub_add_left_eq_sub]
rfl
rw [this, div_eq_mul_inv]
gcongr
rw [← two_add_one_eq_three, add_le_add_iff_right]
exact (nnq_mem_Ioc X).2
calc ↑‖∫ x, ((starRingEnd ℂ) (g x)) * ∑ (p ∈ 𝔄), T p f x‖₊
_ ≤ (snorm (∑ (p ∈ 𝔄), T p f) 2 volume) * (snorm g 2 volume) := by
-- 6.1.18. Use Cauchy-Schwarz
rw [mul_comm]
sorry
_ ≤ 2 ^ (107*a^3) * (snorm (fun x ↦ ((MB volume 𝔄 𝔠 (fun 𝔭 ↦ 8*D ^ 𝔰 𝔭) f x).toNNReal : ℂ))
2 volume) * (snorm g 2 volume) := by
-- 6.1.19. Use Lemma 6.1.2.
apply mul_le_mul_of_nonneg_right _ (zero_le _)
have h2 : (2 : ℝ≥0∞) ^ (107 * a ^ 3) = ‖(2 : ℝ) ^ (107 * a ^ 3)‖₊ := by
simp only [nnnorm_pow, nnnorm_two, ENNReal.coe_pow, coe_ofNat]
rw [h2, ← MeasureTheory.snorm_const_smul]
apply snorm_mono_nnnorm
intro z
have MB_top : MB volume (↑𝔄) 𝔠 (fun 𝔭 ↦ 8 * ↑D ^ 𝔰 𝔭) f z ≠ ⊤ := by
-- apply ne_top_of_le_ne_top _ (MB_le_snormEssSup)
--apply ne_of_lt
--apply snormEssSup_lt_top_of_ae_nnnorm_bound
sorry
rw [← ENNReal.coe_le_coe, Finset.sum_apply]
convert (MaximalBoundAntichain h𝔄 (le_trans (by linarith) ha) hf z)
· simp only [Pi.smul_apply, real_smul, nnnorm_mul, nnnorm_eq, nnnorm_mul,
nnnorm_real, nnnorm_pow, nnnorm_two,
nnnorm_eq, coe_mul, C_6_1_2, ENNReal.coe_toNNReal MB_top]
norm_cast
_ ≤ 2 ^ (107*a^3 + 2*a + 2) * (q' - 1)⁻¹ * (dens₂ (𝔄 : Set (𝔓 X))) ^ ((q' : ℝ)⁻¹ - 2⁻¹) *
(snorm f 2 volume) * (snorm g 2 volume) := by
-- 6.1.20. use 6.1.14 and 6.1.16.
sorry
_ ≤ (C_6_1_3 a nnq) * (dens₂ (𝔄 : Set (𝔓 X))) ^ ((q' : ℝ)⁻¹ - 2⁻¹) *
(snorm f 2 volume) * (snorm g 2 volume) := by
-- use 4 ≤ a, hq'_inv.
have h3 : 3 * ((C_6_1_3 a nnq) * (dens₂ (𝔄 : Set (𝔓 X))) ^ ((q' : ℝ)⁻¹ - 2⁻¹) *
(snorm f 2 volume) * (snorm g 2 volume)) =
(2 : ℝ≥0)^(111*a^3) * (3 * (nnq-1)⁻¹) * (dens₂ (𝔄 : Set (𝔓 X))) ^ ((q' : ℝ)⁻¹ - 2⁻¹) *
(snorm f 2 volume) * (snorm g 2 volume) := by
conv_lhs => simp only [C_6_1_3, ENNReal.coe_mul, ← mul_assoc]
rw [mul_comm 3, mul_assoc _ 3]
norm_cast
rw [← ENNReal.mul_le_mul_left (Ne.symm (NeZero.ne' 3)) (ofNat_ne_top 3), h3]
conv_lhs => simp only [← mul_assoc]
gcongr
· norm_cast
calc 3 * 2 ^ (107 * a ^ 3 + 2 * a + 2)
_ ≤ 4 * 2 ^ (107 * a ^ 3 + 2 * a + 2) := mul_le_mul_of_nonneg_right (by omega) (zero_le _)
_ = 2 ^ (107 * a ^ 3 + 2 * a + 4) := by ring
_ ≤ 2 ^ (107 * a ^ 3) * 2 ^ (4 * a ^ 3) := by
rw [add_assoc, pow_add]
apply mul_le_mul_of_nonneg_left _ (zero_le _)
apply pow_right_mono one_le_two
apply Nat.add_le_of_le_sub'
· have h4a3 : 4 * a ^ 3 = 2 * a * (2 * a^2) := by ring
exact h4a3 ▸ Nat.le_mul_of_pos_right _ (by positivity)
· apply le_trans ha
calc a
_ ≤ a * (4 * a ^ 2 - 2) := by
apply Nat.le_mul_of_pos_right _
rw [tsub_pos_iff_lt]
exact lt_of_lt_of_le (by linarith)
(Nat.mul_le_mul_left 4 (pow_le_pow_left zero_le_four ha 2))
_ = 4 * a ^ 3 - 2 * a := by
rw [Nat.mul_sub]
ring_nf
_ = 2 ^ (111 * a ^ 3) := by ring
· norm_cast -- uses hq'_inv

/-- The constant appearing in Proposition 2.0.3.
Has value `2 ^ (150 * a ^ 3) / (q - 1)` in the blueprint. -/
Expand Down

0 comments on commit 4f239f7

Please sign in to comment.