CountingDiscard.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The cost of discarding the counting exceptional set

This proves §6 count:discard-cost from the actual restricted integral, the ordinary model's L² estimate, and the exceptional-set area budget.

theorem OAI.LipschitzHilbert.integral_norm_on_set_le_l2 line 26

Source documentation

Cauchy–Schwarz on a finite-measure set, with the L² energy taken on the whole space. In particular the restricted norm integral exists.

theorem integral_norm_on_set_le_l2 (μ : Measure X) (P : X → V)
    (hP : MemLp P 2 μ) {A : Set X} (hA : μ A ≠ ∞) :
    IntegrableOn (fun x => ‖P x‖) A μ ∧
      (∫ x in A, ‖P x‖ ∂μ) ≤
        Real.sqrt (∫ x, ‖P x‖ ^ 2 ∂μ) * Real.sqrt (μ.real A) := by
…

theorem OAI.LipschitzHilbert.sqrt_exp_half line 48

theorem OAI.LipschitzHilbert.counting_discard_from_area line 55

Source documentation

The L² model estimate and the area budget give the exponentially small discarded integral with its exact square-root loss.

theorem counting_discard_from_area (μ : Measure X) (P : X → V)
    (hP : MemLp P 2 μ) {A E : Set X} (hA : μ A ≠ ∞)
    {K B J L : ℝ} (hK : 0 ≤ K) (hB : 0 ≤ B)
    (hmodel : (∫ x, ‖P x‖ ^ 2 ∂μ) ≤ K ^ 2 * μ.real E)
    (harea : μ.real A ≤ B * μ.real E * Real.exp (-J * L)) :
    IntegrableOn (fun x => ‖P x‖) A μ ∧
      (∫ x in A, ‖P x‖ ∂μ) ≤ K * Real.sqrt B * μ.real E * Real.exp (-J * L / 2) := by
…

theorem OAI.LipschitzHilbert.counting_discard_cost line 81

Source documentation

Converting |E|=N²|F| and N≤exp(2L) gives the precise exponent (2-J/2)L in the source discard estimate.

theorem counting_discard_cost (μ : Measure X) (P : X → V)
    (hP : MemLp P 2 μ) {A E F : Set X} (hA : μ A ≠ ∞)
    {K B J L N : ℝ} (hK : 0 ≤ K) (hB : 0 ≤ B) (hN : 0 ≤ N)
    (hratio : μ.real E = N ^ 2 * μ.real F) (hNlarge : N ≤ Real.exp (2 * L))
    (hmodel : (∫ x, ‖P x‖ ^ 2 ∂μ) ≤ K ^ 2 * μ.real E)
    (harea : μ.real A ≤ B * μ.real E * Real.exp (-J * L)) :
    IntegrableOn (fun x => ‖P x‖) A μ ∧
      (∫ x in A, ‖P x‖ ∂μ) ≤
        (K * Real.sqrt B) * Real.exp ((2 - J / 2) * L) * N * μ.real F := by
…