OAI/Analysis/SignedDisk/VectorRefinement1.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SignedDisk.VectorRefinement.quadratic_defect line 29

   Source documentation

   Exact quadratic defect of a positive vector refinement, including zero parent mass.

   theorem quadratic_defect {ι E : Type*} [Fintype ι]
       [NormedAddCommGroup E] [InnerProductSpace ℝ E]
       (w a : ι → ℝ) (θ : ι → E) (n : E) (A : ℝ)
       (hn : ‖n‖ = 1) (hθ : ∀ i, ‖θ i‖ = 1)
       (href : A • n = ∑ i, (w i*a i) • θ i) :
       (∑ i, w i*a i)-A = (1/2:ℝ)*∑ i, w i*a i*‖θ i-n‖^2 := by
   …

2. lemma OAI.SignedDisk.VectorRefinement.sq_norm_triangle line 44
3. theorem OAI.SignedDisk.VectorRefinement.pair_defect_bound line 53

   Source documentation

   Two sufficiently represented children cannot have a large angular disagreement without spending the actual parent's triangle defect.

   theorem pair_defect_bound {ι E : Type*} [Fintype ι] [DecidableEq ι]
       [NormedAddCommGroup E] [InnerProductSpace ℝ E]
       (w a : ι → ℝ) (θ : ι → E) (n : E) (A : ℝ)
       (hw : ∀ i, 0 ≤ w i) (ha : ∀ i, 0 ≤ a i)
       (hn : ‖n‖ = 1) (hθ : ∀ i, ‖θ i‖ = 1)
       (href : A • n = ∑ i, (w i*a i) • θ i)
       {q s : ι} (hwaq : 1/4 ≤ w q) (hwas : 9/64 ≤ w s) (has : a q ≤ a s) :
       a q*‖θ q-θ s‖^2 ≤ 48*((∑ i, w i*a i)-A) := by
   …

4. lemma OAI.SignedDisk.PlanePotential.integral_affine line 90
5. lemma OAI.SignedDisk.PlanePotential.integrable_affine_iff line 101
6. lemma OAI.SignedDisk.PlanePotential.integral_affine_reverse line 112
7. lemma OAI.SignedDisk.PlanePotential.segment_ftc line 117
8. def OAI.SignedDisk.PlanePotential.segmentForm line 130
9. def OAI.SignedDisk.PlanePotential.pullbackForm line 132
10. lemma OAI.SignedDisk.PlanePotential.pullback_identity line 135
11. lemma OAI.SignedDisk.PlanePotential.segmentForm_continuous line 145
12. lemma OAI.SignedDisk.PlanePotential.segmentForm_integrable_column line 151
13. lemma OAI.SignedDisk.PlanePotential.pullbackForm_measurable line 157
14. lemma OAI.SignedDisk.PlanePotential.pullbackForm_integrable_column line 164
15. lemma OAI.SignedDisk.PlanePotential.pullback_column_integral line 171
16. lemma OAI.SignedDisk.PlanePotential.pullback_column_norm line 178
17. lemma OAI.SignedDisk.PlanePotential.segmentForm_bound line 186
18. lemma OAI.SignedDisk.PlanePotential.segment_weight_integrable line 197
19. theorem OAI.SignedDisk.PlanePotential.pullbackForm_integrable line 204

    Source documentation

    Absolute integrability justifies the double integral even at t approaching zero.

    theorem pullbackForm_integrable {ψ g : ℂ → ℝ} (hψ : Continuous ψ)
        (hψc : HasCompactSupport ψ) (hg : ContDiff ℝ 1 g) {D : ℝ}
        (hD : ∀ y, ‖fderiv ℝ g y‖ ≤ D) (x : ℂ) :
        Integrable (fun p : ℝ × ℂ => pullbackForm ψ g x p.1 p.2)
          ((volume.restrict (Ioc (0:ℝ) 1)).prod volume) := by
    …

    Mentions: OAI.SignedDisk.PlanePotential.pullbackForm

20. lemma OAI.SignedDisk.PlanePotential.segmentForm_integrable line 222
21. lemma OAI.SignedDisk.PlanePotential.green_pullback line 239
22. theorem OAI.SignedDisk.PlanePotential.green_representation line 244

    Source documentation

    The true segment-kernel representation, with Fubini justified absolutely.

    theorem green_representation {ψ g : ℂ → ℝ} (hψ : Continuous ψ)
        (hψc : HasCompactSupport ψ) (hg : ContDiff ℝ 1 g) {D : ℝ}
        (hD : ∀ y, ‖fderiv ℝ g y‖ ≤ D) (hψ1 : ∫ z, ψ z = 1) (x : ℂ) :
        (∫ y, fderiv ℝ g y (green ψ x y)) = g x-∫ z, ψ z*g z := by
    …

    Mentions: OAI.SignedDisk.PlanePotential.green

23. lemma OAI.SignedDisk.PlanePotential.lintegral_norm_rpow_near line 278
24. lemma OAI.SignedDisk.PlanePotential.lintegral_norm_rpow_far line 284
25. lemma OAI.SignedDisk.PlanePotential.lintegral_translated_near line 290
26. lemma OAI.SignedDisk.PlanePotential.lintegral_translated_far line 303
27. lemma OAI.SignedDisk.PlanePotential.norm_power_bound line 312
28. lemma OAI.SignedDisk.PlanePotential.kernel_near_three_halves line 325
29. lemma OAI.SignedDisk.PlanePotential.kernel_far_three_halves line 345
30. lemma OAI.SignedDisk.PlanePotential.green_diagonal line 370
31. lemma OAI.SignedDisk.PlanePotential.green_size_all line 373
32. lemma OAI.SignedDisk.PlanePotential.green_near_column line 383
33. lemma OAI.SignedDisk.PlanePotential.green_far_column line 398
34. def OAI.SignedDisk.PlanePotential.cancelledGreen line 429

    Source documentation

    The center is subtracted only off the near region, so this measurable kernel retains integrability at the center and realizes zero-mass cancellation.

    def cancelledGreen (ψ : ℂ → ℝ) (z : ℂ) (a : ℝ) (x y : ℂ) : ℂ :=
    …

35. lemma OAI.SignedDisk.PlanePotential.cancelledGreen_measurable line 432
36. lemma OAI.SignedDisk.PlanePotential.green_piece_column line 440