OAI/MeasureTheory/Falconer/Fourier/PolicyJetData.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Falconer.PolicyJetData line 16

   Source documentation

   Data retained during an angular episode. Its descriptor list and split are computed from the inherited positive interval.

   structure PolicyJetData (m : ℕ) where
   …

2. def OAI.Falconer.PolicyJetData.list line 53
3. def OAI.Falconer.PolicyJetData.longest line 56
4. def OAI.Falconer.PolicyJetData.splitDepth line 58
5. theorem OAI.Falconer.PolicyJetData.list_card line 61
6. theorem OAI.Falconer.PolicyJetData.longest_le_N line 64
7. theorem OAI.Falconer.PolicyJetData.split_gap line 72
8. def OAI.Falconer.PolicyJetData.farThreshold line 88
9. def OAI.Falconer.PolicyJetData.farData line 94

   Source documentation

   The retained list and prescribed split determine the analytic data. No frequency assumption is supplied by the caller.

   noncomputable def farData (P : PolicyJetData m) (B : ℝ)
       (hB : 1 ≤ B) (hσ : 0 < P.σ) (hσ1 : P.σ ≤ 1)
       (hN : farThreshold B P.σ hB hσ hσ1 m ≤ P.N)
       (hfar : P.a < P.splitDepth) (loss : ℝ) (hloss : 0 ≤ loss) : JetStateFarData m B := by
   …

   Mentions: OAI.Falconer.PolicyJetData, OAI.Falconer.PolicyJetData.farThreshold, OAI.Falconer.JetStateFarData