OAI/Analysis/LipschitzHilbert/Phase/SourceActivePrediction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Removing the zero snapshot children preserves the exact prediction. The remaining children have significant representatives, with precisely the one allowed unshrunk path exception.

  1. abbrev OAI.LipschitzHilbert.SourceActive line 17
  2. theorem OAI.LipschitzHilbert.sum_source_active line 19
  3. theorem OAI.LipschitzHilbert.source_prediction_active line 31
  4. theorem OAI.LipschitzHilbert.source_snapshot_active line 45
  5. theorem OAI.LipschitzHilbert.eventually_source_active_significant line 66

    Source documentation

    Nonzero shrunken children must be significant, except for the one path child that the source deliberately leaves unshrunk.

    theorem eventually_source_active_significant (Q : ℝ) :
    ∀ᶠ L : ℝ in atTop, ∀ (ι κ : Type) [Fintype κ]
      (c : ι → ℝ) (A : ι → EuclideanSpace ℂ κ) (significant : ι → Prop) (path : ι),
      (∀ i, 0 ≤ c i) →
      (∀ i, ¬significant i → ‖A i‖ ≤ (L^Q*Real.exp (-L*Real.log L))*c i) →
      let shrink := fun i => if i = path then A i else
…