OAI/Analysis/LipschitzHilbert/Trees/SourceWeightedBadPath.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.weighted_small_set_le line 15
2. theorem OAI.LipschitzHilbert.source_line_weighted_bad line 48

   Source documentation

   On every interval of top length, an unweighted relative tail becomes an equally small weighted tail, up to the fixed weight comparison factor.

   theorem source_line_weighted_bad (T : SlopeBox) (origin y H : ℝ) {K D δ : ℝ}
       (hK : 1 ≤ K) (hD : 0 ≤ D) (hH : 0 < H) (hHT : H ≤ T.length)
       (hδ : 0 ≤ δ) (bad : Set ℝ) (hbad : MeasurableSet bad)
       (hsmall : (volume.restrict (Ico origin (origin+H))).real bad ≤ δ*H) :
       IntegrableOn (bad.indicator (fun x => T.weight K D (x,y+T.slope*x)))
         (Ico origin (origin+H)) volume ∧
         (∫ x in Ico origin (origin+H), bad.indicator
           (fun x => T.weight K D (x,y+T.slope*x)) x) ≤
           (Real.exp (2*D)*δ)*(∫ x in Ico origin (origin+H), T.weight K D (x,y+T.slope*x)) := by
   …

   Mentions: OAI.LipschitzHilbert.SlopeBox

3. theorem OAI.LipschitzHilbert.source_weighted_bad_path_area line 79

   Source documentation

   Summing the line estimates over all tiles and then all tops retains exactly the total top area and the full spatial weight.

   theorem source_weighted_bad_path_area {ι : Type*} (tops : Finset ι)
       (T : ι → SlopeBox) (bad : ι → Set (ℝ × ℝ))
       (hbad : ∀ t ∈ tops, MeasurableSet (bad t)) {K D δ : ℝ}
       (hK : 1 ≤ K) (hD : 2 < D) (hδ : 0 ≤ δ)
       (htail : ∀ t ∈ tops, ∀ᵐ y : ℝ ∂volume, ∀ k : ℤ,
         (volume.restrict (sourceLineTile (T t).length k)).real
           {x | (x,y+(T t).slope*x) ∈ bad t} ≤ δ*(T t).length) :
       Integrable (fun z => ∑ t ∈ tops, (bad t).indicator ((T t).weight K D) z)
         (volume.prod volume) ∧
         (∫ z, ∑ t ∈ tops, (bad t).indicator ((T t).weight K D) z ∂volume.prod volume) ≤
           (((Real.exp (2*D)*δ)*(2^D*∫ z, topProfile D z ∂volume.prod volume))*K^2)*
             ∑ t ∈ tops, (T t).length*(T t).width := by
   …

   Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.sourceLineTile, OAI.LipschitzHilbert.topProfile