OAI/Geometry/Convex/GeneralMahler/Budget/Klimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Pointwise Young estimate assembled before integrating; common lemma for the two kernel estimates.

  1. lemma OAI.GeneralMahler.mats_s2 line 14
  2. lemma OAI.GeneralMahler.mats_int line 18
  3. lemma OAI.GeneralMahler.w_Young line 28
  4. lemma OAI.GeneralMahler.Frm.loc_s line 40
  5. lemma OAI.GeneralMahler.ctR_box line 43
  6. lemma OAI.GeneralMahler.ck_i line 48
  7. def OAI.GeneralMahler.Hcomm line 62
  8. lemma OAI.GeneralMahler.ProjField.Klimit line 69

    Source comment

    f,b profiles in k; R profile for diagonal gain; bAv f gives matrix subtracted pairing. κ₀ scales both f and U choice exposed
    lemma Klimit (ht:T∈specBox m tmin tmax)
    {f w R:Plane→ℝ} (hf:Bwt f) (hw:Bwt w) (hR:Bwt R)
    (hp:∀ v:Plane,0≤w v)
    (c:ℝ) (_hc:0≤c)
    (hmat:∀ (z:ℝ) (l:Fin m→ℝ) (t:Mat m), t∈specBox m tmin tmax →
      Matrix.diagonal (fun i=>R (z,l i)) ≤
        c • jprod t (diagonal (fun i=> bAv f (z,l i))))
    (U:ℝ→ℝ→ℝ→ℝ) (b₀:ℝ)
    (hU:∀ x y,Integrable (U x y) ∧ (∫ z,U x y z)=b₀*(x-y)^2)
    (hu:∀ x y z,z≠x→z≠y→0≤U x y z)
    (hK:∀ x y z,z≠x→z≠y→ (c*kz f x y z)^2≤
      ((|x-z| * w (z,x)+|y-z| * w (z,y))/2)*U x y z)
…

    Mentions: OAI.GeneralMahler.specBox, OAI.GeneralMahler.tmin, OAI.GeneralMahler.tmax, OAI.GeneralMahler.Plane, OAI.GeneralMahler.Bwt, OAI.GeneralMahler.Mat, OAI.GeneralMahler.jprod, OAI.GeneralMahler.bAv