OAI/Analysis/FourierLLogL/Compress/Phase.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Compress.char_neg line 15
2. lemma OAI.FourierLLogL.Compress.char_sum line 21
3. lemma OAI.FourierLLogL.Compress.heat_prod line 30
4. def OAI.FourierLLogL.Compress.defect line 60

   Source documentation

   Defect between two letter phases.

   def defect (tag : A → G) (χ : Θ → AddChar G ℂ) (a b : A) (t : Θ) :=
   …

5. lemma OAI.FourierLLogL.Compress.defect_nonneg line 63
6. lemma OAI.FourierLLogL.Compress.defect_mean line 69
7. lemma OAI.FourierLLogL.Compress.phase_region line 81

   Source documentation

   If the characteristic product has large integral, then it has large volume at the corresponding defect level.

   lemma phase_region (Q : Law Θ) (f : I → Θ → ℝ) (hf : ∀ i t, 0 ≤ f i t ∧ f i t ≤ 1)
       {E : ℝ} (he : 1 ≤ E) (h : exp (-(2*E)) ≤ Q.Ex fun t => ∏ i, f i t) :
       let A (x : Θ) := ∑ i, (1-f i x ^ 2)
   …

   Mentions: OAI.FourierLLogL.Law

8. lemma OAI.FourierLLogL.Compress.log_gap line 120
9. lemma OAI.FourierLLogL.Compress.prob_half line 163
10. def OAI.FourierLLogL.Compress.small_defects line 183
11. lemma OAI.FourierLLogL.Compress.alignment line 188