OAI/Analysis/SeparableQuotients/WindowCharges.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.ActualSpace.PartialBlock line 12

   Source documentation

   A crop meets but does not contain an actual finite block support.

   def PartialBlock {f : Family} (z : BlockSequence f) (A : Crop) (i : ℕ) : Prop :=
   …

   Mentions: OAI.SeparableQuotient.ActualSpace.BlockSequence

2. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.partial_crop_le_four line 15
3. lemma OAI.SeparableQuotient.ActualSpace.evaluateArray_crop_finite_fixed line 54
4. lemma OAI.SeparableQuotient.ActualSpace.evaluateArray_crop_nonzero_support line 63
5. lemma OAI.SeparableQuotient.ActualSpace.crop_or_fixed_of_nonzero line 74
6. lemma OAI.SeparableQuotient.ActualSpace.cropped_weighted_abs_sum_bound line 90

   Source documentation

   The weighted absolute column estimate, obtained using the actual rational Type II normers and density of rational coefficients, not an assumed dual ball.

   lemma cropped_weighted_abs_sum_bound {f : Family} {h : ℕ} (P : Fin h → FinitePath f)
       (A : Fin h → Crop) (hm : ∀ b i j, ((P b).piece i).child j ∈ f.norming)
       (hdis : Pairwise (fun i j => Disjoint ((P i).active (A i)) ((P j).active (A j))))
       (c : Fin h → ℝ) (x : E) :
       (∑ i, |c i| * |croppedPathFunctional (P i) (A i) x|) ≤
         (∑ i, |c i|^f.q)^(1/f.q) * ‖x‖ := by
   …

   Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.croppedPathFunctional

7. lemma OAI.SeparableQuotient.ActualSpace.TypeII.window_column_bound line 108
8. lemma OAI.SeparableQuotient.ActualSpace.cropped_window_anchor line 130
9. lemma OAI.SeparableQuotient.ActualSpace.TypeII.cropped_window_count line 146

   Source documentation

   Distinct original active weights bound the number of paths contributing in a window. The +1 version is convenient for zero-based natural indices; the positive-weight sharper T bound is not needed for the geometric charge.

   lemma TypeII.cropped_window_count {f : Family} (e : TypeII f) (x : E) (J T : ℕ) :
       (Finset.univ.filter (fun b => norming.evaluateArray x
         (restrict ((e.crop b).set f) ((e.path b).window J T)) ≠ 0)).card ≤ T+1 := by
   …

   Mentions: OAI.SeparableQuotient.ActualSpace.e, OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.restrict

10. def OAI.SeparableQuotient.ActualSpace.firstNonzero line 170
11. lemma OAI.SeparableQuotient.ActualSpace.firstNonzero_mem line 173
12. lemma OAI.SeparableQuotient.ActualSpace.firstNonzero_le line 179
13. def OAI.SeparableQuotient.ActualSpace.ThinnedWindows.middleEval line 185
14. def OAI.SeparableQuotient.ActualSpace.ThinnedWindows.marks line 190
15. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.marks_card line 198
16. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.unmarked_small line 212
17. lemma OAI.SeparableQuotient.ActualSpace.geometric_charge_le line 244
18. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.unmarked_column line 254