11.9. HardyZeta.HardyWeight🔗

def hardyWeight (t : ℝ) : ℝ := hardyXi t / (t ^ 2 + 1 / 4)theorem ofReal_hardyWeight (t : ℝ) : (hardyWeight t : ℂ) = -completedRiemannZeta (criticalPoint t) / 2 := byt:ℝ⊢ ↑(hardyWeight t) = -completedRiemannZeta (criticalPoint t) / 2 have ht : (t : ℂ) ^ 2 + 1 / 4 ≠ 0 := by intro het:ℝhe:↑t ^ 2 + 1 / 4 = 0⊢ False have h := congrArg Complex.re het:ℝhe:↑t ^ 2 + 1 / 4 = 0h:(↑t ^ 2 + 1 / 4).re = re 0⊢ False norm_num [pow_two] at ht:ℝhe:↑t ^ 2 + 1 / 4 = 0h:t * t + 1 / 4 = 0⊢ False nlinarith [sq_nonneg t]t:ℝht:↑t ^ 2 + 1 / 4 ≠ 0⊢ ↑(hardyWeight t) = -completedRiemannZeta (criticalPoint t) / 2 unfold hardyWeightt:ℝht:↑t ^ 2 + 1 / 4 ≠ 0⊢ ↑(hardyXi t / (t ^ 2 + 1 / 4)) = -completedRiemannZeta (criticalPoint t) / 2 push_castt:ℝht:↑t ^ 2 + 1 / 4 ≠ 0⊢ ↑(hardyXi t) / (↑t ^ 2 + 1 / 4) = -completedRiemannZeta (criticalPoint t) / 2 rw [ofReal_hardyXi,t:ℝht:↑t ^ 2 + 1 / 4 ≠ 0⊢ criticalXi t / (↑t ^ 2 + 1 / 4) = -completedRiemannZeta (criticalPoint t) / 2 criticalXi,t:ℝht:↑t ^ 2 + 1 / 4 ≠ 0⊢ xi (criticalPoint t) / (↑t ^ 2 + 1 / 4) = -completedRiemannZeta (criticalPoint t) / 2 xit:ℝht:↑t ^ 2 + 1 / 4 ≠ 0⊢ 1 / 2 * criticalPoint t * (criticalPoint t - 1) * completedRiemannZeta (criticalPoint t) / (↑t ^ 2 + 1 / 4) = -completedRiemannZeta (criticalPoint t) / 2]t:ℝht:↑t ^ 2 + 1 / 4 ≠ 0⊢ 1 / 2 * criticalPoint t * (criticalPoint t - 1) * completedRiemannZeta (criticalPoint t) / (↑t ^ 2 + 1 / 4) = -completedRiemannZeta (criticalPoint t) / 2 have hs : criticalPoint t * (criticalPoint t - 1) = -((t : ℂ) ^ 2 + 1 / 4) := byt:ℝ⊢ ↑(hardyWeight t) = -completedRiemannZeta (criticalPoint t) / 2 unfold criticalPointt:ℝht:↑t ^ 2 + 1 / 4 ≠ 0⊢ (1 / 2 + ↑t * I) * (1 / 2 + ↑t * I - 1) = -(↑t ^ 2 + 1 / 4) ring_nft:ℝht:↑t ^ 2 + 1 / 4 ≠ 0⊢ -1 / 4 + ↑t ^ 2 * I ^ 2 = -1 / 4 - ↑t ^ 2 simp [I_sq]t:ℝht:↑t ^ 2 + 1 / 4 ≠ 0⊢ -1 / 4 + -↑t ^ 2 = -1 / 4 - ↑t ^ 2 ringt:ℝht:↑t ^ 2 + 1 / 4 ≠ 0hs:criticalPoint t * (criticalPoint t - 1) = -(↑t ^ 2 + 1 / 4)⊢ 1 / 2 * criticalPoint t * (criticalPoint t - 1) * completedRiemannZeta (criticalPoint t) / (↑t ^ 2 + 1 / 4) = -completedRiemannZeta (criticalPoint t) / 2 rw [mul_assoc (1 / 2) (criticalPoint t),t:ℝht:↑t ^ 2 + 1 / 4 ≠ 0hs:criticalPoint t * (criticalPoint t - 1) = -(↑t ^ 2 + 1 / 4)⊢ 1 / 2 * (criticalPoint t * (criticalPoint t - 1)) * completedRiemannZeta (criticalPoint t) / (↑t ^ 2 + 1 / 4) = -completedRiemannZeta (criticalPoint t) / 2 hst:ℝht:↑t ^ 2 + 1 / 4 ≠ 0hs:criticalPoint t * (criticalPoint t - 1) = -(↑t ^ 2 + 1 / 4)⊢ 1 / 2 * -(↑t ^ 2 + 1 / 4) * completedRiemannZeta (criticalPoint t) / (↑t ^ 2 + 1 / 4) = -completedRiemannZeta (criticalPoint t) / 2]t:ℝht:↑t ^ 2 + 1 / 4 ≠ 0hs:criticalPoint t * (criticalPoint t - 1) = -(↑t ^ 2 + 1 / 4)⊢ 1 / 2 * -(↑t ^ 2 + 1 / 4) * completedRiemannZeta (criticalPoint t) / (↑t ^ 2 + 1 / 4) = -completedRiemannZeta (criticalPoint t) / 2 rw [div_eq_iff htt:ℝht:↑t ^ 2 + 1 / 4 ≠ 0hs:criticalPoint t * (criticalPoint t - 1) = -(↑t ^ 2 + 1 / 4)⊢ 1 / 2 * -(↑t ^ 2 + 1 / 4) * completedRiemannZeta (criticalPoint t) = -completedRiemannZeta (criticalPoint t) / 2 * (↑t ^ 2 + 1 / 4)]t:ℝht:↑t ^ 2 + 1 / 4 ≠ 0hs:criticalPoint t * (criticalPoint t - 1) = -(↑t ^ 2 + 1 / 4)⊢ 1 / 2 * -(↑t ^ 2 + 1 / 4) * completedRiemannZeta (criticalPoint t) = -completedRiemannZeta (criticalPoint t) / 2 * (↑t ^ 2 + 1 / 4) ringAll goals completed! 🐙theorem continuous_hardyWeight : Continuous hardyWeight := by⊢ Continuous hardyWeight unfold hardyWeight⊢ Continuous fun t => hardyXi t / (t ^ 2 + 1 / 4) exact continuous_hardyXi.div (by⊢ Continuous fun t => t ^ 2 + 1 / 4 fun_propAll goals completed! 🐙) (fun t ↦ byt:ℝ⊢ t ^ 2 + 1 / 4 ≠ 0 positivityAll goals completed! 🐙)theorem hardyWeight_neg (t : ℝ) : hardyWeight (-t) = hardyWeight t := byt:ℝ⊢ hardyWeight (-t) = hardyWeight t simp [hardyWeight, hardyXi_neg]All goals completed! 🐙theorem abs_hardyWeight_le {a : ℝ} (ha : 0 < a) (ha' : a < Real.pi / 4) (t : ℝ) : |hardyWeight t| ≤ (thetaHorizontalMass (-2 * a) / 4) * Real.exp (-a * t) := bya:ℝha:0 < aha':a < Real.pi / 4t:ℝ⊢ |hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t) have h := norm_completedZeta_critical_le ha ha' ta:ℝha:0 < aha':a < Real.pi / 4t:ℝh:‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)⊢ |hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t) have he : |hardyWeight t| = ‖completedRiemannZeta (criticalPoint t)‖ / 2 := by rw [← Real.norm_eq_abs,a:ℝha:0 < aha':a < Real.pi / 4t:ℝh:‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)⊢ ‖hardyWeight t‖ = ‖completedRiemannZeta (criticalPoint t)‖ / 2 ← norm_real,a:ℝha:0 < aha':a < Real.pi / 4t:ℝh:‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)⊢ ‖↑(hardyWeight t)‖ = ‖completedRiemannZeta (criticalPoint t)‖ / 2 ofReal_hardyWeight,a:ℝha:0 < aha':a < Real.pi / 4t:ℝh:‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)⊢ ‖-completedRiemannZeta (criticalPoint t) / 2‖ = ‖completedRiemannZeta (criticalPoint t)‖ / 2 norm_div,a:ℝha:0 < aha':a < Real.pi / 4t:ℝh:‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)⊢ ‖-completedRiemannZeta (criticalPoint t)‖ / ‖2‖ = ‖completedRiemannZeta (criticalPoint t)‖ / 2 norm_nega:ℝha:0 < aha':a < Real.pi / 4t:ℝh:‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)⊢ ‖completedRiemannZeta (criticalPoint t)‖ / ‖2‖ = ‖completedRiemannZeta (criticalPoint t)‖ / 2]a:ℝha:0 < aha':a < Real.pi / 4t:ℝh:‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)⊢ ‖completedRiemannZeta (criticalPoint t)‖ / ‖2‖ = ‖completedRiemannZeta (criticalPoint t)‖ / 2 norm_numa:ℝha:0 < aha':a < Real.pi / 4t:ℝh:‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)he:|hardyWeight t| = ‖completedRiemannZeta (criticalPoint t)‖ / 2⊢ |hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t) rw [hea:ℝha:0 < aha':a < Real.pi / 4t:ℝh:‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)he:|hardyWeight t| = ‖completedRiemannZeta (criticalPoint t)‖ / 2⊢ ‖completedRiemannZeta (criticalPoint t)‖ / 2 ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)]a:ℝha:0 < aha':a < Real.pi / 4t:ℝh:‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)he:|hardyWeight t| = ‖completedRiemannZeta (criticalPoint t)‖ / 2⊢ ‖completedRiemannZeta (criticalPoint t)‖ / 2 ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t) nlinarithAll goals completed! 🐙theorem cosh_le_exp_abs (x : ℝ) : Real.cosh x ≤ Real.exp |x| := byx:ℝ⊢ Real.cosh x ≤ Real.exp |x| rw [Real.cosh_eqx:ℝ⊢ (Real.exp x + Real.exp (-x)) / 2 ≤ Real.exp |x|]x:ℝ⊢ (Real.exp x + Real.exp (-x)) / 2 ≤ Real.exp |x| have hp := Real.exp_le_exp.mpr (le_abs_self x)x:ℝhp:Real.exp x ≤ Real.exp |x|⊢ (Real.exp x + Real.exp (-x)) / 2 ≤ Real.exp |x| have hn := Real.exp_le_exp.mpr (neg_le_abs x)x:ℝhp:Real.exp x ≤ Real.exp |x|hn:Real.exp (-x) ≤ Real.exp |x|⊢ (Real.exp x + Real.exp (-x)) / 2 ≤ Real.exp |x| linarithAll goals completed! 🐙 /-- The actual cosh-weighted zeta integral is absolutely convergent in the open strip. -/theorem integrableOn_hardyWeight_cosh {α : ℝ} (hα : |α| < Real.pi / 4) : IntegrableOn (fun t : ℝ ↦ hardyWeight t * Real.cosh (α * t)) (Ioi 0) := byα:ℝhα:|α| < Real.pi / 4⊢ IntegrableOn (fun t => hardyWeight t * Real.cosh (α * t)) (Ioi 0) volume obtain ⟨a, ha, ha'⟩ := exists_between hαα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4⊢ IntegrableOn (fun t => hardyWeight t * Real.cosh (α * t)) (Ioi 0) volume have ha0 : 0 < a := (abs_nonneg α).trans_lt haα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < a⊢ IntegrableOn (fun t => hardyWeight t * Real.cosh (α * t)) (Ioi 0) volume have h0 := integrableOn_exp_mul_Ioi (a := -(a - |α|)) (byα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < a⊢ -(a - |α|) < 0 linarithAll goals completed! 🐙) 0α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volume⊢ IntegrableOn (fun t => hardyWeight t * Real.cosh (α * t)) (Ioi 0) volume have hdec := h0.const_mul (thetaHorizontalMass (-2 * a) / 4)α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))⊢ IntegrableOn (fun t => hardyWeight t * Real.cosh (α * t)) (Ioi 0) volume apply hdec.mono'hfα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))⊢ AEStronglyMeasurable (fun t => hardyWeight t * Real.cosh (α * t)) (volume.restrict (Ioi 0))hα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))⊢ ∀ᵐ (a_1 : ℝ) ∂volume.restrict (Ioi 0), ‖hardyWeight a_1 * Real.cosh (α * a_1)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * a_1) ·hfα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))⊢ AEStronglyMeasurable (fun t => hardyWeight t * Real.cosh (α * t)) (volume.restrict (Ioi 0)) exact (continuous_hardyWeight.mul (byα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))⊢ Continuous fun t => Real.cosh (α * t) fun_propAll goals completed! 🐙)).aestronglyMeasurable ·hα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))⊢ ∀ᵐ (a_1 : ℝ) ∂volume.restrict (Ioi 0), ‖hardyWeight a_1 * Real.cosh (α * a_1)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * a_1) filter_upwards [ae_restrict_mem measurableSet_Ioi] with t htα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0⊢ ‖hardyWeight t * Real.cosh (α * t)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) have ht0 : 0 ≤ t := le_of_lt htα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ t⊢ ‖hardyWeight t * Real.cosh (α * t)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) have hc : 0 ≤ thetaHorizontalMass (-2 * a) / 4 := div_nonneg (thetaHorizontalMass_nonneg _) (byα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ t⊢ 0 ≤ 4 norm_numAll goals completed! 🐙)α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4⊢ ‖hardyWeight t * Real.cosh (α * t)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) have hb := abs_hardyWeight_le ha0 ha' tα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)⊢ ‖hardyWeight t * Real.cosh (α * t)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) have hh : Real.cosh (α * t) ≤ Real.exp (|α| * t) := byα:ℝhα:|α| < Real.pi / 4⊢ IntegrableOn (fun t => hardyWeight t * Real.cosh (α * t)) (Ioi 0) volume simpa only [abs_mul, abs_of_nonneg ht0] using cosh_le_exp_abs (α * t)α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)hh:Real.cosh (α * t) ≤ Real.exp (|α| * t)⊢ ‖hardyWeight t * Real.cosh (α * t)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) rw [Real.norm_eq_abs,α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)hh:Real.cosh (α * t) ≤ Real.exp (|α| * t)⊢ |hardyWeight t * Real.cosh (α * t)| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) abs_mul,α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)hh:Real.cosh (α * t) ≤ Real.exp (|α| * t)⊢ |hardyWeight t| * |Real.cosh (α * t)| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) abs_of_pos (Real.cosh_pos _)α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)hh:Real.cosh (α * t) ≤ Real.exp (|α| * t)⊢ |hardyWeight t| * Real.cosh (α * t) ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t)]α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)hh:Real.cosh (α * t) ≤ Real.exp (|α| * t)⊢ |hardyWeight t| * Real.cosh (α * t) ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) calc |hardyWeight t| * Real.cosh (α * t) ≤ ((thetaHorizontalMass (-2 * a) / 4) * Real.exp (-a * t)) * Real.exp (|α| * t) := mul_le_mul hb hh (Real.cosh_pos _).le (mul_nonneg hc (Real.exp_pos _).le) _ = (thetaHorizontalMass (-2 * a) / 4) * Real.exp (-(a - |α|) * t) := byα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)hh:Real.cosh (α * t) ≤ Real.exp (|α| * t)⊢ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t) * Real.exp (|α| * t) = thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) rw [mul_assoc,α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)hh:Real.cosh (α * t) ≤ Real.exp (|α| * t)⊢ thetaHorizontalMass (-2 * a) / 4 * (Real.exp (-a * t) * Real.exp (|α| * t)) = thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) ← Real.exp_addα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)hh:Real.cosh (α * t) ≤ Real.exp (|α| * t)⊢ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t + |α| * t) = thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t)]α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)hh:Real.cosh (α * t) ≤ Real.exp (|α| * t)⊢ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t + |α| * t) = thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * t) congr 2e_aα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:IntegrableOn (fun x => Real.exp (-(a - |α|) * x)) (Ioi 0) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * x)) (volume.restrict (Ioi 0))t:ℝht:t ∈ Ioi 0ht0:0 ≤ thc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)hh:Real.cosh (α * t) ≤ Real.exp (|α| * t)⊢ -a * t + |α| * t = -(a - |α|) * t ringAll goals completed! 🐙theorem hardyWeight_abs (t : ℝ) : hardyWeight |t| = hardyWeight t := byt:ℝ⊢ hardyWeight |t| = hardyWeight t rcases le_total 0 t with h | hinlt:ℝh:0 ≤ t⊢ hardyWeight |t| = hardyWeight tinrt:ℝh:t ≤ 0⊢ hardyWeight |t| = hardyWeight t ·inlt:ℝh:0 ≤ t⊢ hardyWeight |t| = hardyWeight t rw [abs_of_nonneg hinlt:ℝh:0 ≤ t⊢ hardyWeight t = hardyWeight t]All goals completed! 🐙 ·inrt:ℝh:t ≤ 0⊢ hardyWeight |t| = hardyWeight t rw [abs_of_nonpos h,inrt:ℝh:t ≤ 0⊢ hardyWeight (-t) = hardyWeight t hardyWeight_neginrt:ℝh:t ≤ 0⊢ hardyWeight t = hardyWeight t]All goals completed! 🐙theorem abs_hardyWeight_le_abs {a : ℝ} (ha : 0 < a) (ha' : a < Real.pi / 4) (t : ℝ) : |hardyWeight t| ≤ (thetaHorizontalMass (-2 * a) / 4) * Real.exp (-a * |t|) := bya:ℝha:0 < aha':a < Real.pi / 4t:ℝ⊢ |hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|) simpa only [hardyWeight_abs] using abs_hardyWeight_le ha ha' |t|All goals completed! 🐙 /-- Two-sided absolute convergence for exponential weights inside the strip. -/theorem integrable_hardyWeight_exp {α : ℝ} (hα : |α| < Real.pi / 4) : Integrable (fun t : ℝ ↦ hardyWeight t * Real.exp (α * t)) := byα:ℝhα:|α| < Real.pi / 4⊢ Integrable (fun t => hardyWeight t * Real.exp (α * t)) volume obtain ⟨a, ha, ha'⟩ := exists_between hαα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4⊢ Integrable (fun t => hardyWeight t * Real.exp (α * t)) volume have ha0 : 0 < a := (abs_nonneg α).trans_lt haα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < a⊢ Integrable (fun t => hardyWeight t * Real.exp (α * t)) volume have h0 := (integrable_exp_neg_abs (a := a - |α|) (byα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < a⊢ 0 < a - |α| linarithAll goals completed! 🐙)).normα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => ‖↑(Real.exp (-(a - |α|) * |a_1|))‖) volume⊢ Integrable (fun t => hardyWeight t * Real.exp (α * t)) volume simp only [norm_real, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] at h0α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volume⊢ Integrable (fun t => hardyWeight t * Real.exp (α * t)) volume have hdec := h0.const_mul (thetaHorizontalMass (-2 * a) / 4)α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volume⊢ Integrable (fun t => hardyWeight t * Real.exp (α * t)) volume apply hdec.mono'hfα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volume⊢ AEStronglyMeasurable (fun t => hardyWeight t * Real.exp (α * t)) volumehα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volume⊢ ∀ᵐ (a_1 : ℝ), ‖hardyWeight a_1 * Real.exp (α * a_1)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |a_1|) ·hfα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volume⊢ AEStronglyMeasurable (fun t => hardyWeight t * Real.exp (α * t)) volume exact (continuous_hardyWeight.mul (byα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volume⊢ Continuous fun t => Real.exp (α * t) fun_propAll goals completed! 🐙)).aestronglyMeasurable ·hα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volume⊢ ∀ᵐ (a_1 : ℝ), ‖hardyWeight a_1 * Real.exp (α * a_1)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |a_1|) filter_upwards with thα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝ⊢ ‖hardyWeight t * Real.exp (α * t)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|) have hc : 0 ≤ thetaHorizontalMass (-2 * a) / 4 := div_nonneg (thetaHorizontalMass_nonneg _) (byα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝ⊢ 0 ≤ 4 norm_numAll goals completed! 🐙)hα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4⊢ ‖hardyWeight t * Real.exp (α * t)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|) have hb := abs_hardyWeight_le_abs ha0 ha' thα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)⊢ ‖hardyWeight t * Real.exp (α * t)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|) have hh : Real.exp (α * t) ≤ Real.exp (|α| * |t|) := byα:ℝhα:|α| < Real.pi / 4⊢ Integrable (fun t => hardyWeight t * Real.exp (α * t)) volume apply Real.exp_le_exp.mprα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)⊢ α * t ≤ |α| * |t| rw [← abs_mulα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)⊢ α * t ≤ |α * t|]α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)⊢ α * t ≤ |α * t| exact le_abs_self _hα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)hh:Real.exp (α * t) ≤ Real.exp (|α| * |t|)⊢ ‖hardyWeight t * Real.exp (α * t)‖ ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|) rw [Real.norm_eq_abs,hα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)hh:Real.exp (α * t) ≤ Real.exp (|α| * |t|)⊢ |hardyWeight t * Real.exp (α * t)| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|) abs_mul,hα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)hh:Real.exp (α * t) ≤ Real.exp (|α| * |t|)⊢ |hardyWeight t| * |Real.exp (α * t)| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|) abs_of_pos (Real.exp_pos _)hα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)hh:Real.exp (α * t) ≤ Real.exp (|α| * |t|)⊢ |hardyWeight t| * Real.exp (α * t) ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|)]hα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)hh:Real.exp (α * t) ≤ Real.exp (|α| * |t|)⊢ |hardyWeight t| * Real.exp (α * t) ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|) calc |hardyWeight t| * Real.exp (α * t) ≤ ((thetaHorizontalMass (-2 * a) / 4) * Real.exp (-a * |t|)) * Real.exp (|α| * |t|) := mul_le_mul hb hh (Real.exp_pos _).le (mul_nonneg hc (Real.exp_pos _).le) _ = (thetaHorizontalMass (-2 * a) / 4) * Real.exp (-(a - |α|) * |t|) := byα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)hh:Real.exp (α * t) ≤ Real.exp (|α| * |t|)⊢ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|) * Real.exp (|α| * |t|) = thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|) rw [mul_assoc,α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)hh:Real.exp (α * t) ≤ Real.exp (|α| * |t|)⊢ thetaHorizontalMass (-2 * a) / 4 * (Real.exp (-a * |t|) * Real.exp (|α| * |t|)) = thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|) ← Real.exp_addα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)hh:Real.exp (α * t) ≤ Real.exp (|α| * |t|)⊢ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t| + |α| * |t|) = thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|)]α:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)hh:Real.exp (α * t) ≤ Real.exp (|α| * |t|)⊢ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t| + |α| * |t|) = thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |t|) congr 2e_aα:ℝhα:|α| < Real.pi / 4a:ℝha:|α| < aha':a < Real.pi / 4ha0:0 < ah0:Integrable (fun a_1 => Real.exp (-(a - |α|) * |a_1|)) volumehdec:Integrable (fun x => thetaHorizontalMass (-2 * a) / 4 * Real.exp (-(a - |α|) * |x|)) volumet:ℝhc:0 ≤ thetaHorizontalMass (-2 * a) / 4hb:|hardyWeight t| ≤ thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)hh:Real.exp (α * t) ≤ Real.exp (|α| * |t|)⊢ -a * |t| + |α| * |t| = -(a - |α|) * |t| ringAll goals completed! 🐙