OAI/Analysis/LpDimension/Entropy.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.entropy_le_log_card line 12
2. lemma OAI.SubpolynomialLp.log_ratio_lower line 21
3. lemma OAI.SubpolynomialLp.log_mean_sq_le line 46

   Source documentation

   The logarithmic-mean estimate in a division-free form, valid also at a=b.

   lemma log_mean_sq_le {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
       (a - b) ^ 2 ≤ (a - b) * (Real.log a - Real.log b) * ((a + b) / 2) := by
   …

4. def OAI.SubpolynomialLp.electricalEnergy line 66
5. lemma OAI.SubpolynomialLp.sub_mul_log_sub_nonneg line 70
6. lemma OAI.SubpolynomialLp.electricalEnergy_nonneg line 79
7. lemma OAI.SubpolynomialLp.electrical_cauchy_schwarz line 89

   Source documentation

   The weighted Cauchy--Schwarz step, before mass normalization.

   lemma electrical_cauchy_schwarz (src dst : E → V) (c w : E → ℝ) (h : V → ℝ)
       (hc : ∀ e, 0 ≤ c e) (hh : ∀ i, 0 < h i) :
       (∑ e, w e * Real.sqrt (c e) * |h (src e) - h (dst e)|) ^ 2 ≤
         electricalEnergy src dst c h *
           ∑ e, (w e) ^ 2 * ((h (src e) + h (dst e)) / 2) := by
   …

   Mentions: OAI.SubpolynomialLp.electricalEnergy

8. def OAI.SubpolynomialLp.vertexWeight line 116
9. def OAI.SubpolynomialLp.vertexMass line 120
10. lemma OAI.SubpolynomialLp.vertexWeight_pairing line 123
11. lemma OAI.SubpolynomialLp.vertexMass_pairing line 140
12. lemma OAI.SubpolynomialLp.vertexMass_sum line 145
13. lemma OAI.SubpolynomialLp.heat_cauchy_schwarz line 154

    Source documentation

    The precise normalized energy inequality used in the heat-entropy proof.

    lemma heat_cauchy_schwarz (src dst : E → V) (c w : E → ℝ) (h : V → ℝ)
        (hc : ∀ e, 0 ≤ c e) (hh : ∀ i, 0 < h i)
        (hw : 0 < ∑ e, (w e) ^ 2)
        (hmass : ∑ i, vertexMass src dst w i * h i = 1) :
        (∑ e, w e * Real.sqrt (c e) * |h (src e) - h (dst e)|) ^ 2 ≤
          electricalEnergy src dst c h * (∑ e, (w e) ^ 2) := by
    …

    Mentions: OAI.SubpolynomialLp.vertexMass, OAI.SubpolynomialLp.electricalEnergy

14. def OAI.SubpolynomialLp.graphLaplacian line 170
15. lemma OAI.SubpolynomialLp.graphLaplacian_pairing line 174
16. lemma OAI.SubpolynomialLp.graphLaplacian_sum line 185
17. def OAI.SubpolynomialLp.heatEntropy line 189
18. lemma OAI.SubpolynomialLp.heatEntropy_hasDerivAt line 193

    Source documentation

    Entropy dissipation, from the actual weighted graph heat equation.

    lemma heatEntropy_hasDerivAt (src dst : E → V) (c : E → ℝ) (μ : V → ℝ)
        (h : ℝ → V → ℝ) (s : ℝ) (hμ : ∀ i, 0 < μ i) (hp : ∀ i, 0 < h s i)
        (hd : ∀ i, HasDerivAt (fun t => h t i)
          (-graphLaplacian src dst c (h s) i / μ i) s) :
        HasDerivAt (fun t => heatEntropy μ (h t))
          (-electricalEnergy src dst c (h s)) s := by
    …

    Mentions: OAI.SubpolynomialLp.graphLaplacian, OAI.SubpolynomialLp.heatEntropy, OAI.SubpolynomialLp.electricalEnergy

19. lemma OAI.SubpolynomialLp.heatEntropy_continuous line 220
20. lemma OAI.SubpolynomialLp.heatEntropy_integral line 226

    Source documentation

    The entropy identity for the weighted graph heat flow, including the singular initial point mass. Positivity is only required at strictly positive times.

    lemma heatEntropy_integral (src dst : E → V) (c : E → ℝ) (μ : V → ℝ)
        (h : ℝ → V → ℝ) (v : V) (hc : ∀ e, 0 ≤ c e) (hμ : ∀ i, 0 < μ i)
        (hcont : Continuous h) (hp : ∀ s : ℝ, 0 < s → ∀ i, 0 < h s i)
        (hd : ∀ s : ℝ, 0 < s → ∀ i, HasDerivAt (fun t => h t i)
          (-graphLaplacian src dst c (h s) i / μ i) s)
        (hzero : h 0 = Pi.single v (1 / μ v))
        (htop : Tendsto h atTop (𝓝 (fun _ => 1))) :
        IntegrableOn (fun s => electricalEnergy src dst c (h s)) (Set.Ioi 0) ∧
          (∫ s in Set.Ioi (0 : ℝ), electricalEnergy src dst c (h s)) = Real.log (1 / μ v) := by
    …

    Mentions: OAI.SubpolynomialLp.graphLaplacian, OAI.SubpolynomialLp.electricalEnergy

21. def OAI.SubpolynomialLp.incidence line 265
22. def OAI.SubpolynomialLp.laplacianMatrix line 268
23. lemma OAI.SubpolynomialLp.incidence_mulVec line 272
24. lemma OAI.SubpolynomialLp.laplacianMatrix_mulVec line 276
25. lemma OAI.SubpolynomialLp.laplacianMatrix_symmetric line 288
26. lemma OAI.SubpolynomialLp.laplacianMatrix_posSemidef line 293
27. lemma OAI.SubpolynomialLp.laplacianMatrix_apply line 308
28. lemma OAI.SubpolynomialLp.laplacianMatrix_offdiag_neg line 321
29. lemma OAI.SubpolynomialLp.graphLaplacian_kernel_constant line 338