added comments

Author: SmaniaD

Burkholder/Basic.lean

@@ -1 +1,7 @@
+/--
+A tiny exported test definition.
+
+It is just a sanity-check value used by the package skeleton,
+returning the string "world".
+-/
 def hello := "world"

Burkholder/Majorants.lean

@@ -24,6 +24,17 @@ namespace Majorants
 
 /- Final result: majorant exists for p > 1 -/
 
+/--
+Main existence theorem for the Burkholder majorant when `p > 1`.
+
+In plain terms: this says we can build a function `u` (with first derivatives)
+that has controlled growth, satisfies the tangent-step inequality used in the
+martingale argument, dominates the base Burkholder function `v`, and is
+nonpositive on the opposite-sign region `x * y ≤ 0`.
+
+The proof dispatches to the specialized constructions in the three regimes
+`p = 2`, `p > 2`, and `1 < p < 2`.
+-/
 theorem exists_majorant_p_g_1 (p : ℝ) (hp : p> 1) :
     ∃ u du_dx du_dy : ℝ → ℝ → ℝ, ∃ C : ℝ,
       0 ≤ C ∧

Burkholder/Majorants/Majorant_p_eq_2.lean

@@ -19,6 +19,14 @@ noncomputable section
 
 namespace Majorants
 
+/--
+Explicit majorant package in the special case `p = 2`.
+
+At this exponent the construction becomes very concrete: we can take
+`u(x,y) = x*y`, with derivatives `du_dx = y` and `du_dy = x`.
+This theorem checks, one by one, that this choice satisfies the full list of
+majorant requirements (growth, tangency, domination of `v`, and sign behavior).
+-/
 theorem exists_majorant_p_eq_2 (p : ℝ) (hp : p=2) :
      ∃ u du_dx du_dy : ℝ → ℝ → ℝ, ∃ C : ℝ,
       0 ≤ C ∧