OAI/Analysis/LipschitzHilbert/Estimates/WitnessBinCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.SlopeBox.compact_witness_list_count line 17

   Source documentation

   Every compact witness supplies one of the popular bins counted by the same reference count. The count was chosen independently of this finite list.

   theorem compact_witness_list_count {ι : Type*} [DecidableEq ι]
       (R : SlopeBox) (T : ι → SlopeBox) (I : Finset ι)
       (u : ℝ × ℝ → ℝ) (hu : Measurable u) (z : ℝ × ℝ)
       {A q P θ c : ℝ} {M : ℕ} (hA : 0 < A) (hq : 0 ≤ q)
       (hP : 0 < P) (hAP : A ≤ P) (hθ : θ ≤ q / (4 * A * P))
       (E : ι → Set (ℝ × ℝ)) (bin : ι → AngularBins.Bin M)
       (hbin : Set.InjOn bin I)
       (hcompact : ∀ i ∈ I, IsCompact (E i))
       (hbox : ∀ i ∈ I, ∀ w ∈ E i, (T i).radius w ≤ A)
       (harea : ∀ i ∈ I, q * (T i).length * (T i).width ≤ (volume.prod volume).real (E i))
       (hlength : ∀ i ∈ I, (T i).length ≤ R.length)
       (hz : ∀ i ∈ I, (T i).radius z ≤ P)
   …

   Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.AngularBins.Bin, OAI.LipschitzHilbert.SlopeBox.radius

2. theorem OAI.LipschitzHilbert.SlopeBox.compact_witness_count_outside line 66

   Source documentation

   The same compact-witness count is bounded at every significant point outside the fixed reference exceptional set.

   theorem compact_witness_count_outside {R : SlopeBox} {N : ℝ × ℝ → ℝ≥0∞}
       {K lambda : ℝ} {z : ℝ × ℝ} {n : ℕ}
       (hcount : (n : ℝ≥0∞) ≤ N ((R.referenceChart.symm z).2, z.1))
       (hz : R.radius z ≤ K) (hout : z ∉ R.referenceException N K lambda)
       (hlambda : 0 ≤ lambda) : (n : ℝ) ≤ lambda := by
   …

   Mentions: OAI.LipschitzHilbert.SlopeBox