OAI/Analysis/ForestSpace/Paired.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ForestSpace.gateSigns line 16
2. theorem OAI.ForestSpace.gateSigns_sq line 19
3. def OAI.ForestSpace.correctedTail line 22
4. theorem OAI.ForestSpace.correctedTail_supported line 25
5. theorem OAI.ForestSpace.correctedTail_testBound line 32
6. theorem OAI.ForestSpace.correctedTail_at_gate line 44
7. theorem OAI.ForestSpace.gate_charge_le line 58
8. theorem OAI.ForestSpace.segment_cut line 65

   Source documentation

   The local choice of a suffix cut, including empty cuts for inexpensive terms.

    theorem segment_cut (hF : ForestOrder V) {H : Set V} (hH : IsLowerSet H)
       {f k : V → ℝ} (hf : SupportedOn f H) (hk : SupportedOn k Hᶜ)
       {s τ : ℝ} (hs : 0 ≤ s) (hτ : |τ| ≤ 1)
       {S : Finset V} (hS : IsSegment S) :
       ∃ L : Finset V, L ⊆ S.filter (· ∈ H) ∧ IsSegment L ∧
         IsSegment (S.filter (· ∈ H) \ L) ∧
         (segSum f S + s * segSum (correctedTail H f k s τ) S) ^ 2 ≤
           (segSum f S - segSum f L) ^ 2 + segSum f L ^ 2 +
           8 * s ^ 2 * (∑ v ∈ S, gateWeight H k v) +
           s ^ 2 * segSum (correctedTail H f k s τ) S ^ 2 := by
   …

   Mentions: OAI.ForestSpace.ForestOrder, OAI.ForestSpace.SupportedOn, OAI.ForestSpace.IsSegment, OAI.ForestSpace.segSum, OAI.ForestSpace.correctedTail, OAI.ForestSpace.gateWeight

9. theorem OAI.ForestSpace.simultaneous_cut_bound line 117

   Source documentation

   All suffix cuts can be charged to one disjoint segment test of the head.

    theorem simultaneous_cut_bound [Fintype V] [PartialOrder V] {H : Set V} {f : V → ℝ}
       (hf : SupportedOn f H) (hf₁ : TestBound f 1)
       {ι : Type} [Fintype ι] (S L : ι → Finset V)
       (hd : Pairwise (fun i j => Disjoint (S i) (S j)))
       (hL : ∀ i, L i ⊆ (S i).filter (· ∈ H))
       (hseg : ∀ i, IsSegment (L i))
       (hdiff : ∀ i, IsSegment ((S i).filter (· ∈ H) \ L i)) :
       (∑ i, ((segSum f (S i) - segSum f (L i)) ^ 2 + segSum f (L i) ^ 2)) ≤ 1 := by
   …

   Mentions: OAI.ForestSpace.SupportedOn, OAI.ForestSpace.TestBound, OAI.ForestSpace.IsSegment, OAI.ForestSpace.segSum

10. theorem OAI.ForestSpace.corrected_test_bound line 157

    Source documentation

    The corrected tests have squared norm at most 1+12s², for either sign.

     theorem corrected_test_bound (hF : ForestOrder V) {H : Set V} (hH : IsLowerSet H)
        {f k : V → ℝ} (hf : SupportedOn f H) (hk : SupportedOn k Hᶜ)
        (hf₁ : TestBound f 1) (hk₁ : TestBound k 1)
        {s τ : ℝ} (hs : 0 ≤ s) (hτ : |τ| ≤ 1) :
        TestBound (f + s • correctedTail H f k s τ) (1 + 12 * s ^ 2) := by
    …

    Mentions: OAI.ForestSpace.ForestOrder, OAI.ForestSpace.SupportedOn, OAI.ForestSpace.TestBound, OAI.ForestSpace.correctedTail

11. theorem OAI.ForestSpace.paired_finite_test_correction line 177

    Source documentation

    Finite-support paired extension: the common correction cancels on averaging.

     theorem paired_finite_test_correction
        (hF : ForestOrder V) (H : Set V) (hH : IsLowerSet H) (f k : V → ℝ)
        (hf : ∀ v, v ∉ H → f v = 0) (hk : ∀ v, v ∈ H → k v = 0)
        (hf₁ : TestBound f 1) (hk₁ : TestBound k 1)
        (s : ℝ) (hs : 0 < s) :
        ∃ c : V → ℝ, (∀ v, v ∈ H → c v = 0) ∧ TestBound c 1 ∧
          TestBound (f + s • (c + k)) (1 + 12 * s ^ 2) ∧
          TestBound (f + s • (c - k)) (1 + 12 * s ^ 2) := by
    …

    Mentions: OAI.ForestSpace.ForestOrder, OAI.ForestSpace.TestBound

12. theorem OAI.ForestSpace.forestOrder_subtype line 202
13. theorem OAI.ForestSpace.IsSegment.subtype line 206
14. theorem OAI.ForestSpace.IsSegment.image_subtype line 214
15. theorem OAI.ForestSpace.segSum_image_subtype line 228
16. theorem OAI.ForestSpace.segSum_subtype line 233
17. theorem OAI.ForestSpace.TestBound.restrict_subtype line 241
18. theorem OAI.ForestSpace.TestBound.of_restrict line 251
19. theorem OAI.ForestSpace.exists_finite_lower_hull line 265

    Source documentation

    The finite ancestor assumption ensures that no node inserted between two supported coordinates is lost when we use a finite test forest.

     theorem exists_finite_lower_hull (hAnc : ∀ v : V, (Set.Iic v).Finite)
        (S : Finset V) : ∃ B : Finset V, S ⊆ B ∧ IsLowerSet (B : Set V) := by
    …

20. def OAI.ForestSpace.finiteExtension line 278

    Source documentation

    Extension by zero from a finite lower subforest.

    noncomputable def finiteExtension (B : Finset V) (u : B → ℝ) : V →₀ ℝ :=
    …

21. theorem OAI.ForestSpace.finiteExtension_apply line 285
22. theorem OAI.ForestSpace.finiteExtension_supported line 289
23. theorem OAI.ForestSpace.finiteExtension_testBound line 294
24. theorem OAI.ForestSpace.finsupp_paired_correction line 301

    Source documentation

    The finite-support corrected tests on an arbitrary finite-ancestor forest. No assertion about the full dual having dense finite coordinates is used.

     theorem finsupp_paired_correction (hF : ForestOrder V)
        (hAnc : ∀ v : V, (Set.Iic v).Finite)
        (H : Set V) (hH : IsLowerSet H) (f k : V →₀ ℝ)
        (hf : SupportedOn f H) (hk : SupportedOn k Hᶜ)
        (hf₁ : TestBound f 1) (hk₁ : TestBound k 1) (s : ℝ) (hs : 0 < s) :
        ∃ c : V →₀ ℝ, SupportedOn c Hᶜ ∧ TestBound c 1 ∧
          TestBound (f + s • (c + k)) (1 + 12 * s ^ 2) ∧
          TestBound (f + s • (c - k)) (1 + 12 * s ^ 2) := by
    …

    Mentions: OAI.ForestSpace.ForestOrder, OAI.ForestSpace.SupportedOn, OAI.ForestSpace.TestBound