diff --git a/Carleson/AntichainOperator.lean b/Carleson/AntichainOperator.lean index 2535f9ea..4adaffaf 100644 --- a/Carleson/AntichainOperator.lean +++ b/Carleson/AntichainOperator.lean @@ -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 @@ -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. -/